From: msoos Date: Mon, 7 Dec 2009 15:48:56 +0000 (+0000) Subject: Updating CryptoMiniSat to r565. Should solve the problem with performReplace failing... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=fe3320468ab07f542107eb16a55e2917a9ce3def;p=francis%2Fstp.git Updating CryptoMiniSat to r565. Should solve the problem with performReplace failing. It also brings a bit of speedup and a cleaner performReplace::replace_set() code for a cleaner (thus easier-to-debug) code git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@474 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp index 890a8ba..36d277e 100644 --- a/src/sat/cryptominisat2/ClauseCleaner.cpp +++ b/src/sat/cryptominisat2/ClauseCleaner.cpp @@ -119,8 +119,8 @@ void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type) if (c.size() == 2) { vec ps(2); - ps[0] = c[0]; - ps[1] = c[1]; + ps[0] = c[0].unsign(); + ps[1] = c[1].unsign(); solver.toReplace->replace(ps, c.xor_clause_inverted(), c.group); solver.removeClause(c); s++; diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp index f11cf4e..e71c9c4 100644 --- a/src/sat/cryptominisat2/Conglomerate.cpp +++ b/src/sat/cryptominisat2/Conglomerate.cpp @@ -79,11 +79,12 @@ void Conglomerate::fillVarToXor() } } -void Conglomerate::process_clause(XorClause& x, const uint num, uint var, vec& vars) { +void Conglomerate::process_clause(XorClause& x, const uint num, Var remove_var, vec& vars) { for (const Lit* a = &x[0], *end = a + x.size(); a != end; a++) { - if (a->var() != var) { - vars.push(*a); - varToXorMap::iterator finder = varToXor.find(a->var()); + Var var = a->var(); + if (var != remove_var) { + vars.push(Lit(var, false)); + varToXorMap::iterator finder = varToXor.find(var); if (finder != varToXor.end()) { vector >::iterator it = std::find(finder->second.begin(), finder->second.end(), make_pair(&x, num)); diff --git a/src/sat/cryptominisat2/Conglomerate.h b/src/sat/cryptominisat2/Conglomerate.h index 4193fce..d0eeb7c 100644 --- a/src/sat/cryptominisat2/Conglomerate.h +++ b/src/sat/cryptominisat2/Conglomerate.h @@ -33,7 +33,7 @@ public: private: - void process_clause(XorClause& x, const uint num, uint var, vec& vars); + void process_clause(XorClause& x, const uint num, Var remove_var, vec& vars); void fillVarToXor(); void clearDouble(vec& ps) const; void clearToRemove(); diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index 8813176..d8c5a3c 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -376,6 +376,18 @@ void Solver::detachModifiedClause(const Lit lit1, const Lit lit2, const uint ori else clauses_literals -= origSize; } +void Solver::detachModifiedClause(const Var var1, const Var var2, const uint origSize, const XorClause* address) +{ + assert(origSize > 2); + + assert(find(xorwatches[var1], address)); + assert(find(xorwatches[var2], address)); + remove(xorwatches[var1], address); + remove(xorwatches[var2], address); + if (address->learnt()) learnts_literals -= origSize; + else clauses_literals -= origSize; +} + // Revert to the state at given level (keeping all assignment at 'level' but not beyond). // void Solver::cancelUntil(int level) diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 3c16fde..65a0752 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -273,6 +273,7 @@ protected: void detachClause (const XorClause& c); void detachClause (const Clause& c); // Detach a clause to watcher lists. void detachModifiedClause(const Lit lit1, const Lit lit2, const uint size, const Clause* address); + void detachModifiedClause(const Var var1, const Var var2, const uint origSize, const XorClause* address); void removeClause(Clause& c); // Detach and free a clause. void removeClause(XorClause& c); // Detach and free a clause. bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state. diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 3771163..b18870e 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,3 +1,3 @@ CryptoMiniSat -SVN revision: 561 -GIT revision: 56d0a713979afbe737a7da1670f39eaf8c6f53a5 +SVN revision: 565 +GIT revision: a83e40474c31b7a0b902addfc37ff99a188d0ad3 diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index 0da1bec..62d840d 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -5,6 +5,7 @@ #include "ClauseCleaner.h" //#define VERBOSE_DEBUG +//#define DEBUG_REPLACER #ifdef VERBOSE_DEBUG #include @@ -42,6 +43,16 @@ void VarReplacer::performReplace() } #endif + S->clauseCleaner->removeSatisfied(S->clauses, ClauseCleaner::clauses); + S->clauseCleaner->removeSatisfied(S->learnts, ClauseCleaner::learnts); + S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses); + + S->clauseCleaner->cleanClauses(S->clauses, ClauseCleaner::clauses); + S->clauseCleaner->cleanClauses(S->learnts, ClauseCleaner::learnts); + S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses); + + if (!addedNewClause || replacedVars == 0) return; + uint i = 0; const vector& removedVars = S->conglomerate->getRemovedVars(); for (vector::const_iterator it = table.begin(); it != table.end(); it++, i++) { @@ -50,19 +61,6 @@ void VarReplacer::performReplace() if (!removedVars[it->var()]) S->setDecisionVar(it->var(), true); } - - if (!addedNewClause || replacedVars == 0) return; - - S->clauseCleaner->removeSatisfied(S->clauses, ClauseCleaner::clauses); - S->clauseCleaner->removeSatisfied(S->learnts, ClauseCleaner::learnts); - S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses); - - S->clauseCleaner->cleanClauses(S->clauses, ClauseCleaner::clauses); - S->clauseCleaner->cleanClauses(S->learnts, ClauseCleaner::learnts); - S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses); - for (uint i = 0; i < clauses.size(); i++) - S->removeClause(*clauses[i]); - clauses.clear(); replace_set(S->clauses); replace_set(S->learnts); @@ -70,6 +68,10 @@ void VarReplacer::performReplace() replace_set(S->xorclauses, true); replace_set(S->conglomerate->getCalcAtFinish(), false); + for (uint i = 0; i < clauses.size(); i++) + S->removeClause(*clauses[i]); + clauses.clear(); + if (S->verbosity >=1) printf("| Replacing %8d vars, replaced %8d lits |\n", replacedVars, replacedLits); @@ -81,68 +83,29 @@ void VarReplacer::performReplace() S->order_heap.filter(Solver::VarFilter(*S)); } -void VarReplacer::replace_set(vec& cs, const bool need_reattach) +void VarReplacer::replace_set(vec& cs, const bool isAttached) { XorClause **a = cs.getData(); XorClause **r = a; for (XorClause **end = a + cs.size(); r != end;) { XorClause& c = **r; - bool needReattach = false; + bool changed = false; + Var origVar1 = c[0].var(); + Var origVar2 = c[1].var(); for (Lit *l = &c[0], *lend = l + c.size(); l != lend; l++) { Lit newlit = table[l->var()]; if (newlit.var() != l->var()) { - if (need_reattach && !needReattach) - S->detachClause(c); - needReattach = true; + changed = true; *l = Lit(newlit.var(), false); c.invert(newlit.sign()); replacedLits++; } } - if (need_reattach && needReattach) { - std::sort(c.getData(), c.getData() + c.size()); - Lit p; - int i, j; - for (i = j = 0, p = lit_Undef; i < c.size(); i++) { - c[i] = c[i].unsign(); - if (c[i] == p) { - //added, but easily removed - j--; - p = lit_Undef; - if (!S->assigns[c[i].var()].isUndef()) - c.invert(S->assigns[c[i].var()].getBool()); - } else if (S->assigns[c[i].var()].isUndef()) //just add - c[j++] = p = c[i]; - else c.invert(S->assigns[c[i].var()].getBool()); //modify xor_clause_inverted instead of adding - } - c.shrink(i - j); - - switch (c.size()) { - case 0: - if (!c.xor_clause_inverted()) - S->ok = false; - r++; - break; - case 1: - S->uncheckedEnqueue(c[0] ^ c.xor_clause_inverted()); - r++; - break; - case 2: { - vec ps(2); - ps[0] = c[0]; - ps[1] = c[1]; - addBinaryXorClause(ps, c.xor_clause_inverted(), c.group, true); - c.mark(1); - r++; - break; - } - default: - S->attachClause(c); - *a++ = *r++; - break; - } + if (isAttached && changed && handleUpdatedClause(c, origVar1, origVar2)) { + c.mark(1); + r++; } else { *a++ = *r++; } @@ -150,6 +113,56 @@ void VarReplacer::replace_set(vec& cs, const bool need_reattach) cs.shrink(r-a); } +const bool VarReplacer::handleUpdatedClause(XorClause& c, const Var origVar1, const Var origVar2) +{ + uint origSize = c.size(); + std::sort(c.getData(), c.getData() + c.size()); + Lit p; + int i, j; + for (i = j = 0, p = lit_Undef; i < c.size(); i++) { + c[i] = c[i].unsign(); + if (c[i] == p) { + //added, but easily removed + j--; + p = lit_Undef; + if (!S->assigns[c[i].var()].isUndef()) + c.invert(S->assigns[c[i].var()].getBool()); + } else if (S->assigns[c[i].var()].isUndef()) //just add + c[j++] = p = c[i]; + else c.invert(S->assigns[c[i].var()].getBool()); //modify xor_clause_inverted instead of adding + } + c.shrink(i - j); + + switch (c.size()) { + case 0: + S->detachModifiedClause(origVar1, origVar2, origSize, &c); + if (!c.xor_clause_inverted()) + S->ok = false; + return true; + case 1: + S->detachModifiedClause(origVar1, origVar2, origSize, &c); + S->uncheckedEnqueue(c[0] ^ c.xor_clause_inverted()); + return true; + case 2: { + S->detachModifiedClause(origVar1, origVar2, origSize, &c); + vec ps(2); + ps[0] = c[0]; + ps[1] = c[1]; + addBinaryXorClause(ps, c.xor_clause_inverted(), c.group, true); + return true; + } + default: + if (origVar1 != c[0].var() || origVar2 != c[1].var()) { + S->detachModifiedClause(origVar1, origVar2, origSize, &c); + S->attachClause(c); + } + return false; + } + + assert(false); + return false; +} + void VarReplacer::replace_set(vec& cs) { Clause **a = cs.getData(); @@ -177,7 +190,7 @@ void VarReplacer::replace_set(vec& cs) cs.shrink(r-a); } -bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2) +const bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2) { bool satisfied = false; std::sort(c.getData(), c.getData() + c.size()); @@ -205,8 +218,8 @@ bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const Lit o S->ok = false; return true; case 1 : - S->uncheckedEnqueue(c[0]); S->detachModifiedClause(origLit1, origLit2, origSize, &c); + S->uncheckedEnqueue(c[0]); return true; case 2: S->detachModifiedClause(origLit1, origLit2, origSize, &c); @@ -219,6 +232,9 @@ bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const Lit o } return false; } + + assert(false); + return false; } const uint VarReplacer::getNumReplacedLits() const @@ -276,6 +292,19 @@ void VarReplacer::extendModel() const void VarReplacer::replace(vec& ps, const bool xor_clause_inverted, const uint group) { + #ifdef VERBOSE_DEBUG + cout << "replace() called with var " << ps[0]+1 << " and var " << ps[1]+1 << " with xor_clause_inverted " << xor_clause_inverted << endl; + #endif + + #ifdef DEBUG_REPLACER + assert(ps.size() == 2); + assert(!ps[0].sign()); + assert(!ps[1].sign()); + assert(S->assigns[ps[0].var()].isUndef()); + assert(S->assigns[ps[1].var()].isUndef()); + #endif + + addBinaryXorClause(ps, xor_clause_inverted, group); Var var = ps[0].var(); Lit lit = Lit(ps[1].var(), !xor_clause_inverted); @@ -340,9 +369,12 @@ void VarReplacer::replace(vec& ps, const bool xor_clause_inverted, const ui void VarReplacer::addBinaryXorClause(vec& ps, const bool xor_clause_inverted, const uint group, const bool internal) { + #ifdef DEBUG_REPLACER + assert(!ps[0].sign()); + assert(!ps[1].sign()); + #endif + Clause* c; - ps[0] = ps[0].unsign(); - ps[1] = ps[1].unsign(); ps[0] ^= xor_clause_inverted; c = Clause_new(ps, group, false); diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h index e6c8917..6739304 100644 --- a/src/sat/cryptominisat2/VarReplacer.h +++ b/src/sat/cryptominisat2/VarReplacer.h @@ -35,8 +35,9 @@ class VarReplacer private: void replace_set(vec& set); - void replace_set(vec& cs, const bool need_reattach); - bool handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2); + void replace_set(vec& cs, const bool isAttached); + const bool handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2); + const bool handleUpdatedClause(XorClause& c, const Var origVar1, const Var origVar2); void addBinaryXorClause(vec& ps, const bool xor_clause_inverted, const uint group, const bool internal = false); void setAllThatPointsHereTo(const Var var, const Lit lit);