Updating CMS2 to correct destructor segfault

XorFinder left the state in an unstable manner when UNSAT was found this
later lead to a segfault when trying to destruct the solver. Fixed.

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

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

diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp
index e499ac45cab2653c580e548d625ef18da4f3608e..261288ec8cfe983ee4d92e55c65012c6472f4a31 100644 (file)
--- a/src/sat/cryptominisat2/VarReplacer.cpp
+++ b/src/sat/cryptominisat2/VarReplacer.cpp
@@ -75,12 +75,8 @@ const bool VarReplacer::performReplaceInternal()
     }*/
     #endif //REPLACE_STATISTICS
     
-    solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses);
-    solver.clauseCleaner->cleanClauses(solver.learnts, ClauseCleaner::learnts);
-    solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses);
-    solver.clauseCleaner->removeSatisfied(solver.binaryClauses, ClauseCleaner::binaryClauses);
-    if (solver.ok == false)
-        return false;
+    solver.clauseCleaner->removeAndCleanAll(true);
+    if (solver.ok == false) return false;
     
     #ifdef VERBOSE_DEBUG
     {
@@ -123,19 +119,18 @@ const bool VarReplacer::performReplaceInternal()
     
     lastReplacedVars = replacedVars;
     
-    if (!replace_set(solver.clauses)) return false;
-    if (!replace_set(solver.learnts)) return false;
-    if (!replace_set(solver.binaryClauses)) return false;
-    
-    if (!replace_set(solver.xorclauses, true)) return false;
-    if (!replace_set(solver.conglomerate->getCalcAtFinish(), false)) return false;
+    if (!replace_set(solver.clauses)) goto end;
+    if (!replace_set(solver.learnts)) goto end;
+    if (!replace_set(solver.binaryClauses)) goto end;
+    if (!replace_set(solver.xorclauses)) goto end;
     
+end:
     for (uint i = 0; i != clauses.size(); i++)
         solver.removeClause(*clauses[i]);
     clauses.clear();
     
     if (solver.verbosity >= 2) {
-        std::cout << "     Replaced " <<  std::setw(8) << replacedLits<< " lits"
+        std::cout << "c |  Replaced " <<  std::setw(8) << replacedLits<< " lits"
         << "     Time: " << std::setw(8) << std::fixed << std::setprecision(2) << cpuTime()-time << " s "
         << std::setw(12) <<  " |" << std::endl;
     }
@@ -147,7 +142,7 @@ const bool VarReplacer::performReplaceInternal()
     return solver.ok;
 }
 
-const bool VarReplacer::replace_set(vec<XorClause*>& cs, const bool isAttached)
+const bool VarReplacer::replace_set(vec<XorClause*>& cs)
 {
     XorClause **a = cs.getData();
     XorClause **r = a;
@@ -168,10 +163,9 @@ const bool VarReplacer::replace_set(vec<XorClause*>& cs, const bool isAttached)
             }
         }
         
