From 1ed7e9aed374bf9974c45895ff528455af8be177 Mon Sep 17 00:00:00 2001 From: msoos Date: Wed, 21 Apr 2010 10:44:06 +0000 Subject: [PATCH] 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 --- src/sat/cryptominisat2/VERSION | 2 +- src/sat/cryptominisat2/VarReplacer.cpp | 31 +++++++---------- src/sat/cryptominisat2/VarReplacer.h | 2 +- src/sat/cryptominisat2/XorFinder.cpp | 46 ++++++++++++++++---------- src/sat/cryptominisat2/XorFinder.h | 1 + 5 files changed, 43 insertions(+), 39 deletions(-) diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 5069102..43593b7 100644 --- 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 e499ac4..261288e 100644 --- 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& cs, const bool isAttached) +const bool VarReplacer::replace_set(vec& cs) { XorClause **a = cs.getData(); XorClause **r = a; @@ -168,10 +163,9 @@ const bool VarReplacer::replace_set(vec& 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& 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 3669b84..1a6e7b7 100644 --- 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& set); - const bool replace_set(vec& cs, const bool isAttached); + const bool replace_set(vec& cs); const bool handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2); const bool handleUpdatedClause(XorClause& c, const Var origVar1, const Var origVar2); template diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp index 3c1e045..847a5af 100644 --- 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 7140a5c..f07190f 100644 --- a/src/sat/cryptominisat2/XorFinder.h +++ b/src/sat/cryptominisat2/XorFinder.h @@ -122,6 +122,7 @@ class XorFinder ClauseTable table; vector toRemove; + vector toLeaveInPlace; void clearToRemove(); uint32_t foundXors; -- 2.47.3