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 8a31895b74b22b39c975f83fe6966cdf3aa875e1..e8d4186f1e4dc6e3eea2edf1ece0f226da6213d0 100644 (file)
--- 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 69cca9b19c41180e07f8badbe9dda47d3202f32c..f44772afbc6366182986c5d61bdf3fa5fb1f092c 100644 (file)
--- 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 58626540fdc9e9afb1bfc91adf004fc6c470434a..06f3c04380aeb4039c914a9db42c1e7e6801d380 100644 (file)
--- 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 9e95bca5358d83b19f6ca69f40d4bc26039605bb..63218cb44dbe157df1a4778cf1be46a39946b0fd 100644 (file)
--- 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 e7cdd395b977ad7892f03a5cb34b3e06ca75c0af..5392d7bab3b600bd6871fb184314b5a47f6dbd4b 100644 (file)
--- 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