Fixing CMS2's library debug routine

It didn't work correctly when re-adding removed clauses: variable
elimination, conglomeration, and part-handling all dumped data, but they
shouldn't have been

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

diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp
index 18680519f47eb9233b0535cfcee12d06d200fee5..770c88acfe0612b3e65411aac53918238f4ac229 100644 (file)
--- a/src/sat/cryptominisat2/Conglomerate.cpp
+++ b/src/sat/cryptominisat2/Conglomerate.cpp
@@ -502,12 +502,15 @@ const bool Conglomerate::addRemovedClauses()
         for(Lit *l = c.getData(), *end2 = c.getDataEnd(); l != end2 ; l++)
             *l = l->unsign();
         
+        FILE* backup_libraryCNFfile = solver.libraryCNFFile;
+        solver.libraryCNFFile = NULL;
         if (!solver.addXorClause(c, c.xor_clause_inverted(), c.getGroup())) {
             for (;it != end; it++)
                 free(&c);
             calcAtFinish.clear();
             return false;
         }
+        solver.libraryCNFFile = backup_libraryCNFfile;
         free(&c);
     }
     calcAtFinish.clear();

diff --git a/src/sat/cryptominisat2/PartHandler.cpp b/src/sat/cryptominisat2/PartHandler.cpp
index c7f666ace59e16279c2756cf843953cd244992a3..c1773bd4f986df99a37f759db3e89957de582192 100644 (file)
--- a/src/sat/cryptominisat2/PartHandler.cpp
+++ b/src/sat/cryptominisat2/PartHandler.cpp
@@ -286,6 +286,8 @@ void PartHandler::addSavedState()
 
 void PartHandler::readdRemovedClauses()
 {
+    FILE* backup_libraryCNFfile = solver.libraryCNFFile;
+    solver.libraryCNFFile = NULL;
     for (Clause **it = clausesRemoved.getData(), **end = clausesRemoved.getDataEnd(); it != end; it++) {
         solver.addClause(**it, (*it)->getGroup());
         assert(solver.ok);
@@ -300,6 +302,7 @@ void PartHandler::readdRemovedClauses()
         assert(solver.ok);
     }
     xorClausesRemoved.clear();
+    solver.libraryCNFFile = backup_libraryCNFfile;
 }
 
 }; //NAMESPACE MINISAT

diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp
index 40152cd5cbafd68d6a7bcffe2af434c459a2f7a8..cf711e4439e5727ac8583d48495de4fea9872f20 100644 (file)
--- a/src/sat/cryptominisat2/Subsumer.cpp
+++ b/src/sat/cryptominisat2/Subsumer.cpp
@@ -90,12 +90,15 @@ const bool Subsumer::unEliminate(const Var var)
     solver.setDecisionVar(var, true);
     var_elimed[var] = false;
     numElimed--;
+    FILE* backup_libraryCNFfile = solver.libraryCNFFile;
+    solver.libraryCNFFile = NULL;
     for (vector<vector<Lit> >::iterator it2 = it->second.begin(), end2 = it->second.end(); it2 != end2; it2++) {
         tmp.clear();
         tmp.growTo(it2->size());
-        memcpy(tmp.getData(), &((*it2)[0]), sizeof(Lit)*it2->size());  //*it2 is never empty
+        std::copy(it2->begin(), it2->end(), tmp.getData());
         solver.addClause(tmp);
     }
+    solver.libraryCNFFile = backup_libraryCNFfile;
     elimedOutVar.erase(it);
     
     if (!solver.ok) return false;

diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index a01b800adaa1655e073d9db66d9b2d50626d2809..506910205a6482febd91c206661a227f0a8bf31e 100644 (file)
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,2 @@
 CryptoMiniSat
-GIT revision: cebb0caeb2928eb96e114864c580c341e904245d
+GIT revision: 8dccdf7df73e761aba7a8c9a0251e2327a9bd97c