CMS2 update: Extending the conglomerated clauses was done too early. Also, some non...

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 ee986c3fd2653a181b8080007afcf3bf9a643d67..552b2a8147a7b65f9f1ae70c79a1d743595cc78b 100644 (file)
--- 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 aaf632c3ddff62d44804981134419363d845ac4e..9891684c5d96e231660db62fa42ffc34976f6b6c 100644 (file)
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,2 @@
 CryptoMiniSat
-GIT revision: 7aa24081ccebef355347957349c09b0c00fe5512
+GIT revision: 1d73485d3a23121ac2d9c5cf4732f0a914018fec