From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 2 Dec 2009 16:27:28 +0000 (+0000)
Subject: Updating CryptoMiniSat2 to r504, fixing all known bugs
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=00502658d5008034231dd182b60a3be35c1d6ce6;p=francis%2Fstp.git

Updating CryptoMiniSat2 to r504, fixing all known bugs

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

diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index 8a31895..e8d4186 100644
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -175,6 +175,7 @@ bool Solver::addXorClause(vec<Lit>& ps, bool xor_clause_inverted, const uint gro
     Lit p;
     int i, j;
     for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
+        ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
         xor_clause_inverted ^= ps[i].sign();
         ps[i] ^= ps[i].sign();
 
@@ -250,6 +251,7 @@ bool Solver::addClause(vec<Lit>& ps, const uint group, char* group_name)
     Lit p;
     int i, j;
     for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
+        ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
         if (value(ps[i]) == l_True || ps[i] == ~p)
             return true;
         else if (value(ps[i]) != l_False && ps[i] != p)
@@ -1631,7 +1633,8 @@ next:
 
     assert(!failed);
 
-    printf("Verified %d clauses.\n", clauses.size() + xorclauses.size() + conglomerate->getCalcAtFinish().size());
+    if (verbosity >=1)
+        printf("Verified %d clauses.\n", clauses.size() + xorclauses.size() + conglomerate->getCalcAtFinish().size());
 }
 
 
diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index 69cca9b..f44772a 100644
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,4 +1,4 @@
 CryptoMiniSat
-SVN revision: r494
-GIT revision: eb7c71aaf2cea3bf064270d227cf7ddf27b852f2
+SVN revision: 504
+GIT revision: 4f460459f42a5fd33d971a19f9c206985a73c40d
 
diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp
index 5862654..06f3c04 100644
--- a/src/sat/cryptominisat2/VarReplacer.cpp
+++ b/src/sat/cryptominisat2/VarReplacer.cpp
@@ -22,6 +22,12 @@ VarReplacer::VarReplacer(Solver *_S) :
 {
 }
 
+VarReplacer::~VarReplacer()
+{
+    for (uint i = 0; i < toRemove.size(); i++)
+        free(toRemove[i]);
+}
+
 void VarReplacer::performReplace()
 {
     #ifdef VERBOSE_DEBUG
diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h
index 9e95bca..63218cb 100644
--- a/src/sat/cryptominisat2/VarReplacer.h
+++ b/src/sat/cryptominisat2/VarReplacer.h
@@ -21,6 +21,7 @@ class VarReplacer
 {
     public:
         VarReplacer(Solver* S);
+        ~VarReplacer();
         void replace(vec<Lit>& ps, const bool xor_clause_inverted, const uint group);
         void extendModel() const;
         void performReplace();
diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp
index e7cdd39..5392d7b 100644
--- a/src/sat/cryptominisat2/XorFinder.cpp
+++ b/src/sat/cryptominisat2/XorFinder.cpp
@@ -175,7 +175,8 @@ uint XorFinder::findXors(uint& sumLengths)
         cout << "- Found clauses:" << endl;
         #endif
         
-        for (ClauseTable::iterator it = begin; it != end; it++) {
+        for (ClauseTable::iterator it = begin; it != end; it++)
+            if (impairSigns(*it->first) == impair){
             #ifdef VERBOSE_DEBUG
             it->first->plain_print();
             #endif