Improvement. Adds an extra method to minisat that does unit propagation given some...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1642 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/sat/MinisatCore.h b/src/sat/MinisatCore.h
index 30919c6d4e4549bab462fb1d50a9a7b67a765b3a..d40f2784c64a8596b0740c9bbeb08616820373eb 100644 (file)
--- a/src/sat/MinisatCore.h
+++ b/src/sat/MinisatCore.h
@@ -54,6 +54,11 @@ namespace BEEV
     virtual lbool undef_literal()  {return ((uint8_t)2);}
 
     virtual int nClauses();
+
+    bool unitPropagate(const vec_literals& ps)
+    {
+      return s->unitPropagate(ps);
+    }
   };
 }
 ;

diff --git a/src/sat/core/Solver.cc b/src/sat/core/Solver.cc
index 6c8ad78240ba3ed006fb3ebeb40ec48d97d38b2e..ce509e6eaa00bcd18e411d4979228a9ea3753ab0 100644 (file)
--- a/src/sat/core/Solver.cc
+++ b/src/sat/core/Solver.cc
@@ -747,6 +747,66 @@ static double luby(double y, int x){
     return pow(y, seq);
 }
 
+bool Solver::unitPropagate(  const vec<Lit>& assumps)
+{
+  model.clear();
+  conflict.clear();
+
+  ok = true;
+
+  assert(assumptions.size() == 0);
+  assert(decisionLevel()== 0);
+
+  // None of the values should be known.
+  for (int i = 0; i < nVars(); i++)
+    {
+    assert(value(i) == l_Undef);
+    }
+
+
+  assumps.copyTo(assumptions);
+
+  while (decisionLevel() < assumptions.size())
+    {
+      // Perform user provided assumption:
+      Lit p = assumptions[decisionLevel()];
+      if (value(p) == l_True){
+          // Dummy decision level:
+          newDecisionLevel();
+      }else if (value(p) == l_False){
+          analyzeFinal(~p, conflict);
+          ok =false;
+          break;
+      }else{
+          newDecisionLevel();
+          uncheckedEnqueue(p);
+          if (propagate() != CRef_Undef)
+            {
+            ok =false;
+            break;
+            }
+      }
+  }
+
+  if (ok)
+    {
+      // Extend & copy model:
+      model.growTo(nVars());
+      for (int i = 0; i < nVars(); i++) model[i] = value(i);
+    }
+
+  cancelUntil(0);
+  assumptions.clear();
+
+  for (int i = 0; i < nVars(); i++)
+    {
+    assert(value(i) == l_Undef);
+    }
+
+  return ok;
+}
+
+
 // NOTE: assumptions passed in member-variable 'assumptions'.
 lbool Solver::solve_()
 {
@@ -799,11 +859,18 @@ lbool Solver::solve_()
 
 static Var mapVar(Var x, vec<Var>& map, Var& max)
 {
-    if (map.size() <= x || map[x] == -1){
+  if (max < x+1)
+    max =x+1;
+  return x;
+
+/*
+
+   if (map.size() <= x || map[x] == -1){
         map.growTo(x+1, -1);
         map[x] = max++;
     }
     return map[x];
+    */
 }
 
 
@@ -828,6 +895,7 @@ void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
 }
 
 
+
 void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
 {
     // Handle case when solver is in contradictory state:

diff --git a/src/sat/core/Solver.h b/src/sat/core/Solver.h
index af16887e7746d480e3d8aa537a99f280a4bae4ab..2979ca62d49890b06177ce8e13c0a880024b85aa 100644 (file)
--- a/src/sat/core/Solver.h
+++ b/src/sat/core/Solver.h
@@ -138,6 +138,8 @@ public:
     uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
     uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
 
+    bool unitPropagate(  const vec<Lit>& assumps);
+
 protected:
 
     // Helper structures:
@@ -185,7 +187,11 @@ protected:
     int                 qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
     int                 simpDB_assigns;   // Number of top-level assignments since last execution of 'simplify()'.
     int64_t             simpDB_props;     // Remaining number of propagations that must be made before next execution of 'simplify()'.
+
+
     vec<Lit>            assumptions;      // Current set of assumptions provided to solve by the user.
+
+
     Heap<VarOrderLt>    order_heap;       // A priority queue of variables ordered with respect to the variable activity.
     double              progress_estimate;// Set by 'search()'.
     bool                remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.

diff --git a/src/sat/core/SolverTypes.h b/src/sat/core/SolverTypes.h
index c193378b1a93ef8bb35b0ecc40998a19b5746d0e..0bcf9459d7c38b56d26b4920e035b05945e356ec 100644 (file)
--- a/src/sat/core/SolverTypes.h
+++ b/src/sat/core/SolverTypes.h
@@ -81,9 +81,9 @@ const Lit lit_Error = { -1 };  // }
 //       does enough constant propagation to produce sensible code, and this appears to be somewhat
 //       fragile unfortunately.
 
-#define l_True  (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
-#define l_False (lbool((uint8_t)1))
-#define l_Undef (lbool((uint8_t)2))
+#define l_True  (Minisat::lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
+#define l_False (Minisat::lbool((uint8_t)1))
+#define l_Undef (Minisat::lbool((uint8_t)2))
 
 class lbool {
     uint8_t value;