Improvement. Change the unit propagation method to not set the model.

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

diff --git a/src/sat/MinisatCore.h b/src/sat/MinisatCore.h
index d40f2784c64a8596b0740c9bbeb08616820373eb..1f94c8fd276786bca579d181435e3c49f0dcf88a 100644 (file)
--- a/src/sat/MinisatCore.h
+++ b/src/sat/MinisatCore.h
@@ -39,6 +39,12 @@ namespace BEEV
 
     virtual uint8_t modelValue(Var x) const;
 
+    uint8_t
+    value(Var x) const
+    {
+      return Minisat::toInt(s->value(x));
+    }
+
     virtual Var newVar();
 
     int setVerbosity(int v);

diff --git a/src/sat/core/Solver.cc b/src/sat/core/Solver.cc
index ce509e6eaa00bcd18e411d4979228a9ea3753ab0..732873c330447298f00e0b51f4df7eaf3031bade 100644 (file)
--- a/src/sat/core/Solver.cc
+++ b/src/sat/core/Solver.cc
@@ -747,14 +747,24 @@ static double luby(double y, int x){
     return pow(y, seq);
 }
 
+// NB. This method doesn't copy into the modelValue. You need to read the results
+// with value(). So you can't add any clauses to the SAT solver until you've
+// cancelleduntil(0)  --- which clears the values. Otherwise the results will be wrong.
+
 bool Solver::unitPropagate(  const vec<Lit>& assumps)
 {
   model.clear();
   conflict.clear();
 
+  remove_satisfied = false;
   ok = true;
 
-  assert(assumptions.size() == 0);
+  cancelUntil(0);
+  for (int i = 0; i < nVars(); i++)
+    {
+    assert(value(i) == l_Undef);
+    }
+
   assert(decisionLevel()== 0);
 
   // None of the values should be known.
@@ -763,7 +773,7 @@ bool Solver::unitPropagate(  const vec<Lit>& assumps)
     assert(value(i) == l_Undef);
     }
 
-
+  assumptions.clear();
   assumps.copyTo(assumptions);
 
   while (decisionLevel() < assumptions.size())
@@ -788,21 +798,6 @@ bool Solver::unitPropagate(  const vec<Lit>& assumps)
       }
   }
 
-  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;
 }