From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 15 Apr 2010 15:53:38 +0000 (+0000)
Subject: CMS2 update: Extending the conglomerated clauses was done too early. Also, some non... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=bd7bcd8d5ef49da039c61e754f783f28db662ca4;p=francis%2Fstp.git

CMS2 update: Extending the conglomerated clauses was done too early. Also, some non-decision variables were set for no reason in the model

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

diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index ee986c3..552b2a8 100644
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -2010,7 +2010,6 @@ lbool Solver::solve(const vec<Lit>& assumps)
         }
         
         partHandler->addSavedState();
-        conglomerate->doCalcAtFinish();
         varReplacer->extendModelPossible();
 #ifndef NDEBUG
         //checkSolution();
@@ -2019,13 +2018,17 @@ lbool Solver::solve(const vec<Lit>& assumps)
         if (subsumer->getNumElimed() > 0) {
             Solver s;
             s.doSubsumption = false;
+            s.performReplace = false;
             s.findBinaryXors = false;
             s.findNormalXors = false;
             s.failedVarSearch = false;
+            s.conglomerateXors = false;
             s.greedyUnbound = greedyUnbound;
             for (Var var = 0; var < nVars(); var++) {
                 s.newVar(decision_var[var] || subsumer->getVarElimed()[var] || varReplacer->varHasBeenReplaced(var));
+                assert(!(conglomerate->getRemovedVars()[var] && (decision_var[var] || subsumer->getVarElimed()[var] || varReplacer->varHasBeenReplaced(var))));
                 if (value(var) != l_Undef) {
+                    assert(!conglomerate->getRemovedVars()[var]);
                     vec<Lit> tmp;
                     tmp.push(Lit(var, value(var) == l_False));
                     s.addClause(tmp);
@@ -2037,9 +2040,10 @@ lbool Solver::solve(const vec<Lit>& assumps)
             status = s.solve();
             assert(status == l_True);
             for (Var var = 0; var < nVars(); var++) {
-                if (assigns[var] == l_Undef) uncheckedEnqueue(Lit(var, s.model[var] == l_False));
+                if (assigns[var] == l_Undef && s.model[var] != l_Undef) uncheckedEnqueue(Lit(var, s.model[var] == l_False));
             }
         }
+        conglomerate->doCalcAtFinish();
         // Extend & copy model:
 #ifndef NDEBUG
         //checkSolution();
diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index aaf632c..9891684 100644
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,2 @@
 CryptoMiniSat
-GIT revision: 7aa24081ccebef355347957349c09b0c00fe5512
+GIT revision: 1d73485d3a23121ac2d9c5cf4732f0a914018fec