From bb39647f233fbaa93e44f138e58ac1d425256bd1 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 20 Apr 2012 01:01:00 +0000
Subject: [PATCH] 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
---
 src/sat/MinisatCore.h  |  6 ++++++
 src/sat/core/Solver.cc | 29 ++++++++++++-----------------
 2 files changed, 18 insertions(+), 17 deletions(-)

diff --git a/src/sat/MinisatCore.h b/src/sat/MinisatCore.h
index d40f278..1f94c8f 100644
--- 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 ce509e6..732873c 100644
--- 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;
 }
 
-- 
2.47.3