From 79c027bc7e776290f347271a86331d62019db366 Mon Sep 17 00:00:00 2001 From: msoos Date: Fri, 4 Dec 2009 10:36:20 +0000 Subject: [PATCH] Updating CryptoMiniSat to r519. Should fix problems with xor-conglomeration, and should also free all memory git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@453 e59a4935-1847-0410-ae03-e826735625c1 --- src/sat/cryptominisat2/Clause.h | 19 ++++---- src/sat/cryptominisat2/Conglomerate.cpp | 57 +++++++++++++++++++----- src/sat/cryptominisat2/Conglomerate.h | 2 + src/sat/cryptominisat2/Gaussian.cpp | 7 ++- src/sat/cryptominisat2/Logger.cpp | 2 + src/sat/cryptominisat2/Solver.cpp | 59 +++++++++++-------------- src/sat/cryptominisat2/Solver.h | 7 ++- src/sat/cryptominisat2/VERSION | 4 +- src/sat/cryptominisat2/VarReplacer.cpp | 5 +++ src/sat/cryptominisat2/VarReplacer.h | 1 + src/sat/cryptominisat2/XorFinder.cpp | 1 - 11 files changed, 103 insertions(+), 61 deletions(-) diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h index 42e1b7e..1c64836 100644 --- a/src/sat/cryptominisat2/Clause.h +++ b/src/sat/cryptominisat2/Clause.h @@ -79,8 +79,8 @@ public: } // -- use this function instead: - friend Clause* Clause_new(const vec& ps, const uint group, const bool learnt = false); - friend Clause* Clause_new(const vector& ps, const uint group, const bool learnt = false); + template + friend Clause* Clause_new(const T& ps, const uint group, const bool learnt = false); uint size () const { return size_etc >> 16; @@ -171,11 +171,7 @@ public: // -- use this function instead: template - friend XorClause* XorClause_new(const V& ps, const bool inverted, const uint group) { - void* mem = malloc(sizeof(XorClause) + sizeof(Lit)*(ps.size())); - XorClause* real= new (mem) XorClause(ps, inverted, group); - return real; - } + friend XorClause* XorClause_new(const V& ps, const bool inverted, const uint group); inline bool xor_clause_inverted() const { @@ -226,7 +222,14 @@ Clause* Clause_new(const T& ps, const uint group, const bool learnt = false) Clause* real= new (mem) Clause(ps, group, learnt); return real; } -//Clause* Clause_new(const vector& ps, const uint group, const bool learnt); + +template +XorClause* XorClause_new(const T& ps, const bool inverted, const uint group) +{ + void* mem = malloc(sizeof(XorClause) + sizeof(Lit)*(ps.size())); + XorClause* real= new (mem) XorClause(ps, inverted, group); + return real; +} /*_________________________________________________________________________________________________ | diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp index a5da602..b1e5fc5 100644 --- a/src/sat/cryptominisat2/Conglomerate.cpp +++ b/src/sat/cryptominisat2/Conglomerate.cpp @@ -4,6 +4,7 @@ #include #include +using std::make_pair; //#define VERBOSE_DEBUG @@ -13,7 +14,6 @@ using std::cout; using std::endl; #endif -using std::make_pair; namespace MINISAT { @@ -23,6 +23,12 @@ Conglomerate::Conglomerate(Solver *_S) : S(_S) {} +Conglomerate::~Conglomerate() +{ + for(uint i = 0; i < calcAtFinish.size(); i++) + free(calcAtFinish[i]); +} + const vec& Conglomerate::getCalcAtFinish() const { return calcAtFinish; @@ -49,6 +55,14 @@ 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 Clause& c = **it; + for (const Lit* a = &c[0], *end = a + c.size(); a != end; a++) { + blocked[a->var()] = true; + } + } + uint i = 0; for (XorClause* const* it = S->xorclauses.getData(), *const*end = it + S->xorclauses.size(); it != end; it++, i++) { const XorClause& c = **it; @@ -57,14 +71,6 @@ void Conglomerate::fillVarToXor() varToXor[a->var()].push_back(make_pair(*it, i)); } } - - const vector& replaceTable = S->toReplace->getReplaceTable(); - for (uint i = 0; i < replaceTable.size(); i++) { - if (replaceTable[i] != Lit(i, false)) { - blocked[i] = true; - blocked[replaceTable[i].var()] = true; - } - } } void Conglomerate::process_clause(XorClause& x, const uint num, uint var, vec& vars) { @@ -85,12 +91,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); + fillVarToXor(); uint found = 0; @@ -225,7 +235,6 @@ bool Conglomerate::dealWithNewClause(vec& ps, const bool inverted, const ui #endif S->xorclauses.push(newX); - S->xorclauses_tofree.push(newX); toRemove.push_back(false); S->attachClause(*newX); for (const Lit * a = &((*newX)[0]), *end = a + newX->size(); a != end; a++) { @@ -314,4 +323,32 @@ void Conglomerate::doCalcAtFinish() } } +void Conglomerate::addRemovedClauses() +{ + #ifdef VERBOSE_DEBUG + cout << "Executing addRemovedClauses" << endl; + #endif + + char tmp[100]; + tmp[0] = '\0'; + vec ps; + for(uint i = 0; i < calcAtFinish.size(); i++) + { + XorClause& c = *calcAtFinish[i]; + #ifdef VERBOSE_DEBUG + cout << "readding already removed (conglomerated) clause: "; + c.plain_print(); + #endif + + ps.clear(); + for(uint i2 = 0; i2 != c.size() ; i2++) { + ps.push(c[i2]); + S->setDecisionVar(c[i2].var(), true); + } + S->addXorClause(ps, c.xor_clause_inverted(), c.group, tmp); + free(&c); + } + calcAtFinish.clear(); +} + }; diff --git a/src/sat/cryptominisat2/Conglomerate.h b/src/sat/cryptominisat2/Conglomerate.h index 6957a7c..24efe74 100644 --- a/src/sat/cryptominisat2/Conglomerate.h +++ b/src/sat/cryptominisat2/Conglomerate.h @@ -20,7 +20,9 @@ class Conglomerate { public: Conglomerate(Solver *S); + ~Conglomerate(); uint conglomerateXors(); ///& getCalcAtFinish() const; vec& getCalcAtFinish(); diff --git a/src/sat/cryptominisat2/Gaussian.cpp b/src/sat/cryptominisat2/Gaussian.cpp index c1b0d1b..7630e44 100644 --- a/src/sat/cryptominisat2/Gaussian.cpp +++ b/src/sat/cryptominisat2/Gaussian.cpp @@ -21,6 +21,9 @@ along with this program. If not, see . #include #include "Clause.h" #include +using std::ostream; +using std::cout; +using std::endl; #ifdef VERBOSE_DEBUG #include @@ -30,10 +33,6 @@ namespace MINISAT { using namespace MINISAT; -using std::ostream; -using std::cout; -using std::endl; - ostream& operator << (ostream& os, const vec& v) { for (int i = 0; i < v.size(); i++) { diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp index dd7b23b..d70ca14 100644 --- a/src/sat/cryptominisat2/Logger.cpp +++ b/src/sat/cryptominisat2/Logger.cpp @@ -126,6 +126,8 @@ void Logger::set_group_name(const uint group, string name) if (name.length() == 0) return; + if (name == "Noname" || name == "") return; + if (groupnames[group] == "Noname") { groupnames[group] = name; } else if (groupnames[group] != name) { diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index bcf6931..c5abee0 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -52,6 +52,7 @@ using namespace MINISAT; //================================================================================================= // Constructor/Destructor: + Solver::Solver() : // Parameters: (formerly in 'SearchParams') var_decay(1 / 0.95), random_var_freq(0.02) @@ -65,6 +66,7 @@ Solver::Solver() : , restrictedPickBranch(0) , useRealUnknowns (false) , xorFinder (true) + , performReplace (true) , greedyUnbound (false) // Statistics: (formerly in 'SolverStats') @@ -111,7 +113,7 @@ Solver::~Solver() for (int i = 0; i < learnts.size(); i++) free(learnts[i]); for (int i = 0; i < unitary_learnts.size(); i++) free(unitary_learnts[i]); for (int i = 0; i < clauses.size(); i++) free(clauses[i]); - for (int i = 0; i < xorclauses_tofree.size(); i++) free(xorclauses_tofree[i]); + for (int i = 0; i < xorclauses.size(); i++) free(xorclauses[i]); for (uint i = 0; i < gauss_matrixes.size(); i++) delete gauss_matrixes[i]; gauss_matrixes.clear(); delete toReplace; @@ -175,7 +177,7 @@ bool Solver::addXorClause(vec& 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(); + ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); xor_clause_inverted ^= ps[i].sign(); ps[i] ^= ps[i].sign(); @@ -219,7 +221,6 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro XorClause* c = XorClause_new(ps, xor_clause_inverted, group); xorclauses.push(c); - xorclauses_tofree.push(c); attachClause(*c); toReplace->newClause(); break; @@ -251,7 +252,7 @@ bool Solver::addClause(vec& 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(); + 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) @@ -415,24 +416,6 @@ void Solver::cancelUntil(int level) #endif } -//Permutates the clauses in the solver. Very useful to calcuate the average time it takes the solver to solve the prolbem -void Solver::permutateClauses() -{ - for (int i = 0; i < clauses.size(); i++) { - int j = mtrand.randInt(i); - Clause* tmp = clauses[i]; - clauses[i] = clauses[j]; - clauses[j] = tmp; - } - - for (int i = 0; i < xorclauses.size(); i++) { - int j = mtrand.randInt(i); - XorClause* tmp = xorclauses[i]; - xorclauses[i] = xorclauses[j]; - xorclauses[j] = tmp; - } -} - void Solver::setRealUnknown(const uint var) { if (realUnknowns.size() < var+1) @@ -1452,8 +1435,12 @@ lbool Solver::solve(const vec& assumps) nbclausesbeforereduce = (nClauses() * learntsize_factor)/2; } - //toReplace->performReplace(); - //if (!ok) return l_False; + conglomerate->addRemovedClauses(); + + if (performReplace) { + toReplace->performReplace(); + if (!ok) return l_False; + } if (xorFinder) { double time; @@ -1464,10 +1451,15 @@ lbool Solver::solve(const vec& assumps) uint sumLengths = 0; XorFinder xorFinder(this, clauses); uint foundXors = xorFinder.doNoPart(sumLengths, 2, 10); + if (!ok) return l_False; if (verbosity >=1) printf("| Finding XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors); - if (!ok) return l_False; + + if (performReplace) { + toReplace->performReplace(); + if (!ok) return l_False; + } } if (xorclauses.size() > 1) { @@ -1478,8 +1470,6 @@ lbool Solver::solve(const vec& assumps) } time = cpuTime(); - removeSatisfied(xorclauses); - cleanClauses(xorclauses); uint foundCong = conglomerate->conglomerateXors(); if (verbosity >=1) printf("| Conglomerating XORs: %4.2lf s (removed %6d vars) |\n", cpuTime()-time, foundCong); @@ -1494,12 +1484,14 @@ lbool Solver::solve(const vec& assumps) printf("| Sum xclauses before: %8d, after: %12d |\n", orig_num_cls, new_num_cls); printf("| Sum xlits before: %11d, after: %12d |\n", orig_total, new_total); } + + if (performReplace) { + toReplace->performReplace(); + if (!ok) return l_False; + } } } - //toReplace->performReplace(); - //if (!ok) return l_False; - if (gaussconfig.decision_until > 0 && xorclauses.size() > 1 && xorclauses.size() < 20000) { removeSatisfied(xorclauses); cleanClauses(xorclauses); @@ -1509,6 +1501,7 @@ lbool Solver::solve(const vec& assumps) if (verbosity >=1) printf("| Finding matrixes : %4.2lf s (found %5d) |\n", cpuTime()-time, numMatrixes); } + if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) { printf("============================[ Search Statistics ]========================================\n"); @@ -1592,8 +1585,10 @@ bool Solver::verifyXorClauses(const vec& cs) const bool final = c.xor_clause_inverted(); #ifdef VERBOSE_DEBUG - std::sort(&c[0], &c[0] + c.size()); - c.plain_print(); + XorClause* c2 = XorClause_new(c, c.xor_clause_inverted(), c.group); + std::sort(c2->getData(), c2->getData()+ c2->size()); + c2->plain_print(); + free(c2); #endif for (uint j = 0; j < c.size(); j++) { diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index e1cbe2a..45e3f83 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -93,7 +93,6 @@ public: void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'. void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic. void setSeed (const uint32_t seed); // Sets the seed to be the given number - void permutateClauses(); // Permutates the clauses using the seed. It updates the seed in mtrand void needRealUnknowns(); // Uses the "real unknowns" set by setRealUnknown void setRealUnknown(const uint var); //sets a variable to be 'real', i.e. to preferentially branch on it during solving (when useRealUnknown it turned on) void setMaxRestarts(const uint num); //sets the maximum number of restarts to given value @@ -133,10 +132,11 @@ public: bool expensive_ccmin; // Controls conflict clause minimization. (default TRUE) int polarity_mode; // Controls which polarity the decision heuristic chooses. See enum below for allowed modes. (default polarity_false) int verbosity; // Verbosity level. 0=silent, 1=some progress report (default 0) - uint restrictedPickBranch; // Pick variables to branch on preferentally from the highest [0, restrictedPickBranch]. If set to 0, preferentiality is turned off (i.e. picked randomly between [0, all]) + Var restrictedPickBranch; // Pick variables to branch on preferentally from the highest [0, restrictedPickBranch]. If set to 0, preferentiality is turned off (i.e. picked randomly between [0, all]) bool useRealUnknowns; // Whether 'real unknown' optimization should be used. If turned on, VarActivity is only bumped for variables for which the real_unknowns[var] == true vector realUnknowns; // The important variables. This vector stores 'false' at realUnknowns[var] if the var is not a real unknown, and stores a 'true' if it is a real unkown. If var is larger than realUnkowns.size(), then it is not an important variable bool xorFinder; // Automatically find xor-clauses and convert them + bool performReplace; // Should var-replacing be performed? friend class FindUndef; bool greedyUnbound; //If set to TRUE, then we will greedily unbound variables (set them to l_Undef) void set_gaussian_decision_until(const uint to); @@ -190,8 +190,7 @@ protected: // bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! vec clauses; // List of problem clauses. - vec xorclauses; // List of problem xor-clauses. Will not be freed - vec xorclauses_tofree;// List of problem xor-clauses. Will be freed + vec xorclauses; // List of problem xor-clauses. Will be freed vec learnts; // List of learnt clauses. vec unitary_learnts; // List of learnt clauses. vec activity; // A heuristic measurement of the activity of a variable. diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index f44772a..0814fa6 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,4 +1,4 @@ CryptoMiniSat -SVN revision: 504 -GIT revision: 4f460459f42a5fd33d971a19f9c206985a73c40d +SVN revision: 519 +GIT revision: 0426e61b02a00a073a87fdffc0282820875fad61 diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index 06f3c04..4e08cd1 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -229,6 +229,11 @@ const vector VarReplacer::getReplacingVars() const return replacingVars; } +const vec& VarReplacer::getToRemove() const +{ + return toRemove; +} + void VarReplacer::extendModel() const { uint i = 0; diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h index 63218cb..d0c1484 100644 --- a/src/sat/cryptominisat2/VarReplacer.h +++ b/src/sat/cryptominisat2/VarReplacer.h @@ -29,6 +29,7 @@ class VarReplacer const uint getNumReplacedVars() const; const vector getReplacingVars() const; const vector& getReplaceTable() const; + const vec& getToRemove() const; void newClause(); void newVar(); diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp index 5392d7b..766f6c1 100644 --- a/src/sat/cryptominisat2/XorFinder.cpp +++ b/src/sat/cryptominisat2/XorFinder.cpp @@ -199,7 +199,6 @@ uint XorFinder::findXors(uint& sumLengths) default: { XorClause* x = XorClause_new(lits, impair, old_group); S->xorclauses.push(x); - S->xorclauses_tofree.push(x); S->attachClause(*x); #ifdef VERBOSE_DEBUG -- 2.47.3