From fd4ccf3ec07389cfb690ed61552431af9d2c5e45 Mon Sep 17 00:00:00 2001 From: msoos Date: Tue, 1 Dec 2009 23:14:57 +0000 Subject: [PATCH] Updating CryptoMiniSat2 to r494. The only difference between this version and the version in SVN is that performReplace() is not called here. The reasons for this are: 1) performReplace() is at the moment buggy when MiniSat is used as a library 2) For a programmable solver, we need to have all variables to propagating at all times, thus we cannot accept to have certain variables acting as more than one (for which performReplace is used) git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@443 e59a4935-1847-0410-ae03-e826735625c1 --- src/sat/cryptominisat2/Conglomerate.cpp | 42 +++++++++---- src/sat/cryptominisat2/Conglomerate.h | 6 +- src/sat/cryptominisat2/MatrixFinder.cpp | 16 +++-- src/sat/cryptominisat2/Solver.cpp | 78 ++++++++++++++++++------ src/sat/cryptominisat2/Solver.h | 21 +------ src/sat/cryptominisat2/VERSION | 4 +- src/sat/cryptominisat2/VarReplacer.cpp | 79 ++++++++++++++++++++----- src/sat/cryptominisat2/VarReplacer.h | 7 ++- src/sat/cryptominisat2/XorFinder.cpp | 16 +++-- 9 files changed, 181 insertions(+), 88 deletions(-) diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp index 0d7696c..a5da602 100644 --- a/src/sat/cryptominisat2/Conglomerate.cpp +++ b/src/sat/cryptominisat2/Conglomerate.cpp @@ -57,12 +57,20 @@ 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, vector& vars) { +void Conglomerate::process_clause(XorClause& x, const uint num, uint var, vec& vars) { for (const Lit* a = &x[0], *end = a + x.size(); a != end; a++) { if (a->var() != var) { - vars.push_back(*a); + vars.push(*a); varToXorMap::iterator finder = varToXor.find(a->var()); if (finder != varToXor.end()) { vector >::iterator it = @@ -90,6 +98,13 @@ uint Conglomerate::conglomerateXors() varToXorMap::iterator it = varToXor.begin(); const vector >& c = it->second; const uint& var = it->first; + + //We blocked the var during dealWithNewClause (it was in a 2-long xor-clause) + if (blocked[var]) { + varToXor.erase(it); + continue; + } + S->setDecisionVar(var, false); if (c.size() == 0) { @@ -103,7 +118,7 @@ uint Conglomerate::conglomerateXors() XorClause& x = *(c[0].first); bool first_inverted = !x.xor_clause_inverted(); - vector first_vars; + vec first_vars; process_clause(x, c[0].second, var, first_vars); #ifdef VERBOSE_DEBUG @@ -118,9 +133,9 @@ uint Conglomerate::conglomerateXors() calcAtFinish.push(&x); found++; - vector ps; for (uint i = 1; i < c.size(); i++) { - ps = first_vars; + vec ps(first_vars.size()); + memcpy(ps.getData(), first_vars.getData(), sizeof(Lit)*first_vars.size()); XorClause& x = *c[i].first; process_clause(x, c[i].second, var, ps); @@ -149,14 +164,13 @@ uint Conglomerate::conglomerateXors() clearToRemove(); - S->toReplace->performReplace(); - if (S->ok == false) return found; - S->ok = (S->propagate() == NULL); + if (S->ok != false) + S->ok = (S->propagate() == NULL); return found; } -bool Conglomerate::dealWithNewClause(vector& ps, const bool inverted, const uint old_group) +bool Conglomerate::dealWithNewClause(vec& ps, const bool inverted, const uint old_group) { switch(ps.size()) { case 0: { @@ -196,7 +210,9 @@ bool Conglomerate::dealWithNewClause(vector& ps, const bool inverted, const free(newX); #endif - S->toReplace->replace(ps[0].var(), Lit(ps[1].var(), !inverted)); + S->toReplace->replace(ps, inverted, old_group); + blocked[ps[0].var()] = true; + blocked[ps[1].var()] = true; break; } @@ -223,9 +239,9 @@ bool Conglomerate::dealWithNewClause(vector& ps, const bool inverted, const return true; } -void Conglomerate::clearDouble(vector& ps) const +void Conglomerate::clearDouble(vec& ps) const { - std::sort(ps.begin(), ps.end()); + std::sort(ps.getData(), ps.getData() + ps.size()); Lit p; uint i, j; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { @@ -236,7 +252,7 @@ void Conglomerate::clearDouble(vector& ps) const } else //just add ps[j++] = p = ps[i]; } - ps.resize(ps.size()-(i - j)); + ps.shrink(i - j); } void Conglomerate::clearToRemove() diff --git a/src/sat/cryptominisat2/Conglomerate.h b/src/sat/cryptominisat2/Conglomerate.h index 1927571..6957a7c 100644 --- a/src/sat/cryptominisat2/Conglomerate.h +++ b/src/sat/cryptominisat2/Conglomerate.h @@ -27,11 +27,11 @@ public: private: - void process_clause(XorClause& x, const uint num, uint var, vector& vars); + void process_clause(XorClause& x, const uint num, uint var, vec& vars); void fillVarToXor(); - void clearDouble(vector& ps) const; + void clearDouble(vec& ps) const; void clearToRemove(); - bool dealWithNewClause(vector& ps, const bool inverted, const uint old_group); + bool dealWithNewClause(vec& ps, const bool inverted, const uint old_group); typedef map > > varToXorMap; varToXorMap varToXor; diff --git a/src/sat/cryptominisat2/MatrixFinder.cpp b/src/sat/cryptominisat2/MatrixFinder.cpp index ba1e552..def2113 100644 --- a/src/sat/cryptominisat2/MatrixFinder.cpp +++ b/src/sat/cryptominisat2/MatrixFinder.cpp @@ -177,17 +177,21 @@ const uint MatrixFinder::setMatrixes() && numXorInMatrix[a].second <= 1000 && realMatrixNum < 3) { - cout << "| Matrix no " << std::setw(4) << realMatrixNum; + if (S->verbosity >=1) + cout << "| Matrix no " << std::setw(4) << realMatrixNum; S->gauss_matrixes.push_back(new Gaussian(*S, S->gaussconfig, realMatrixNum, xorsInMatrix[i])); realMatrixNum++; } else { - cout << "| Unused Matrix "; + if (S->verbosity >=1) + cout << "| Unused Matrix "; + } + if (S->verbosity >=1) { + cout << std::setw(5) << numXorInMatrix[a].second << " x" << std::setw(5) << reverseTable[i].size(); + cout << " density:" << std::setw(5) << std::fixed << std::setprecision(1) << density << "%"; + cout << " xorlen avg:" << std::setw(5) << std::fixed << std::setprecision(2) << avg; + cout << " stdev:" << std::setw(6) << std::fixed << std::setprecision(2) << stdDeviation << " |" << endl; } - cout << std::setw(5) << numXorInMatrix[a].second << " x" << std::setw(5) << reverseTable[i].size(); - cout << " density:" << std::setw(5) << std::fixed << std::setprecision(1) << density << "%"; - cout << " xorlen avg:" << std::setw(5) << std::fixed << std::setprecision(2) << avg; - cout << " stdev:" << std::setw(6) << std::fixed << std::setprecision(2) << stdDeviation << " |" << endl; } return realMatrixNum; diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index 73607d7..8a31895 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -37,6 +37,14 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Conglomerate.h" #include "XorFinder.h" +//#define DEBUG_LIB + +#ifdef DEBUG_LIB +#include +FILE* myoutputfile; +static uint numcalled = 0; +#endif //DEBUG_LIB + namespace MINISAT { using namespace MINISAT; @@ -44,7 +52,6 @@ using namespace MINISAT; //================================================================================================= // Constructor/Destructor: - Solver::Solver() : // Parameters: (formerly in 'SearchParams') var_decay(1 / 0.95), random_var_freq(0.02) @@ -90,6 +97,12 @@ Solver::Solver() : toReplace = new VarReplacer(this); conglomerate = new Conglomerate(this); logger.setSolver(this); + + #ifdef DEBUG_LIB + std::stringstream ss; + ss << "inputfile" << numcalled << ".cnf"; + myoutputfile = fopen(ss.str().c_str(), "w"); + #endif } @@ -103,6 +116,10 @@ Solver::~Solver() gauss_matrixes.clear(); delete toReplace; delete conglomerate; + + #ifdef DEBUG_LIB + fclose(myoutputfile); + #endif //DEBUG_LIB } //================================================================================================= @@ -139,8 +156,14 @@ Var Solver::newVar(bool sign, bool dvar) bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint group, char* group_name) { - 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); + } + fprintf(myoutputfile, "0\n"); + #endif //DEBUG_LIB if (dynamic_behaviour_analysis) logger.set_group_name(group, group_name); @@ -177,7 +200,7 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro } case 1: { assert(value(ps[0]) == l_Undef); - uncheckedEnqueue( (xor_clause_inverted) ? ~ps[0] : ps[0]); + uncheckedEnqueue(ps[0] ^ xor_clause_inverted); if (dynamic_behaviour_analysis) logger.propagation((xor_clause_inverted) ? ~ps[0] : ps[0], Logger::add_clause_type, group); return ok = (propagate() == NULL); @@ -187,8 +210,7 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro cout << "--> xor is 2-long, replacing var " << ps[0].var()+1 << " with " << (!xor_clause_inverted ? "-" : "") << ps[1].var()+1 << endl; #endif - learnt_clause_group = std::max(group+1, learnt_clause_group); - toReplace->replace(ps[0].var(), Lit(ps[1].var(), !xor_clause_inverted)); + toReplace->replace(ps, xor_clause_inverted, group); break; } default: { @@ -198,6 +220,7 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro xorclauses.push(c); xorclauses_tofree.push(c); attachClause(*c); + toReplace->newClause(); break; } } @@ -208,6 +231,13 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro bool Solver::addClause(vec& ps, const uint group, char* group_name) { assert(decisionLevel() == 0); + + #ifdef DEBUG_LIB + for (int i = 0; i < ps.size(); i++) { + fprintf(myoutputfile, "%s%d ", ps[i].sign() ? "-" : "", ps[i].var()+1); + } + fprintf(myoutputfile, "0\n"); + #endif //DEBUG_LIB if (dynamic_behaviour_analysis) logger.set_group_name(group, group_name); @@ -239,11 +269,11 @@ bool Solver::addClause(vec& ps, const uint group, char* group_name) return ok = (propagate() == NULL); } else { learnt_clause_group = std::max(group+1, learnt_clause_group); - Clause* c = Clause_new(ps, group); clauses.push(c); attachClause(*c); + toReplace->newClause(); } return true; @@ -1093,10 +1123,10 @@ void Solver::cleanClauses(vec& cs) if (i-j > 0) useful++; if (c.size() == 2) { - vec ps; - ps.push(c[0]); - ps.push(c[1]); - addBinaryXorClause(ps, c.xor_clause_inverted(), c.group); + vec ps(2); + ps[0] = c[0]; + ps[1] = c[1]; + toReplace->replace(ps, c.xor_clause_inverted(), c.group); removeClause(c); s++; } else @@ -1396,12 +1426,15 @@ void Solver::print_gauss_sum_stats() const lbool Solver::solve(const vec& assumps) { + #ifdef DEBUG_LIB + fprintf(myoutputfile, "c Solver::solve() called\n"); + #endif + if (dynamic_behaviour_analysis) logger.end(Logger::done_adding_clauses); model.clear(); conflict.clear(); - curRestart = 1; if (!ok) return l_False; @@ -1417,8 +1450,8 @@ lbool Solver::solve(const vec& assumps) nbclausesbeforereduce = (nClauses() * learntsize_factor)/2; } - toReplace->performReplace(); - if (!ok) return l_False; + //toReplace->performReplace(); + //if (!ok) return l_False; if (xorFinder) { double time; @@ -1430,7 +1463,8 @@ lbool Solver::solve(const vec& assumps) XorFinder xorFinder(this, clauses); uint foundXors = xorFinder.doNoPart(sumLengths, 2, 10); - printf("| Finding XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors); + 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; } @@ -1445,7 +1479,8 @@ lbool Solver::solve(const vec& assumps) removeSatisfied(xorclauses); cleanClauses(xorclauses); uint foundCong = conglomerate->conglomerateXors(); - printf("| Conglomerating XORs: %4.2lf s (removed %6d vars) |\n", cpuTime()-time, foundCong); + if (verbosity >=1) + printf("| Conglomerating XORs: %4.2lf s (removed %6d vars) |\n", cpuTime()-time, foundCong); if (!ok) return l_False; uint new_total = 0; @@ -1453,20 +1488,25 @@ lbool Solver::solve(const vec& assumps) for (uint i = 0; i < xorclauses.size(); i++) { new_total += xorclauses[i]->size(); } - 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 (verbosity >=1) { + 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); + } } } + //toReplace->performReplace(); + //if (!ok) return l_False; + if (gaussconfig.decision_until > 0 && xorclauses.size() > 1 && xorclauses.size() < 20000) { removeSatisfied(xorclauses); cleanClauses(xorclauses); double time = cpuTime(); MatrixFinder m(this); const uint numMatrixes = m.findMatrixes(); - printf("| Finding matrixes : %4.2lf s (found %5d) |\n", cpuTime()-time, numMatrixes); + 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"); diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 31ccbac..ff31e97 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -84,7 +84,6 @@ public: // Solving: // - lbool simplify (); // Removes already satisfied clauses. lbool solve (const vec& assumps); // Search for a model that respects a given set of assumptions. lbool solve (); // Search without assumptions. bool okay () const; // FALSE means solver is in a conflicting state @@ -241,6 +240,7 @@ protected: // Main internal methods: // + lbool simplify (); // Removes already satisfied clauses. //int nbPropagated (int level); void insertVarOrder (Var x); // Insert a variable in the decision order priority queue. Lit pickBranchLit (int polarity_mode); // Return the next decision variable. @@ -283,8 +283,6 @@ protected: 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 - template - inline void addBinaryXorClause(T& ps, const bool xor_clause_inverted, const uint group); //Adds Binary XOR clause as two normal clauses // Misc: // @@ -486,23 +484,6 @@ inline void Solver::reverse_binary_clause(Clause& c) const { c[0] = c[1], c[1] = tmp; } } -template -inline void Solver::addBinaryXorClause(T& ps, const bool xor_clause_inverted, const uint group) { - Clause* c; - ps[0] = ps[0].unsign(); - ps[1] = ps[1].unsign(); - ps[0] ^= xor_clause_inverted; - - c = Clause_new(ps, group, false); - clauses.push(c); - attachClause(*c); - - ps[0] ^= true; - ps[1] ^= true; - c = Clause_new(ps, group, false); - clauses.push(c); - attachClause(*c); -} inline void Solver::removeClause(Clause& c) { detachClause(c); diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index ef1835c..69cca9b 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,4 +1,4 @@ CryptoMiniSat -SVN revision: r484 -GIT revision: 36a94d9b25be76b24dd26a413928a3ae559c3983 +SVN revision: r494 +GIT revision: eb7c71aaf2cea3bf064270d227cf7ddf27b852f2 diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index fde63c6..5862654 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -17,6 +17,7 @@ namespace MINISAT VarReplacer::VarReplacer(Solver *_S) : replacedLits(0) , replacedVars(0) + , addedNewClause(false) , S(_S) { } @@ -32,7 +33,15 @@ void VarReplacer::performReplace() } #endif - if (replacedVars == 0) return; + 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(); replace_set(S->clauses); replace_set(S->learnts); @@ -40,10 +49,11 @@ void VarReplacer::performReplace() replace_set(S->xorclauses, true); replace_set(S->conglomerate->getCalcAtFinish(), false); - printf("| Replacing %8d vars, replaced %8d lits |\n", replacedVars, replacedLits); + if (S->verbosity >=1) + printf("| Replacing %8d vars, replaced %8d lits |\n", replacedVars, replacedLits); - replacedVars = 0; replacedLits = 0; + addedNewClause = false; if (S->ok) S->ok = (S->propagate() == NULL); @@ -90,20 +100,21 @@ void VarReplacer::replace_set(vec& cs, const bool need_reattach) c.shrink(i - j); switch (c.size()) { - case 0: { + case 0: if (!c.xor_clause_inverted()) S->ok = false; r++; break; - } - case 1: { + case 1: S->uncheckedEnqueue(Lit(c[0].var(), !c.xor_clause_inverted())); r++; break; - } - default: { + default: if (c.size() == 2) { - S->addBinaryXorClause(c, c.xor_clause_inverted(), c.group); + 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 { @@ -112,7 +123,6 @@ void VarReplacer::replace_set(vec& cs, const bool need_reattach) } break; } - } } else { *a++ = *r++; } @@ -197,6 +207,11 @@ const uint VarReplacer::getNumReplacedVars() const return replacedVars; } +const vector& VarReplacer::getReplaceTable() const +{ + return table; +} + const vector VarReplacer::getReplacingVars() const { vector replacingVars; @@ -220,16 +235,21 @@ void VarReplacer::extendModel() const cout << endl; #endif - assert(S->assigns[i] == l_Undef); assert(S->assigns[it->var()] != l_Undef); - - bool val = (S->assigns[it->var()] == l_False); - S->uncheckedEnqueue(Lit(i, val ^ it->sign())); + if (S->assigns[i] == l_Undef) { + bool val = (S->assigns[it->var()] == l_False); + S->uncheckedEnqueue(Lit(i, val ^ it->sign())); + } else { + assert(S->assigns[i].getBool() == S->assigns[it->var()].getBool() ^ it->sign()); + } } } -void VarReplacer::replace(Var var, Lit lit) +void VarReplacer::replace(vec& ps, const bool xor_clause_inverted, const uint group) { + addBinaryXorClause(ps, xor_clause_inverted, group); + Var var = ps[0].var(); + Lit lit = Lit(ps[1].var(), !xor_clause_inverted); assert(var != lit.var()); //Detect circle @@ -293,6 +313,30 @@ void VarReplacer::replace(Var var, Lit lit) S->setDecisionVar(var, false); } +void VarReplacer::addBinaryXorClause(vec& ps, const bool xor_clause_inverted, const uint group, const bool internal) +{ + Clause* c; + ps[0] = ps[0].unsign(); + ps[1] = ps[1].unsign(); + ps[0] ^= xor_clause_inverted; + + c = Clause_new(ps, group, false); + if (internal) + S->clauses.push(c); + else + toRemove.push(c); + S->attachClause(*c); + + ps[0] ^= true; + ps[1] ^= true; + c = Clause_new(ps, group, false); + if (internal) + S->clauses.push(c); + else + toRemove.push(c); + S->attachClause(*c); +} + bool VarReplacer::alreadyIn(const Var var, const Lit lit) { Lit lit2 = table[var]; @@ -339,4 +383,9 @@ void VarReplacer::newVar() { table.push_back(Lit(table.size(), false)); } + +void VarReplacer::newClause() +{ + addedNewClause = true; +} }; diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h index 3d11ff0..a682b66 100644 --- a/src/sat/cryptominisat2/VarReplacer.h +++ b/src/sat/cryptominisat2/VarReplacer.h @@ -21,27 +21,32 @@ class VarReplacer { public: VarReplacer(Solver* S); - void replace(const Var var, Lit lit); + void replace(vec& ps, const bool xor_clause_inverted, const uint group); void extendModel() const; void performReplace(); const uint getNumReplacedLits() const; const uint getNumReplacedVars() const; const vector getReplacingVars() const; + const vector& getReplaceTable() const; + void newClause(); void newVar(); 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 addBinaryXorClause(vec& ps, const bool xor_clause_inverted, const uint group, const bool internal = false); void setAllThatPointsHereTo(const Var var, const Lit lit); bool alreadyIn(const Var var, const Lit lit); vector table; map > reverseTable; + vec toRemove; uint replacedLits; uint replacedVars; + bool addedNewClause; Solver* S; }; }; diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp index 3808c85..e7cdd39 100644 --- a/src/sat/cryptominisat2/XorFinder.cpp +++ b/src/sat/cryptominisat2/XorFinder.cpp @@ -61,9 +61,8 @@ uint XorFinder::doNoPart(uint& sumLengths, const uint minSize, const uint maxSiz if (found > 0) { clearToRemove(); - S->toReplace->performReplace(); - if (S->ok == false) return found; - S->ok = (S->propagate() == NULL); + if (S->ok != false) + S->ok = (S->propagate() == NULL); } return found; @@ -140,9 +139,8 @@ uint XorFinder::doByPart(uint& sumLengths, const uint minSize, const uint maxSiz clearToRemove(); - S->toReplace->performReplace(); - if (S->ok == false) return found; - S->ok = (S->propagate() == NULL); + if (S->ok != false) + S->ok = (S->propagate() == NULL); #ifdef VERBOSE_DEBUG cout << "Overdone work due to partitioning:" << (double)sumNumClauses/(double)cls.size() << "x" << endl; @@ -163,13 +161,13 @@ uint XorFinder::findXors(uint& sumLengths) ClauseTable::iterator begin = table.begin(); ClauseTable::iterator end = table.begin(); - vector lits; + vec lits; bool impair; while (getNextXor(begin, end, impair)) { const Clause& c = *(begin->first); lits.clear(); for (const Lit *it = &c[0], *cend = it+c.size() ; it != cend; it++) { - lits.push_back(Lit(it->var(), false)); + lits.push(Lit(it->var(), false)); } uint old_group = c.group; @@ -187,7 +185,7 @@ uint XorFinder::findXors(uint& sumLengths) switch(lits.size()) { case 2: { - S->toReplace->replace(lits[0].var(), Lit(lits[1].var(), !impair)); + S->toReplace->replace(lits, impair, old_group); #ifdef VERBOSE_DEBUG XorClause* x = XorClause_new(lits, impair, old_group); -- 2.47.3