-        if (isAttached && changed && handleUpdatedClause(c, origVar1, origVar2)) {
+        if (changed && handleUpdatedClause(c, origVar1, origVar2)) {
             if (solver.ok == false) {
-                for(;r != end; r++)
-                    free(*r);
+                for(;r != end; r++) free(*r);
                 cs.shrink(r-a);
                 return false;
             }
@@ -259,8 +253,7 @@ const bool VarReplacer::replace_set(vec<Clause*>& cs)
         
         if (changed && handleUpdatedClause(c, origLit1, origLit2)) {
             if (solver.ok == false) {
-                for(;r != end; r++)
-                    free(*r);
+                for(;r != end; r++) free(*r);
                 cs.shrink(r-a);
                 return false;
             }

diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h
index 3669b8413e1452bf9574aae4d4b1744c64a80a32..1a6e7b75ca3ecf284ae0dcffcad43a1b5025ac22 100644 (file)
--- a/src/sat/cryptominisat2/VarReplacer.h
+++ b/src/sat/cryptominisat2/VarReplacer.h
@@ -67,7 +67,7 @@ class VarReplacer
         const bool performReplaceInternal();
         
         const bool replace_set(vec<Clause*>& set);
-        const bool replace_set(vec<XorClause*>& cs, const bool isAttached);
+        const bool replace_set(vec<XorClause*>& cs);
         const bool handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2);
         const bool handleUpdatedClause(XorClause& c, const Var origVar1, const Var origVar2);
         template<class T>

diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp
index 3c1e045f5793aa5532a69206b8ff0de22513a8e6..847a5af40308e8b467375a867e4eb22e5b825126 100644 (file)
--- a/src/sat/cryptominisat2/XorFinder.cpp
+++ b/src/sat/cryptominisat2/XorFinder.cpp
@@ -60,6 +60,8 @@ const bool XorFinder::doNoPart(const uint minSize, const uint maxSize)
     
     toRemove.clear();
     toRemove.resize(cls.size(), false);
+    toLeaveInPlace.clear();
+    toLeaveInPlace.resize(cls.size(), false);
     
     table.clear();
     table.reserve(cls.size());
@@ -94,7 +96,10 @@ const bool XorFinder::doNoPart(const uint minSize, const uint maxSize)
     uint i = 0;
     for (Clause **it = cls.getData(), **end = it + cls.size(); it != end; it++, i++) {
         const uint size = (*it)->size();
-        if ( size > maxSize || size < minSize) continue;
+        if ( size > maxSize || size < minSize) {
+            toLeaveInPlace[i] = true;
+            continue;
+        }
         if ((*it)->getSorted()) sortedTable.push_back(make_pair(*it, i));
         else unsortedTable.push_back(make_pair(*it, i));
     }
@@ -134,9 +139,10 @@ const bool XorFinder::doNoPart(const uint minSize, const uint maxSize)
     }
     #endif //DEBUG_XORFIND
     
-    if (findXors(sumLengths) == false)
-        return false;
+    if (findXors(sumLengths) == false) goto end;
+    S->ok = (S->propagate() == NULL);
     
+end:
     if (S->verbosity >= 2) {
         if (minSize == maxSize && minSize == 2)
             printf("c |  Finding binary XORs:        %5.2lf s (found: %7d, avg size: %3.1lf)                  |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors);
@@ -144,20 +150,25 @@ const bool XorFinder::doNoPart(const uint minSize, const uint maxSize)
             printf("c |  Finding non-binary XORs:    %5.2lf s (found: %7d, avg size: %3.1lf)                  |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors);
     }
     
-    if (type == ClauseCleaner::binaryClauses) {
-        i = 0;
-        uint j = 0;
-        for (uint size = table.size(); i != size; i++) {
-            if (!toRemove[table[i].second]) {
-                table[i].first->setSorted();
-                cls[j++] = table[i].first;
-            }
+    i = 0;
+    uint32_t j = 0;
+    uint32_t toSkip = 0;
+    for (uint end = cls.size(); i != end; i++) {
+        if (toLeaveInPlace[i]) {
+            cls[j] = cls[i];
+            j++;
+            toSkip++;
+            continue;
+        }
+        if (!toRemove[table[i-toSkip].second]) {
+            table[i-toSkip].first->setSorted();
+            cls[j] = table[i-toSkip].first;
+            j++;
         }
-        cls.shrink(i-j);
-    } else if (foundXors > 0)
-        clearToRemove();
+    }
+    cls.shrink(i-j);
     
-    return S->ok = (S->propagate() == NULL);
+    return S->ok;
 }
 
 const bool XorFinder::findXors(uint& sumLengths)
@@ -195,8 +206,7 @@ const bool XorFinder::findXors(uint& sumLengths)
         
         switch(lits.size()) {
         case 2: {
-            if (S->varReplacer->replace(lits, impair, old_group) == false)
-                return false;
+            S->varReplacer->replace(lits, impair, old_group);
             
             #ifdef VERBOSE_DEBUG
             XorClause* x = XorClause_new(lits, impair, old_group);
@@ -222,7 +232,7 @@ const bool XorFinder::findXors(uint& sumLengths)
         sumLengths += lits.size();
     }
     
-    return true;
+    return S->ok;
 }
 
 void XorFinder::clearToRemove()

diff --git a/src/sat/cryptominisat2/XorFinder.h b/src/sat/cryptominisat2/XorFinder.h
index 7140a5cf7f894f6ee187dd2c39405538ea8943c9..f07190f556615efc88542f2d93cff071cebda051 100644 (file)
--- a/src/sat/cryptominisat2/XorFinder.h
+++ b/src/sat/cryptominisat2/XorFinder.h
@@ -122,6 +122,7 @@ class XorFinder
         
         ClauseTable table;
         vector<bool> toRemove;
+        vector<bool> toLeaveInPlace;
         void clearToRemove();
         uint32_t foundXors;