From 892b28bbe956280f9867ab9da1d14d88b65ace4a Mon Sep 17 00:00:00 2001 From: msoos Date: Sun, 6 Dec 2009 17:28:40 +0000 Subject: [PATCH] Updating CryptoMiniSat to SVN r561, fixing a log of bugs git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@466 e59a4935-1847-0410-ae03-e826735625c1 --- src/sat/cryptominisat2/ClauseCleaner.cpp | 165 ++++++++++++++++++++++ src/sat/cryptominisat2/ClauseCleaner.h | 51 +++++++ src/sat/cryptominisat2/Conglomerate.cpp | 76 ++++++++-- src/sat/cryptominisat2/Conglomerate.h | 6 + src/sat/cryptominisat2/Gaussian.cpp | 5 +- src/sat/cryptominisat2/GaussianConfig.h | 4 +- src/sat/cryptominisat2/Logger.cpp | 1 + src/sat/cryptominisat2/Makefile | 2 +- src/sat/cryptominisat2/MatrixFinder.cpp | 12 +- src/sat/cryptominisat2/PackedRow.cpp | 2 - src/sat/cryptominisat2/PackedRow.h | 2 - src/sat/cryptominisat2/Solver.cpp | 168 +++++------------------ src/sat/cryptominisat2/Solver.h | 27 +--- src/sat/cryptominisat2/VERSION | 5 +- src/sat/cryptominisat2/VarReplacer.cpp | 83 ++++++----- src/sat/cryptominisat2/VarReplacer.h | 4 +- src/sat/cryptominisat2/XorFinder.cpp | 2 + 17 files changed, 400 insertions(+), 215 deletions(-) create mode 100644 src/sat/cryptominisat2/ClauseCleaner.cpp create mode 100644 src/sat/cryptominisat2/ClauseCleaner.h diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp new file mode 100644 index 0000000..890a8ba --- /dev/null +++ b/src/sat/cryptominisat2/ClauseCleaner.cpp @@ -0,0 +1,165 @@ +#include "ClauseCleaner.h" + +namespace MINISAT +{ +using namespace MINISAT; + +ClauseCleaner::ClauseCleaner(Solver& _solver) : + solver(_solver) +{ + for (uint i = 0; i < 4; i++) { + lastNumUnitarySat[i] = solver.get_unitary_learnts_num(); + lastNumUnitaryClean[i] = solver.get_unitary_learnts_num(); + } +} + +void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type) +{ + if (lastNumUnitarySat[type] == solver.get_unitary_learnts_num()) + return; + + int i,j; + for (i = j = 0; i < cs.size(); i++) { + if (satisfied(*cs[i])) + solver.removeClause(*cs[i]); + else + cs[j++] = cs[i]; + } + cs.shrink(i - j); + + lastNumUnitarySat[type] = solver.get_unitary_learnts_num(); +} + +void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type) +{ + if (lastNumUnitarySat[type] == solver.get_unitary_learnts_num()) + return; + + int i,j; + for (i = j = 0; i < cs.size(); i++) { + if (satisfied(*cs[i])) + solver.removeClause(*cs[i]); + else + cs[j++] = cs[i]; + } + cs.shrink(i - j); + + lastNumUnitarySat[type] = solver.get_unitary_learnts_num(); +} + +bool ClauseCleaner::cleanClause(Clause& c) +{ + assert(c.size() >= 2); + Lit first = c[0]; + Lit second = c[1]; + + Lit *i, *j, *end; + uint at = 0; + for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) { + if (solver.value(*i) == l_Undef) { + *j = *i; + j++; + } else assert(at > 1); + assert(solver.value(*i) != l_True); + } + if ((c.size() > 2) && (c.size() - (i-j) == 2)) { + solver.detachModifiedClause(first, second, c.size(), &c); + c.shrink(i-j); + solver.attachClause(c); + } else + c.shrink(i-j); + + assert(c.size() > 1); + + return (i-j > 0); +} + +void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type) +{ + if (lastNumUnitaryClean[type] == solver.get_unitary_learnts_num()) + return; + + uint useful = 0; + for (int s = 0; s < cs.size(); s++) + useful += cleanClause(*cs[s]); + + lastNumUnitaryClean[type] = solver.get_unitary_learnts_num(); + + #ifdef VERBOSE_DEBUG + cout << "cleanClauses(Clause) useful:" << useful << endl; + #endif +} + +void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type) +{ + if (lastNumUnitaryClean[type] == solver.get_unitary_learnts_num()) + return; + + uint useful = 0; + XorClause **s, **ss, **end; + for (s = ss = cs.getData(), end = s + cs.size(); s != end;) { + XorClause& c = **s; + #ifdef VERBOSE_DEBUG + std::cout << "Cleaning clause:"; + c.plain_print(); + solver.printClause(c);std::cout << std::endl; + #endif + + Lit *i, *j, *end; + uint at = 0; + for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) { + const lbool& val = solver.assigns[i->var()]; + if (val.isUndef()) { + *j = *i; + j++; + } else /*assert(at>1),*/ c.invert(val.getBool()); + } + c.shrink(i-j); + if (i-j > 0) useful++; + + if (c.size() == 2) { + vec ps(2); + ps[0] = c[0]; + ps[1] = c[1]; + solver.toReplace->replace(ps, c.xor_clause_inverted(), c.group); + solver.removeClause(c); + s++; + } else + *ss++ = *s++; + + #ifdef VERBOSE_DEBUG + std::cout << "Cleaned clause:"; + c.plain_print(); + solver.printClause(c);std::cout << std::endl; + #endif + assert(c.size() > 1); + } + cs.shrink(s-ss); + + lastNumUnitaryClean[type] = solver.get_unitary_learnts_num(); + + #ifdef VERBOSE_DEBUG + cout << "cleanClauses(XorClause) useful:" << useful << endl; + #endif +} + +bool ClauseCleaner::satisfied(const Clause& c) const +{ + for (uint i = 0; i < c.size(); i++) + if (solver.value(c[i]) == l_True) + return true; + return false; +} + +bool ClauseCleaner::satisfied(const XorClause& c) const +{ + bool final = c.xor_clause_inverted(); + for (uint k = 0; k < c.size(); k++ ) { + const lbool& val = solver.assigns[c[k].var()]; + if (val.isUndef()) return false; + final ^= val.getBool(); + } + return final; +} + +}; diff --git a/src/sat/cryptominisat2/ClauseCleaner.h b/src/sat/cryptominisat2/ClauseCleaner.h new file mode 100644 index 0000000..f9a66d1 --- /dev/null +++ b/src/sat/cryptominisat2/ClauseCleaner.h @@ -0,0 +1,51 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#ifndef CLAUSECLEANER_H +#define CLAUSECLEANER_H + +#include "Solver.h" + +namespace MINISAT +{ + +class ClauseCleaner +{ + public: + ClauseCleaner(Solver& solver); + + enum ClauseSetType {clauses, xorclauses, learnts, conglomerate}; + + void cleanClauses(vec& cs, ClauseSetType type); + void cleanClauses(vec& cs, ClauseSetType type); + void removeSatisfied(vec& cs, ClauseSetType type); + void removeSatisfied(vec& cs, ClauseSetType type); + bool satisfied(const Clause& c) const; + bool satisfied(const XorClause& c) const; + + private: + bool cleanClause(Clause& c); + + uint lastNumUnitarySat[4]; + uint lastNumUnitaryClean[4]; + + Solver& solver; +}; + +}; + +#endif //CLAUSECLEANER_H diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp index 27f019b..f11cf4e 100644 --- a/src/sat/cryptominisat2/Conglomerate.cpp +++ b/src/sat/cryptominisat2/Conglomerate.cpp @@ -1,6 +1,7 @@ #include "Conglomerate.h" #include "Solver.h" #include "VarReplacer.h" +#include "ClauseCleaner.h" #include #include @@ -29,6 +30,11 @@ Conglomerate::~Conglomerate() free(calcAtFinish[i]); } +const vector& Conglomerate::getRemovedVars() const +{ + return removedVars; +} + const vec& Conglomerate::getCalcAtFinish() const { return calcAtFinish; @@ -55,8 +61,8 @@ void Conglomerate::fillVarToXor() for (Lit* it = &(S->trail[0]), *end = it + S->trail.size(); it != end; it++) blocked[it->var()] = true; - const vec& tmp = S->toReplace->getToRemove(); - for (Clause *const*it = tmp.getData(), *const*end = it + tmp.size(); it != end; it++) { + const vec& clauses = S->toReplace->getClauses(); + for (Clause *const*it = clauses.getData(), *const*end = it + clauses.size(); it != end; it++) { const Clause& c = **it; for (const Lit* a = &c[0], *end = a + c.size(); a != end; a++) { blocked[a->var()] = true; @@ -91,15 +97,16 @@ uint Conglomerate::conglomerateXors() { if (S->xorclauses.size() == 0) return 0; - toRemove.clear(); - toRemove.resize(S->xorclauses.size(), false); #ifdef VERBOSE_DEBUG cout << "Finding conglomerate xors started" << endl; #endif - S->removeSatisfied(S->xorclauses); - S->cleanClauses(S->xorclauses); + S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses); + S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses); + + toRemove.clear(); + toRemove.resize(S->xorclauses.size(), false); fillVarToXor(); @@ -116,6 +123,7 @@ uint Conglomerate::conglomerateXors() } S->setDecisionVar(var, false); + removedVars[var] = true; if (c.size() == 0) { varToXor.erase(it); @@ -263,16 +271,48 @@ void Conglomerate::clearDouble(vec& ps) const void Conglomerate::clearToRemove() { + assert(toRemove.size() == S->xorclauses.size()); + XorClause **a = S->xorclauses.getData(); XorClause **r = a; XorClause **end = a + S->xorclauses.size(); for (uint i = 0; r != end; i++) { if (!toRemove[i]) *a++ = *r++; - else + else { + (**a).mark(1); r++; + } } S->xorclauses.shrink(r-a); + + clearLearntsFromToRemove(); +} + +void Conglomerate::clearLearntsFromToRemove() +{ + Clause **a = S->learnts.getData(); + Clause **r = a; + Clause **end = a + S->learnts.size(); + for (; r != end;) { + const Clause& c = **r; + bool inside = false; + if (!S->locked(c)) { + for (uint i = 0; i < c.size(); i++) { + if (removedVars[c[i].var()]) { + inside = true; + break; + } + } + } + if (!inside) + *a++ = *r++; + else { + S->removeClause(**r); + r++; + } + } + S->learnts.shrink(r-a); } void Conglomerate::doCalcAtFinish() @@ -309,14 +349,18 @@ void Conglomerate::doCalcAtFinish() } if (toAssign.size() > 1) { cout << "Double assign!" << endl; + for (uint i = 1; i < toAssign.size(); i++) { + cout << "-> extra Var " << toAssign[i]+1 << endl; + } } #endif assert(toAssign.size() > 0); for (uint i = 1; i < toAssign.size(); i++) { - S->uncheckedEnqueue(Lit(toAssign[i], false), &c); + S->uncheckedEnqueue(Lit(toAssign[i], true), &c); } S->uncheckedEnqueue(Lit(toAssign[0], final), &c); + assert(S->clauseCleaner->satisfied(c)); } } @@ -339,13 +383,23 @@ void Conglomerate::addRemovedClauses() ps.clear(); for(uint i2 = 0; i2 != c.size() ; i2++) { - ps.push(c[i2]); - S->setDecisionVar(c[i2].var(), true); + ps.push(Lit(c[i2].var(), false)); } - S->addXorClause(ps, c.xor_clause_inverted(), c.group, tmp); + S->addXorClause(ps, c.xor_clause_inverted(), c.group, tmp, true); free(&c); } calcAtFinish.clear(); + for (uint i = 0; i < removedVars.size(); i++) { + if (removedVars[i]) { + removedVars[i] = false; + S->setDecisionVar(i, true); + } + } +} + +void Conglomerate::newVar() +{ + removedVars.resize(removedVars.size()+1, false); } }; diff --git a/src/sat/cryptominisat2/Conglomerate.h b/src/sat/cryptominisat2/Conglomerate.h index 24efe74..4193fce 100644 --- a/src/sat/cryptominisat2/Conglomerate.h +++ b/src/sat/cryptominisat2/Conglomerate.h @@ -3,12 +3,14 @@ #include #include +#include #include "Clause.h" #include "VarReplacer.h" using std::vector; using std::pair; using std::map; +using std::set; class Solver; @@ -26,6 +28,8 @@ public: void doCalcAtFinish(); ///& getCalcAtFinish() const; vec& getCalcAtFinish(); + const vector& getRemovedVars() const; + void newVar(); private: @@ -33,12 +37,14 @@ private: void fillVarToXor(); void clearDouble(vec& ps) const; void clearToRemove(); + void clearLearntsFromToRemove(); bool dealWithNewClause(vec& ps, const bool inverted, const uint old_group); typedef map > > varToXorMap; varToXorMap varToXor; vector blocked; vector toRemove; + vector removedVars; vec calcAtFinish; diff --git a/src/sat/cryptominisat2/Gaussian.cpp b/src/sat/cryptominisat2/Gaussian.cpp index 3e82b8e..a4c6798 100644 --- a/src/sat/cryptominisat2/Gaussian.cpp +++ b/src/sat/cryptominisat2/Gaussian.cpp @@ -21,6 +21,7 @@ along with this program. If not, see . #include #include "Clause.h" #include +#include "ClauseCleaner.h" using std::ostream; using std::cout; using std::endl; @@ -81,8 +82,8 @@ llbool Gaussian::full_init() bool do_again_gauss = true; while (do_again_gauss) { do_again_gauss = false; - solver.removeSatisfied(solver.xorclauses); - solver.cleanClauses(solver.xorclauses); + solver.clauseCleaner->removeSatisfied(solver.xorclauses, ClauseCleaner::xorclauses); + solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses); init(); Clause* confl; gaussian_ret g = gaussian(confl); diff --git a/src/sat/cryptominisat2/GaussianConfig.h b/src/sat/cryptominisat2/GaussianConfig.h index cc60c80..1994f1a 100644 --- a/src/sat/cryptominisat2/GaussianConfig.h +++ b/src/sat/cryptominisat2/GaussianConfig.h @@ -34,13 +34,10 @@ class GaussianConfig , decision_until(0) , starts_from(3) { - if (PackedRow::tmp_row == NULL) - PackedRow::tmp_row = new uint64_t[1000]; } ~GaussianConfig() { - delete[] PackedRow::tmp_row; } //tuneable gauss parameters @@ -48,5 +45,6 @@ class GaussianConfig uint decision_until; //do Gauss until this level uint starts_from; //Gauss elimination starts from this restart number }; + }; #endif //GAUSSIANCONFIG_H diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp index a89b9f9..19f5a0b 100644 --- a/src/sat/cryptominisat2/Logger.cpp +++ b/src/sat/cryptominisat2/Logger.cpp @@ -871,4 +871,5 @@ void Logger::reset_statistics() branch_depth_distrib.clear(); learnt_unitary_clauses = 0; } + }; diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile index 6db1d0a..064dfea 100644 --- a/src/sat/cryptominisat2/Makefile +++ b/src/sat/cryptominisat2/Makefile @@ -2,7 +2,7 @@ include ../../../scripts/Makefile.common MTL = mtl MTRAND = MTRand -SOURCES = Conglomerate.cpp FindUndef.cpp Gaussian.cpp Logger.cpp MatrixFinder.cpp PackedRow.cpp Solver.cpp VarReplacer.cpp XorFinder.cpp +SOURCES = Conglomerate.cpp FindUndef.cpp Gaussian.cpp Logger.cpp MatrixFinder.cpp PackedRow.cpp Solver.cpp VarReplacer.cpp XorFinder.cpp ClauseCleaner.cpp OBJECTS = $(SOURCES:.cpp=.o) LIB = libminisat.a CFLAGS += -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c diff --git a/src/sat/cryptominisat2/MatrixFinder.cpp b/src/sat/cryptominisat2/MatrixFinder.cpp index d3847db..19c8ad6 100644 --- a/src/sat/cryptominisat2/MatrixFinder.cpp +++ b/src/sat/cryptominisat2/MatrixFinder.cpp @@ -20,6 +20,7 @@ along with this program. If not, see . #include "Solver.h" #include "Gaussian.h" #include "GaussianConfig.h" +#include "ClauseCleaner.h" #include #include @@ -44,8 +45,6 @@ MatrixFinder::MatrixFinder(Solver *_S) : unAssigned(_S->nVars() + 1) , S(_S) { - table.resize(S->nVars(), unAssigned); - matrix_no = 0; } inline const Var MatrixFinder::fingerprint(const XorClause& c) const @@ -75,11 +74,16 @@ inline const bool MatrixFinder::firstPartOfSecond(const XorClause& c1, const Xor const uint MatrixFinder::findMatrixes() { + table.clear(); + table.resize(S->nVars(), unAssigned); + reverseTable.clear(); + matrix_no = 0; + if (S->xorclauses.size() == 0) return 0; - S->removeSatisfied(S->xorclauses); - S->cleanClauses(S->xorclauses); + S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses); + S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses); for (XorClause** c = S->xorclauses.getData(), **end = c + S->xorclauses.size(); c != end; c++) { set tomerge; diff --git a/src/sat/cryptominisat2/PackedRow.cpp b/src/sat/cryptominisat2/PackedRow.cpp index b4f10a4..0689c0d 100644 --- a/src/sat/cryptominisat2/PackedRow.cpp +++ b/src/sat/cryptominisat2/PackedRow.cpp @@ -2,8 +2,6 @@ namespace MINISAT { -__thread uint64_t* PackedRow::tmp_row = NULL; - std::ostream& operator << (std::ostream& os, const PackedRow& m) { for(uint i = 0; i < m.size*64; i++) { diff --git a/src/sat/cryptominisat2/PackedRow.h b/src/sat/cryptominisat2/PackedRow.h index 01fa26e..cad82b3 100644 --- a/src/sat/cryptominisat2/PackedRow.h +++ b/src/sat/cryptominisat2/PackedRow.h @@ -142,8 +142,6 @@ public: } friend std::ostream& operator << (std::ostream& os, const PackedRow& m); - - static __thread uint64_t *tmp_row; private: friend class PackedMatrix; diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index 0cb5424..8813176 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -36,6 +36,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "MatrixFinder.h" #include "Conglomerate.h" #include "XorFinder.h" +#include "ClauseCleaner.h" //#define DEBUG_LIB @@ -98,6 +99,7 @@ Solver::Solver() : { toReplace = new VarReplacer(this); conglomerate = new Conglomerate(this); + clauseCleaner = new ClauseCleaner(*this); logger.setSolver(this); #ifdef DEBUG_LIB @@ -117,6 +119,7 @@ Solver::~Solver() for (uint i = 0; i < freeLater.size(); i++) free(freeLater[i]); delete toReplace; delete conglomerate; + delete clauseCleaner; #ifdef DEBUG_LIB fclose(myoutputfile); @@ -147,23 +150,30 @@ Var Solver::newVar(bool sign, bool dvar) decision_var.push_back(dvar); toReplace->newVar(); + conglomerate->newVar(); insertVarOrder(v); if (dynamic_behaviour_analysis) logger.new_var(v); + + #ifdef DEBUG_LIB + fprintf(myoutputfile, "c Solver::newVar() called\n"); + #endif //DEBUG_LIB return v; } -bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint group, char* group_name) +bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint group, char* group_name, const bool internal) { assert(decisionLevel() == 0); #ifdef DEBUG_LIB - fprintf(myoutputfile, "x"); - for (uint i = 0; i < ps.size(); i++) { - fprintf(myoutputfile, "%s%d ", ps[i].sign() ? "-" : "", ps[i].var()+1); + if (!internal) { + fprintf(myoutputfile, "x"); + for (uint i = 0; i < ps.size(); i++) { + fprintf(myoutputfile, "%s%d ", ps[i].sign() ? "-" : "", ps[i].var()+1); + } + fprintf(myoutputfile, "0\n"); } - fprintf(myoutputfile, "0\n"); #endif //DEBUG_LIB if (dynamic_behaviour_analysis) logger.set_group_name(group, group_name); @@ -222,7 +232,8 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro xorclauses.push(c); attachClause(*c); - toReplace->newClause(); + if (!internal) + toReplace->newClause(); break; } } @@ -365,27 +376,6 @@ void Solver::detachModifiedClause(const Lit lit1, const Lit lit2, const uint ori else clauses_literals -= origSize; } - -bool Solver::satisfied(const Clause& c) const -{ - for (uint i = 0; i < c.size(); i++) - if (value(c[i]) == l_True) - return true; - return false; -} - -bool Solver::satisfied(const XorClause& c) const -{ - bool final = c.xor_clause_inverted(); - for (uint k = 0; k < c.size(); k++ ) { - const lbool& val = assigns[c[k].var()]; - if (val.isUndef()) return false; - final ^= val.getBool(); - } - return final; -} - - // Revert to the state at given level (keeping all assignment at 'level' but not beyond). // void Solver::cancelUntil(int level) @@ -1060,88 +1050,6 @@ void Solver::setMaxRestarts(const uint num) maxRestarts = num; } -bool Solver::cleanClause(Clause& c) -{ - assert(c.size() >= 2); - Lit first = c[0]; - Lit second = c[1]; - - Lit *i, *j, *end; - uint at = 0; - for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) { - if (value(*i) == l_Undef) { - *j = *i; - j++; - } else assert(at > 1); - assert(value(*i) != l_True); - } - if ((c.size() > 2) && (c.size() - (i-j) == 2)) { - detachModifiedClause(first, second, c.size(), &c); - c.shrink(i-j); - attachClause(c); - } else - c.shrink(i-j); - return (i-j > 0); -} - -void Solver::cleanClauses(vec& cs) -{ - uint useful = 0; - for (int s = 0; s < cs.size(); s++) - useful += cleanClause(*cs[s]); - #ifdef VERBOSE_DEBUG - cout << "cleanClauses(Clause) useful:" << useful << endl; - #endif -} - -void Solver::cleanClauses(vec& cs) -{ - uint useful = 0; - XorClause **s, **ss, **end; - for (s = ss = cs.getData(), end = s + cs.size(); s != end;) { - XorClause& c = **s; - #ifdef VERBOSE_DEBUG - std::cout << "Cleaning clause:"; - c.plain_print(); - printClause(c);std::cout << std::endl; - #endif - - Lit *i, *j, *end; - uint at = 0; - for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) { - const lbool& val = assigns[i->var()]; - if (val.isUndef()) { - *j = *i; - j++; - } else /*assert(at>1),*/ c.invert(val.getBool()); - } - c.shrink(i-j); - if (i-j > 0) useful++; - - if (c.size() == 2) { - vec ps(2); - ps[0] = c[0]; - ps[1] = c[1]; - toReplace->replace(ps, c.xor_clause_inverted(), c.group); - removeClause(c); - s++; - } else - *ss++ = *s++; - - #ifdef VERBOSE_DEBUG - std::cout << "Cleaned clause:"; - c.plain_print(); - printClause(c);std::cout << std::endl; - #endif - assert(c.size() > 1); - } - cs.shrink(s-ss); - - #ifdef VERBOSE_DEBUG - cout << "cleanClauses(XorClause) useful:" << useful << endl; - #endif -} - /*_________________________________________________________________________________________________ | | simplify : [void] -> [bool] @@ -1167,10 +1075,10 @@ lbool Solver::simplify() } // Remove satisfied clauses: - removeSatisfied(learnts); + clauseCleaner->removeSatisfied(learnts, ClauseCleaner::learnts); if (remove_satisfied) { // Can be turned off. - removeSatisfied(clauses); - removeSatisfied(xorclauses); + clauseCleaner->removeSatisfied(clauses, ClauseCleaner::clauses); + clauseCleaner->removeSatisfied(xorclauses, ClauseCleaner::xorclauses); } // Remove fixed variables from the variable heap: @@ -1179,9 +1087,9 @@ lbool Solver::simplify() simpDB_assigns = nAssigns(); simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now) - //cleanClauses(clauses); - //cleanClauses(xorclauses); - //cleanClauses(learnts); + //clauseCleaner->cleanClauses(clauses); + //clauseCleaner->cleanClauses(xorclauses); + //clauseCleaner->cleanClauses(learnts); return l_Undef; } @@ -1451,8 +1359,8 @@ lbool Solver::solve(const vec& assumps) double time; if (clauses.size() < 400000) { time = cpuTime(); - removeSatisfied(clauses); - cleanClauses(clauses); + clauseCleaner->removeSatisfied(clauses, ClauseCleaner::clauses); + clauseCleaner->cleanClauses(clauses, ClauseCleaner::clauses); uint sumLengths = 0; XorFinder xorFinder(this, clauses); uint foundXors = xorFinder.doNoPart(sumLengths, 2, 10); @@ -1497,13 +1405,6 @@ lbool Solver::solve(const vec& assumps) } } - for (uint i = 0; i < gauss_matrixes.size(); i++) - delete gauss_matrixes[i]; - gauss_matrixes.clear(); - for (uint i = 0; i < freeLater.size(); i++) - free(freeLater[i]); - freeLater.clear(); - if (gaussconfig.decision_until > 0 && xorclauses.size() > 1 && xorclauses.size() < 20000) { double time = cpuTime(); MatrixFinder m(this); @@ -1525,13 +1426,13 @@ lbool Solver::solve(const vec& assumps) // Search: while (status == l_Undef && starts < maxRestarts) { - removeSatisfied(clauses); - removeSatisfied(xorclauses); - removeSatisfied(learnts); + clauseCleaner->removeSatisfied(clauses, ClauseCleaner::clauses); + clauseCleaner->removeSatisfied(xorclauses, ClauseCleaner::xorclauses); + clauseCleaner->removeSatisfied(learnts, ClauseCleaner::learnts); - cleanClauses(clauses); - cleanClauses(xorclauses); - cleanClauses(learnts); + clauseCleaner->cleanClauses(clauses, ClauseCleaner::clauses); + clauseCleaner->cleanClauses(xorclauses, ClauseCleaner::xorclauses); + clauseCleaner->cleanClauses(learnts, ClauseCleaner::learnts); if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) { printf("| %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nbclausesbeforereduce*curRestart, nLearnts(), (double)learnts_literals/nLearnts()); @@ -1550,6 +1451,13 @@ lbool Solver::solve(const vec& assumps) printf("===================================================================="); print_gauss_sum_stats(); } + + for (uint i = 0; i < gauss_matrixes.size(); i++) + delete gauss_matrixes[i]; + gauss_matrixes.clear(); + for (uint i = 0; i < freeLater.size(); i++) + free(freeLater[i]); + freeLater.clear(); if (status == l_True) { conglomerate->doCalcAtFinish(); diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 2769809..3c16fde 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -54,6 +54,7 @@ class Conglomerate; class VarReplacer; class XorFinder; class FindUndef; +class ClauseCleaner; //#define VERBOSE_DEBUG_XOR //#define VERBOSE_DEBUG @@ -80,7 +81,7 @@ public: // Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. bool addClause (vec& ps, const uint group, char* group_name); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! - bool addXorClause (vec& ps, bool xor_clause_inverted, const uint group, char* group_name); // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method! + bool addXorClause (vec& ps, bool xor_clause_inverted, const uint group, char* group_name, const bool internal = false); // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method! // Solving: // @@ -255,11 +256,6 @@ protected: bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') lbool search (int nof_conflicts); // Search for a given number of conflicts. void reduceDB (); // Reduce the set of learnt clauses. - template - void removeSatisfied (vec& cs); // Shrink 'cs' to contain only non-satisfied clauses. - void cleanClauses (vec& cs); - bool cleanClause (Clause& c); - void cleanClauses (vec& cs); // Remove TRUE or FALSE variables from the xor clauses and remove the FALSE variables from the normal clauses llbool handle_conflict (vec& learnt_clause, Clause* confl, int& conflictC);// Handles the conflict clause llbool new_decision (int& nof_conflicts, int& conflictC); // Handles the case when all propagations have been made, and now a decision must be made @@ -280,8 +276,6 @@ protected: 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. - bool satisfied (const XorClause& c) const; // Returns TRUE if the clause is satisfied in the current state - bool satisfied (const Clause& c) const; // Returns TRUE if the clause is satisfied in the current state. void reverse_binary_clause(Clause& c) const; // Binary clauses --- the first Lit has to be true // Misc: @@ -295,8 +289,10 @@ protected: friend class Conglomerate; friend class MatrixFinder; friend class VarReplacer; + friend class ClauseCleaner; Conglomerate* conglomerate; VarReplacer* toReplace; + ClauseCleaner* clauseCleaner; // Debug: void printLit (const Lit l) const; @@ -439,19 +435,8 @@ inline const uint Solver::get_unitary_learnts_num() const { if (decisionLevel() > 0) return trail_lim[0]; - return 0; -} -template -void Solver::removeSatisfied(vec& cs) -{ - int i,j; - for (i = j = 0; i < cs.size(); i++) { - if (satisfied(*cs[i])) - removeClause(*cs[i]); - else - cs[j++] = cs[i]; - } - cs.shrink(i - j); + else + return trail.size(); } template inline void Solver::removeWatchedCl(vec &ws, const Clause *c) { diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 8ac9e02..3771163 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,4 +1,3 @@ CryptoMiniSat -SVN revision: -GIT revision: 63f0b6f7e4927759643c97913060c37f8ae4c82a - +SVN revision: 561 +GIT revision: 56d0a713979afbe737a7da1670f39eaf8c6f53a5 diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index d6cfb3b..0da1bec 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -2,6 +2,7 @@ #include "Solver.h" #include "Conglomerate.h" +#include "ClauseCleaner.h" //#define VERBOSE_DEBUG @@ -24,30 +25,44 @@ VarReplacer::VarReplacer(Solver *_S) : VarReplacer::~VarReplacer() { - for (uint i = 0; i < toRemove.size(); i++) - free(toRemove[i]); + for (uint i = 0; i < clauses.size(); i++) + free(clauses[i]); } void VarReplacer::performReplace() { #ifdef VERBOSE_DEBUG cout << "Replacer started." << endl; + { + uint i = 0; + for (vector::const_iterator it = table.begin(); it != table.end(); it++, i++) { + if (it->var() == i) continue; + cout << "Replacing var " << i+1 << " with Lit " << (it->sign() ? "-" : "") << it->var()+1 << endl; + } + } + #endif + uint i = 0; + const vector& removedVars = S->conglomerate->getRemovedVars(); for (vector::const_iterator it = table.begin(); it != table.end(); it++, i++) { if (it->var() == i) continue; - cout << "Replacing var " << i+1 << " with Lit " << (it->sign() ? "-" : "") << it->var()+1 << endl; + S->setDecisionVar(i, false); + if (!removedVars[it->var()]) + S->setDecisionVar(it->var(), true); } - #endif - + if (!addedNewClause || replacedVars == 0) return; - S->removeSatisfied(S->clauses); - S->removeSatisfied(S->xorclauses); - S->cleanClauses(S->clauses); - S->cleanClauses(S->xorclauses); - for (uint i = 0; i < toRemove.size(); i++) - S->removeClause(*toRemove[i]); - toRemove.clear(); + 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); @@ -98,9 +113,9 @@ void VarReplacer::replace_set(vec& cs, const bool need_reattach) p = lit_Undef; if (!S->assigns[c[i].var()].isUndef()) c.invert(S->assigns[c[i].var()].getBool()); - } else if (S->value(c[i]) == l_Undef) //just add + } else if (S->assigns[c[i].var()].isUndef()) //just add c[j++] = p = c[i]; - else c.invert(S->value(c[i]) == l_True); //modify xor_clause_inverted instead of adding + else c.invert(S->assigns[c[i].var()].getBool()); //modify xor_clause_inverted instead of adding } c.shrink(i - j); @@ -111,21 +126,21 @@ void VarReplacer::replace_set(vec& cs, const bool need_reattach) r++; break; case 1: - S->uncheckedEnqueue(Lit(c[0].var(), !c.xor_clause_inverted())); + 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: - if (c.size() == 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++; - } else { - S->attachClause(c); - *a++ = *r++; - } + S->attachClause(c); + *a++ = *r++; break; } } else { @@ -193,6 +208,10 @@ bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const Lit o S->uncheckedEnqueue(c[0]); S->detachModifiedClause(origLit1, origLit2, origSize, &c); return true; + case 2: + S->detachModifiedClause(origLit1, origLit2, origSize, &c); + S->attachClause(c); + return false; default: if (origLit1 != c[0] || origLit2 != c[1]) { S->detachModifiedClause(origLit1, origLit2, origSize, &c); @@ -228,9 +247,9 @@ const vector VarReplacer::getReplacingVars() const return replacingVars; } -const vec& VarReplacer::getToRemove() const +const vec& VarReplacer::getClauses() const { - return toRemove; + return clauses; } void VarReplacer::extendModel() const @@ -297,15 +316,12 @@ void VarReplacer::replace(vec& ps, const bool xor_clause_inverted, const ui setAllThatPointsHereTo(lit1.var(), Lit(lit.var(), lit1.sign())); table[lit1.var()] = Lit(lit.var(), lit1.sign()); reverseTable[lit.var()].push_back(lit1.var()); - S->setDecisionVar(lit1.var(), false); setAllThatPointsHereTo(lit2.var(), lit ^ lit2.sign()); table[lit2.var()] = lit ^ lit2.sign(); reverseTable[lit.var()].push_back(lit2.var()); - S->setDecisionVar(lit2.var(), false); table[lit.var()] = Lit(lit.var(), false); - S->setDecisionVar(lit.var(), true); return; } } @@ -320,7 +336,6 @@ void VarReplacer::replace(vec& ps, const bool xor_clause_inverted, const ui table[var] = lit; reverseTable[lit.var()].push_back(var); - S->setDecisionVar(var, false); } void VarReplacer::addBinaryXorClause(vec& ps, const bool xor_clause_inverted, const uint group, const bool internal) @@ -334,7 +349,7 @@ void VarReplacer::addBinaryXorClause(vec& ps, const bool xor_clause_inverte if (internal) S->clauses.push(c); else - toRemove.push(c); + clauses.push(c); S->attachClause(*c); ps[0] ^= true; @@ -343,7 +358,7 @@ void VarReplacer::addBinaryXorClause(vec& ps, const bool xor_clause_inverte if (internal) S->clauses.push(c); else - toRemove.push(c); + clauses.push(c); S->attachClause(*c); } diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h index d0c1484..e6c8917 100644 --- a/src/sat/cryptominisat2/VarReplacer.h +++ b/src/sat/cryptominisat2/VarReplacer.h @@ -29,7 +29,7 @@ class VarReplacer const uint getNumReplacedVars() const; const vector getReplacingVars() const; const vector& getReplaceTable() const; - const vec& getToRemove() const; + const vec& getClauses() const; void newClause(); void newVar(); @@ -44,7 +44,7 @@ class VarReplacer vector table; map > reverseTable; - vec toRemove; + vec clauses; uint replacedLits; uint replacedVars; diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp index 766f6c1..4490a22 100644 --- a/src/sat/cryptominisat2/XorFinder.cpp +++ b/src/sat/cryptominisat2/XorFinder.cpp @@ -217,6 +217,8 @@ uint XorFinder::findXors(uint& sumLengths) void XorFinder::clearToRemove() { + assert(toRemove.size() == cls.size()); + Clause **a = cls.getData(); Clause **r = cls.getData(); Clause **cend = cls.getData() + cls.size(); -- 2.47.3