diff options
Diffstat (limited to 'src/prop/cryptominisat/Solver/Solver.cpp')
| -rw-r--r-- | src/prop/cryptominisat/Solver/Solver.cpp | 2924 |
1 files changed, 0 insertions, 2924 deletions
diff --git a/src/prop/cryptominisat/Solver/Solver.cpp b/src/prop/cryptominisat/Solver/Solver.cpp deleted file mode 100644 index f73d6166e..000000000 --- a/src/prop/cryptominisat/Solver/Solver.cpp +++ /dev/null @@ -1,2924 +0,0 @@ -/***************************************************************************** -MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson -glucose -- Gilles Audemard, Laurent Simon (2008) -CryptoMiniSat -- Copyright (c) 2009 Mate Soos - -Original code by MiniSat and glucose authors are under an MIT licence. -Modifications for CryptoMiniSat are under GPLv3 licence. -******************************************************************************/ - -#include "Solver.h" -#include <cmath> -#include <string.h> -#include <algorithm> -#include <limits.h> -#include <vector> -#include <iomanip> -#include <algorithm> - -#include "Clause.h" -#include "time_mem.h" - -#include "VarReplacer.h" -#include "XorFinder.h" -#include "ClauseCleaner.h" -#include "RestartTypeChooser.h" -#include "FailedLitSearcher.h" -#include "Subsumer.h" -#include "XorSubsumer.h" -#include "StateSaver.h" -#include "SCCFinder.h" -#include "SharedData.h" -#include "ClauseVivifier.h" -#include "Gaussian.h" -#include "MatrixFinder.h" -#include "DataSync.h" -#include "BothCache.h" - -#ifdef VERBOSE_DEBUG -#define UNWINDING_DEBUG -#endif - -//#define DEBUG_UNCHECKEDENQUEUE_LEVEL0 -//#define VERBOSE_DEBUG_POLARITIES -//#define DEBUG_DYNAMIC_RESTART -//#define UNWINDING_DEBUG - -//********************************** -// Constructor/Destructor: -//********************************** - -using namespace CMSat; - -/** -@brief Sets a sane default config and allocates handler classes -*/ -Solver::Solver(const SolverConf& _conf, const GaussConf& _gaussconfig, SharedData* sharedData) : - // Parameters: (formerly in 'SearchParams') - conf(_conf) - , gaussconfig(_gaussconfig) - , needToInterrupt (false) - #ifdef USE_GAUSS - , sum_gauss_called (0) - , sum_gauss_confl (0) - , sum_gauss_prop (0) - , sum_gauss_unit_truths (0) - #endif //USE_GAUSS - - // Stats - , starts(0), dynStarts(0), staticStarts(0), fullStarts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0) - , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) - , nbGlue2(0), numNewBin(0), lastNbBin(0), lastSearchForBinaryXor(0), nbReduceDB(0) - , improvedClauseNo(0), improvedClauseSize(0) - , numShrinkedClause(0), numShrinkedClauseLits(0) - , moreRecurMinLDo(0) - , updateTransCache(0) - , nbClOverMaxGlue(0) - - , ok (true) - , numBins (0) - , cla_inc (1) - , qhead (0) - , mtrand ((unsigned long int)0) - - //variables - , order_heap (VarOrderLt(activity)) - , var_inc (128) - - //learnts - , numCleanedLearnts(1) - , nbClBeforeRed (NBCLAUSESBEFOREREDUCE) - , nbCompensateSubsumer (0) - , libraryCNFFile (NULL) - , restartType (static_restart) - , lastSelectedRestartType (static_restart) - , simplifying (false) - , totalSimplifyTime(0.0) - , simpDB_assigns (-1) - , simpDB_props (0) -{ - mtrand.seed(conf.origSeed); - #ifdef ENABLE_UNWIND_GLUE - assert(conf.maxGlue < MAX_THEORETICAL_GLUE); - #endif //ENABLE_UNWIND_GLUE - varReplacer = new VarReplacer(*this); - clauseCleaner = new ClauseCleaner(*this); - failedLitSearcher = new FailedLitSearcher(*this); - subsumer = new Subsumer(*this); - xorSubsumer = new XorSubsumer(*this); - restartTypeChooser = new RestartTypeChooser(*this); - sCCFinder = new SCCFinder(*this); - clauseVivifier = new ClauseVivifier(*this); - matrixFinder = new MatrixFinder(*this); - dataSync = new DataSync(*this, sharedData); - -} - -/** -@brief Frees clauses and frees all allocated hander classes -*/ -Solver::~Solver() -{ - clearGaussMatrixes(); - delete matrixFinder; - delete varReplacer; - delete clauseCleaner; - delete failedLitSearcher; - delete subsumer; - delete xorSubsumer; - delete restartTypeChooser; - - if (libraryCNFFile) - fclose(libraryCNFFile); -} - -//********************************** -// Minor methods -//********************************** - -/** -@brief Creates a new SAT variable in the solver - -This entails making the datastructures large enough to fit the new variable -in all internal datastructures as well as all datastructures used in -classes used inside Solver - -@p dvar The new variable should be used as a decision variable? - NOTE: this has effects on the meaning of a SATISFIABLE result -*/ -Var Solver::newVar(bool dvar) throw (std::out_of_range) -{ - Var v = nVars(); - if (v >= 1<<30) - throw std::out_of_range("ERROR! Variable requested is far too large"); - - watches .push(); // (list for positive literal) - watches .push(); // (list for negative literal) - reason .push(PropBy()); - assigns .push(l_Undef); - level .push(-1); - binPropData.push(); - activity .push(0); - seen .push_back(0); - seen .push_back(0); - #ifdef ENABLE_UNWIND_GLUE - unWindGlue.push(NULL); - #endif //ENABLE_UNWIND_GLUE - - //Transitive OTF self-subsuming resolution - seen2 .push_back(0); - seen2 .push_back(0); - transOTFCache.push_back(TransCache()); - transOTFCache.push_back(TransCache()); - litReachable.push_back(LitReachData()); - litReachable.push_back(LitReachData()); - - polarity .push_back(defaultPolarity()); - - decision_var.push_back(dvar); - insertVarOrder(v); - - varReplacer->newVar(); - subsumer->newVar(); - xorSubsumer->newVar(); - dataSync->newVar(); - - insertVarOrder(v); - - if (libraryCNFFile) - fprintf(libraryCNFFile, "c Solver::newVar() called\n"); - - return v; -} - -/** -@brief Adds an xor clause to the problem - -Should ONLY be called from internally. This is different from the extenal -xor clause-adding function addXorClause() in that it assumes that the variables -inside are decision variables, have not been replaced, eliminated, etc. -*/ -template<class T> -XorClause* Solver::addXorClauseInt(T& ps, bool xorEqualFalse, const bool learnt) throw (std::out_of_range) -{ - assert(qhead == trail.size()); - assert(decisionLevel() == 0); - - if (ps.size() > (0x01UL << 18)) - throw std::out_of_range("Too long clause!"); - std::sort(ps.getData(), ps.getDataEnd()); - Lit p; - uint32_t i, j; - for (i = j = 0, p = lit_Undef; i != ps.size(); i++) { - if (ps[i].var() == p.var()) { - //added, but easily removed - j--; - p = lit_Undef; - if (!assigns[ps[i].var()].isUndef()) - xorEqualFalse ^= assigns[ps[i].var()].getBool(); - } else if (assigns[ps[i].var()].isUndef()) { //just add - ps[j++] = p = ps[i]; - assert(!subsumer->getVarElimed()[p.var()]); - assert(!xorSubsumer->getVarElimed()[p.var()]); - } else //modify xorEqualFalse instead of adding - xorEqualFalse ^= (assigns[ps[i].var()].getBool()); - } - ps.shrink(i - j); - - switch(ps.size()) { - case 0: { - if (!xorEqualFalse) ok = false; - return NULL; - } - case 1: { - uncheckedEnqueue(Lit(ps[0].var(), xorEqualFalse)); - ok = (propagate<false>().isNULL()); - return NULL; - } - case 2: { - #ifdef VERBOSE_DEBUG - cout << "--> xor is 2-long, replacing var " << ps[0].var()+1 << " with " << (!xorEqualFalse ? "-" : "") << ps[1].var()+1 << endl; - #endif - - ps[0] = ps[0].unsign(); - ps[1] = ps[1].unsign(); - varReplacer->replace(ps, xorEqualFalse, learnt); - return NULL; - } - default: { - assert(!learnt); - XorClause* c = clauseAllocator.XorClause_new(ps, xorEqualFalse); - attachClause(*c); - return c; - } - } -} - -template XorClause* Solver::addXorClauseInt(vec<Lit>& ps, bool xorEqualFalse, const bool learnt); -template XorClause* Solver::addXorClauseInt(XorClause& ps, bool xorEqualFalse, const bool learnt); - -/** -@brief Adds an xor clause to the problem - -Calls addXorClauseInt() for the heavy-lifting. Basically, this does a bit -of debug-related stuff (see "libraryCNFFile"), and then checks if any of the -variables have been eliminated, replaced, etc. If so, it treats it correctly, -and then calls addXorClauseInt() to actually add the xor clause. - -@p ps[inout] The VARIABLES in the xor clause. Beware, there must be NO signs - here: ALL must be unsigned (.sign() == false). Values passed here - WILL be changed, ordered, removed, etc! -@p xorEqualFalse The xor must be equal to TRUE or false? -*/ -template<class T> -bool Solver::addXorClause(T& ps, bool xorEqualFalse) throw (std::out_of_range) -{ - assert(decisionLevel() == 0); - if (ps.size() > (0x01UL << 18)) - throw std::out_of_range("Too long clause!"); - - if (libraryCNFFile) { - fprintf(libraryCNFFile, "x"); - for (uint32_t i = 0; i < ps.size(); i++) ps[i].print(libraryCNFFile); - fprintf(libraryCNFFile, "0\n"); - } - - if (!ok) - return false; - assert(qhead == trail.size()); - #ifndef NDEBUG - for (Lit *l = ps.getData(), *end = ps.getDataEnd(); l != end; l++) { - assert(l->var() < nVars() && "Clause inserted, but variable inside has not been declared with newVar()!"); - } - #endif - - if (varReplacer->getNumLastReplacedVars() || subsumer->getNumElimed() || xorSubsumer->getNumElimed()) { - for (uint32_t i = 0; i != ps.size(); i++) { - Lit otherLit = varReplacer->getReplaceTable()[ps[i].var()]; - if (otherLit.var() != ps[i].var()) { - ps[i] = Lit(otherLit.var(), false); - xorEqualFalse ^= otherLit.sign(); - } - if (subsumer->getVarElimed()[ps[i].var()] && !subsumer->unEliminate(ps[i].var())) - return false; - else if (xorSubsumer->getVarElimed()[ps[i].var()] && !xorSubsumer->unEliminate(ps[i].var())) - return false; - } - } - - XorClause* c = addXorClauseInt(ps, xorEqualFalse); - if (c != NULL) xorclauses.push(c); - - return ok; -} - -template bool Solver::addXorClause(vec<Lit>& ps, bool xorEqualFalse); -template bool Solver::addXorClause(XorClause& ps, bool xorEqualFalse); - -/** -@brief Adds a clause to the problem. Should ONLY be called internally - -This code is very specific in that it must NOT be called with varibles in -"ps" that have been replaced, eliminated, etc. Also, it must not be called -when the solver is in an UNSAT (!ok) state, for example. Use it carefully, -and only internally -*/ -template <class T> -Clause* Solver::addClauseInt(T& ps - , const bool learnt, const uint32_t glue, const float miniSatActivity - , const bool inOriginalInput) -{ - assert(ok); -#ifdef VERBOSE_DEBUG - std::cout << "Adding new clause: " << std::endl; - for(size_t i = 0; i< ps.size(); i++) { - printLit(ps[i]); - std::cout << " "; - } - std::cout << std::endl; -#endif //VERBOSE_DEBUG - - std::sort(ps.getData(), ps.getDataEnd()); - Lit p = lit_Undef; - uint32_t i, j; - for (i = j = 0; i != ps.size(); i++) { - if (value(ps[i]).getBool() || ps[i] == ~p) - return NULL; - else if (value(ps[i]) != l_False && ps[i] != p) { - ps[j++] = p = ps[i]; - assert(!subsumer->getVarElimed()[p.var()]); - assert(!xorSubsumer->getVarElimed()[p.var()]); - } - } - ps.shrink(i - j); - - if (ps.size() == 0) { - ok = false; - return NULL; - } else if (ps.size() == 1) { - uncheckedEnqueue(ps[0]); - ok = (propagate<false>().isNULL()); - return NULL; - } - - if (ps.size() > 2) { - Clause* c = clauseAllocator.Clause_new(ps); - if (learnt) c->makeLearnt(glue, miniSatActivity); - attachClause(*c); - return c; - } else { - attachBinClause(ps[0], ps[1], learnt); - if (!inOriginalInput) dataSync->signalNewBinClause(ps); - numNewBin++; - return NULL; - } -} - -template Clause* Solver::addClauseInt(Clause& ps, const bool learnt, const uint32_t glue, const float miniSatActivity, const bool inOriginalInput); -template Clause* Solver::addClauseInt(vec<Lit>& ps, const bool learnt, const uint32_t glue, const float miniSatActivity, const bool inOriginalInput); - -template<class T> bool Solver::addClauseHelper(T& ps) throw (std::out_of_range) -{ - assert(decisionLevel() == 0); - if (ps.size() > (0x01UL << 18)) - throw std::out_of_range("Too long clause!"); - - if (libraryCNFFile) { - for (uint32_t i = 0; i != ps.size(); i++) ps[i].print(libraryCNFFile); - fprintf(libraryCNFFile, "0\n"); - } - - if (!ok) return false; - assert(qhead == trail.size()); - #ifndef NDEBUG - for (Lit *l = ps.getData(), *end = ps.getDataEnd(); l != end; l++) { - assert(l->var() < nVars() && "Clause inserted, but variable inside has not been declared with Solver::newVar() !"); - } - #endif - - // Check if clause is satisfied and remove false/duplicate literals: - if (varReplacer->getNumLastReplacedVars() || subsumer->getNumElimed() || xorSubsumer->getNumElimed()) { - for (uint32_t i = 0; i != ps.size(); i++) { - ps[i] = varReplacer->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); - if (subsumer->getVarElimed()[ps[i].var()] && !subsumer->unEliminate(ps[i].var())) - return false; - if (xorSubsumer->getVarElimed()[ps[i].var()] && !xorSubsumer->unEliminate(ps[i].var())) - return false; - } - } - - for (uint32_t i = 0; i < ps.size(); i++) { - std::swap(ps[i], ps[(mtrand.randInt() % (ps.size()-i)) + i]); - } - - return true; -} - - -/** -@brief Adds a clause to the problem. Calls addClauseInt() for heavy-lifting - -Does some debug-related stuff (see "libraryCNFFile"), and checks whether the -variables of the literals in "ps" have been eliminated/replaced etc. If so, -it acts on them such that they are correct, and calls addClauseInt() to do -the heavy-lifting -*/ -template<class T> -bool Solver::addClause(T& ps) -{ - #ifdef VERBOSE_DEBUG - std::cout << "addClause() called with new clause: " << ps << std::endl; - #endif //VERBOSE_DEBUG - if (!addClauseHelper(ps)) return false; - Clause* c = addClauseInt(ps, false, 0, 0, true); - if (c != NULL) clauses.push(c); - - return ok; -} - -template bool Solver::addClause(vec<Lit>& ps); -template bool Solver::addClause(Clause& ps); - - -template<class T> -bool Solver::addLearntClause(T& ps, const uint32_t glue, const float miniSatActivity) -{ - if (!addClauseHelper(ps)) return false; - Clause* c = addClauseInt(ps, true, glue, miniSatActivity, true); - if (c != NULL) learnts.push(c); - - return ok; -} - -template bool Solver::addLearntClause(vec<Lit>& ps, const uint32_t glue, const float miniSatActivity); -template bool Solver::addLearntClause(Clause& ps, const uint32_t glue, const float miniSatActivity); - - -/** -@brief Attaches an xor clause to the watchlists - -The xor clause must be larger than 2, since a 2-long XOR clause is a varible -replacement instruction, really. -*/ -void Solver::attachClause(XorClause& c) -{ - assert(c.size() > 2); - #ifdef DEBUG_ATTACH - assert(assigns[c[0].var()] == l_Undef); - assert(assigns[c[1].var()] == l_Undef); - - for (uint32_t i = 0; i < c.size(); i++) { - assert(!subsumer->getVarElimed()[c[i].var()]); - assert(!xorSubsumer->getVarElimed()[c[i].var()]); - } - #endif //DEBUG_ATTACH - - watches[Lit(c[0].var(), false).toInt()].push(clauseAllocator.getOffset((Clause*)&c)); - watches[Lit(c[0].var(), true).toInt()].push(clauseAllocator.getOffset((Clause*)&c)); - watches[Lit(c[1].var(), false).toInt()].push(clauseAllocator.getOffset((Clause*)&c)); - watches[Lit(c[1].var(), true).toInt()].push(clauseAllocator.getOffset((Clause*)&c)); - - clauses_literals += c.size(); -} - -void Solver::attachBinClause(const Lit lit1, const Lit lit2, const bool learnt) -{ - #ifdef DEBUG_ATTACH - assert(lit1.var() != lit2.var()); - assert(assigns[lit1.var()] == l_Undef); - assert(value(lit2) == l_Undef || value(lit2) == l_False); - - assert(!subsumer->getVarElimed()[lit1.var()]); - assert(!subsumer->getVarElimed()[lit2.var()]); - - assert(!xorSubsumer->getVarElimed()[lit1.var()]); - assert(!xorSubsumer->getVarElimed()[lit2.var()]); - #endif //DEBUG_ATTACH - - watches[(~lit1).toInt()].push(Watched(lit2, learnt)); - watches[(~lit2).toInt()].push(Watched(lit1, learnt)); - - #ifdef DUMP_STATS_FULL - if (learnt) { - watches[(~lit1).toInt()].last().glue = 2; - watches[(~lit2).toInt()].last().glue = 2; - } else { - watches[(~lit1).toInt()].last().glue = -1; - watches[(~lit2).toInt()].last().glue = -1; - } - #endif - - numBins++; - if (learnt) learnts_literals += 2; - else clauses_literals += 2; -} - -/** -@brief Attach normal a clause to the watchlists - -Handles 2, 3 and >3 clause sizes differently and specially -*/ -void Solver::attachClause(Clause& c) -{ - assert(c.size() > 2); - #ifdef DEBUG_ATTACH - assert(c[0].var() != c[1].var()); - assert(assigns[c[0].var()] == l_Undef); - assert(value(c[1]) == l_Undef || value(c[1]) == l_False); - - for (uint32_t i = 0; i < c.size(); i++) { - assert(!subsumer->getVarElimed()[c[i].var()]); - assert(!xorSubsumer->getVarElimed()[c[i].var()]); - } - #endif //DEBUG_ATTACH - - if (c.size() == 3) { - watches[(~c[0]).toInt()].push(Watched(c[1], c[2])); - watches[(~c[1]).toInt()].push(Watched(c[0], c[2])); - watches[(~c[2]).toInt()].push(Watched(c[0], c[1])); - - #ifdef DUMP_STATS_FULL - if (c.learnt()) { - watches[(~c[0]).toInt()].last().glue = 2; - watches[(~c[1]).toInt()].last().glue = 2; - watches[(~c[2]).toInt()].last().glue = 2; - } else { - watches[(~c[0]).toInt()].last().glue = -1; - watches[(~c[1]).toInt()].last().glue = -1; - watches[(~c[2]).toInt()].last().glue = -1; - } - #endif - - } else { - ClauseOffset offset = clauseAllocator.getOffset(&c); - watches[(~c[0]).toInt()].push(Watched(offset, c[c.size()/2])); - watches[(~c[1]).toInt()].push(Watched(offset, c[c.size()/2])); - } - - if (c.learnt()) - learnts_literals += c.size(); - else - clauses_literals += c.size(); -} - -/** -@brief Calls detachModifiedClause to do the heavy-lifting -*/ -void Solver::detachClause(const XorClause& c) -{ - detachModifiedClause(c[0].var(), c[1].var(), c.size(), &c); -} - -/** -@brief Calls detachModifiedClause to do the heavy-lifting -*/ -void Solver::detachClause(const Clause& c) -{ - detachModifiedClause(c[0], c[1], (c.size() == 3) ? c[2] : lit_Undef, c.size(), &c); -} - -/** -@brief Detaches a (potentially) modified clause - -The first two literals might have chaned through modification, so they are -passed along as arguments -- they are needed to find the correct place where -the clause is -*/ -void Solver::detachModifiedClause(const Lit lit1, const Lit lit2, const Lit lit3, const uint32_t origSize, const Clause* address) -{ - assert(origSize > 2); - - ClauseOffset offset = clauseAllocator.getOffset(address); - if (origSize == 3) { - //The clause might have been longer, and has only recently - //became 3-long. Check, and detach accordingly - if (findWCl(watches[(~lit1).toInt()], offset)) goto fullClause; - - removeWTri(watches[(~lit1).toInt()], lit2, lit3); - removeWTri(watches[(~lit2).toInt()], lit1, lit3); - removeWTri(watches[(~lit3).toInt()], lit1, lit2); - - } else { - fullClause: - removeWCl(watches[(~lit1).toInt()], offset); - removeWCl(watches[(~lit2).toInt()], offset); - - } - - if (address->learnt()) - learnts_literals -= origSize; - else - clauses_literals -= origSize; -} - -/** -@brief Detaches a (potentially) modified xor clause - -The first two vars might have chaned through modification, so they are passed -along as arguments. -*/ -void Solver::detachModifiedClause(const Var var1, const Var var2, const uint32_t origSize, const XorClause* address) -{ - assert(origSize > 2); - - ClauseOffset offset = clauseAllocator.getOffset(address); - assert(findWXCl(watches[Lit(var1, false).toInt()], offset)); - assert(findWXCl(watches[Lit(var1, true).toInt()], offset)); - assert(findWXCl(watches[Lit(var2, false).toInt()], offset)); - assert(findWXCl(watches[Lit(var2, true).toInt()], offset)); - - removeWXCl(watches[Lit(var1, false).toInt()], offset); - removeWXCl(watches[Lit(var1, true).toInt()], offset); - removeWXCl(watches[Lit(var2, false).toInt()], offset); - removeWXCl(watches[Lit(var2, true).toInt()], offset); - - assert(!address->learnt()); - clauses_literals -= origSize; -} - -/** -@brief Revert to the state at given level - -Also reverts all stuff in Gass-elimination -*/ -void Solver::cancelUntil(int level) -{ - #ifdef VERBOSE_DEBUG - cout << "Canceling until level " << level; - if (level > 0) cout << " sublevel: " << trail_lim[level]; - cout << endl; - #endif - - if ((int)decisionLevel() > level) { - - #ifdef USE_GAUSS - for (vector<Gaussian*>::iterator gauss = gauss_matrixes.begin(), end= gauss_matrixes.end(); gauss != end; gauss++) - (*gauss)->canceling(trail_lim[level]); - #endif //USE_GAUSS - - for (int sublevel = trail.size()-1; sublevel >= (int)trail_lim[level]; sublevel--) { - Var var = trail[sublevel].var(); - #ifdef VERBOSE_DEBUG - cout << "Canceling var " << var+1 << " sublevel: " << sublevel << endl; - #endif - assigns[var] = l_Undef; - #ifdef ANIMATE3D - fprintf(stderr, "u %u\n", var); - #endif - insertVarOrder(var); - #ifdef ENABLE_UNWIND_GLUE - if (unWindGlue[var] != NULL) { - #ifdef UNWINDING_DEBUG - std::cout << "unwind, var:" << var - << " sublevel:" << sublevel - << " coming from:" << (trail.size()-1) - << " going until:" << (int)trail_lim[level] - << std::endl; - unWindGlue[var]->plainPrint(); - #endif //UNWINDING_DEBUG - - Clause*& clauseToFree = unWindGlue[var]; - detachClause(*clauseToFree); - clauseAllocator.clauseFree(clauseToFree); - clauseToFree = NULL; - } - #endif //ENABLE_UNWIND_GLUE - } - qhead = trail_lim[level]; - trail.shrink_(trail.size() - trail_lim[level]); - trail_lim.shrink_(trail_lim.size() - level); - } - - #ifdef VERBOSE_DEBUG - cout << "Canceling finished. (now at level: " << decisionLevel() << " sublevel: " << trail.size()-1 << ")" << endl; - #endif -} - -void Solver::cancelUntilLight() -{ - assert((int)decisionLevel() > 0); - - for (int sublevel = trail.size()-1; sublevel >= (int)trail_lim[0]; sublevel--) { - Var var = trail[sublevel].var(); - assigns[var] = l_Undef; - } - qhead = trail_lim[0]; - trail.shrink_(trail.size() - trail_lim[0]); - trail_lim.clear(); -} - -bool Solver::clearGaussMatrixes() -{ - assert(decisionLevel() == 0); - #ifdef USE_GAUSS - bool ret = gauss_matrixes.size() > 0; - for (uint32_t i = 0; i < gauss_matrixes.size(); i++) - delete gauss_matrixes[i]; - gauss_matrixes.clear(); - - for (uint32_t i = 0; i != freeLater.size(); i++) - clauseAllocator.clauseFree(freeLater[i]); - freeLater.clear(); - - return ret; - #endif //USE_GAUSS - return false; -} - -/** -@brief Returns what polarity[] should be set as default based on polarity_mode - -since polarity is filled with Lit::sign() , "true" here means an inverted -signed-ness, i.e. a FALSE default value. And vice-versa -*/ -inline bool Solver::defaultPolarity() -{ - switch(conf.polarity_mode) { - case polarity_false: - return true; - case polarity_true: - return false; - case polarity_rnd: - return mtrand.randInt(1); - case polarity_auto: - return true; - default: - assert(false); - } - - return true; -} - -/** -@brief Tally votes for a default TRUE or FALSE value for the variable using the Jeroslow-Wang method - -@p votes[inout] Votes are tallied at this place for each variable -@p cs The clause to tally votes for -*/ -void Solver::tallyVotes(const vec<Clause*>& cs, vec<double>& votes) const -{ - for (const Clause * const*it = cs.getData(), * const*end = it + cs.size(); it != end; it++) { - const Clause& c = **it; - if (c.learnt()) continue; - - double divider; - if (c.size() > 63) divider = 0.0; - else divider = 1.0/(double)((uint64_t)1<<(c.size()-1)); - - for (const Lit *it2 = c.getData(), *end2 = c.getDataEnd(); it2 != end2; it2++) { - if (it2->sign()) votes[it2->var()] += divider; - else votes[it2->var()] -= divider; - } - } -} - -void Solver::tallyVotesBin(vec<double>& votes) const -{ - uint32_t wsLit = 0; - for (const vec<Watched> *it = watches.getData(), *end = watches.getDataEnd(); it != end; it++, wsLit++) { - Lit lit = ~Lit::toLit(wsLit); - const vec<Watched>& ws = *it; - for (vec<Watched>::const_iterator it2 = ws.getData(), end2 = ws.getDataEnd(); it2 != end2; it2++) { - if (it2->isBinary() && lit.toInt() < it2->getOtherLit().toInt()) { - if (!it2->getLearnt()) { - if (lit.sign()) votes[lit.var()] += 0.5; - else votes[lit.var()] -= 0.5; - - Lit lit2 = it2->getOtherLit(); - if (lit2.sign()) votes[lit2.var()] += 0.5; - else votes[lit2.var()] -= 0.5; - } - } - } - } -} - -/** -@brief Tally votes a default TRUE or FALSE value for the variable using the Jeroslow-Wang method - -For XOR clause, we simply add some weight for a FALSE default, i.e. being in -xor clauses makes the variabe more likely to be FALSE by default -*/ -void Solver::tallyVotes(const vec<XorClause*>& cs, vec<double>& votes) const -{ - for (const XorClause * const*it = cs.getData(), * const*end = it + cs.size(); it != end; it++) { - const XorClause& c = **it; - double divider; - if (c.size() > 63) divider = 0.0; - else divider = 1.0/(double)((uint64_t)1<<(c.size()-1)); - - for (const Lit *it2 = c.getData(), *end2 = c.getDataEnd(); it2 != end2; it2++) { - votes[it2->var()] += divider; - } - } -} - -/** -@brief Tallies votes for a TRUE/FALSE default polarity using Jeroslow-Wang - -Voting is only used if polarity_mode is "polarity_auto". This is the default. -Uses the tallyVotes() functions to tally the votes -*/ -void Solver::calculateDefaultPolarities() -{ - #ifdef VERBOSE_DEBUG_POLARITIES - std::cout << "Default polarities: " << std::endl; - #endif - - assert(decisionLevel() == 0); - if (conf.polarity_mode == polarity_auto) { - double myTime = cpuTime(); - - vec<double> votes(nVars(), 0.0); - - tallyVotes(clauses, votes); - tallyVotesBin(votes); - tallyVotes(xorclauses, votes); - - Var i = 0; - uint32_t posPolars = 0; - uint32_t undecidedPolars = 0; - for (const double *it = votes.getData(), *end = votes.getDataEnd(); it != end; it++, i++) { - polarity[i] = (*it >= 0.0); - posPolars += (*it < 0.0); - undecidedPolars += (*it == 0.0); - #ifdef VERBOSE_DEBUG_POLARITIES - std::cout << !defaultPolarities[i] << ", "; - #endif //VERBOSE_DEBUG_POLARITIES - } - - if (conf.verbosity >= 2) { - std::cout << "c Calc default polars - " - << " time: " << std::fixed << std::setw(6) << std::setprecision(2) << (cpuTime() - myTime) << " s" - << " pos: " << std::setw(7) << posPolars - << " undec: " << std::setw(7) << undecidedPolars - << " neg: " << std::setw(7) << nVars()- undecidedPolars - posPolars - << std:: endl; - } - } else { - for (uint32_t i = 0; i < polarity.size(); i++) { - polarity[i] = defaultPolarity(); - } - } - - #ifdef VERBOSE_DEBUG_POLARITIES - std::cout << std::endl; - #endif //VERBOSE_DEBUG_POLARITIES -} - -void Solver::calcReachability() -{ - double myTime = cpuTime(); - - for (uint32_t i = 0; i < nVars()*2; i++) { - litReachable[i] = LitReachData(); - } - - for (uint32_t i = 0; i < order_heap.size(); i++) for (uint32_t sig1 = 0; sig1 < 2; sig1++) { - Lit lit = Lit(order_heap[i], sig1); - if (value(lit.var()) != l_Undef - || subsumer->getVarElimed()[lit.var()] - || xorSubsumer->getVarElimed()[lit.var()] - || !decision_var[lit.var()]) - continue; - - vector<Lit>& cache = transOTFCache[(~lit).toInt()].lits; - uint32_t cacheSize = cache.size(); - for (vector<Lit>::const_iterator it = cache.begin(), end = cache.end(); it != end; it++) { - /*if (solver.value(it->var()) != l_Undef - || solver.subsumer->getVarElimed()[it->var()] - || solver.xorSubsumer->getVarElimed()[it->var()]) - continue;*/ - if ((*it == lit) || (*it == ~lit)) continue; - if (litReachable[it->toInt()].lit == lit_Undef || litReachable[it->toInt()].numInCache < cacheSize) { - litReachable[it->toInt()].lit = lit; - litReachable[it->toInt()].numInCache = cacheSize; - } - } - } - - /*for (uint32_t i = 0; i < nVars()*2; i++) { - std::sort(litReachable[i].begin(), litReachable[i].end(), MySorterX(transOTFCache)); - }*/ - - /*for (uint32_t i = 0; i < nVars()*2; i++) { - vector<Lit>& myset = litReachable[i]; - for (uint32_t i2 = 0; i2 < myset.size(); i2++) { - std::cout << transOTFCache[myset[i2].toInt()].lits.size() << " , "; - } - std::cout << std::endl; - }*/ - - if (conf.verbosity >= 1) { - std::cout << "c calculated reachability. Time: " << (cpuTime() - myTime) << std::endl; - } -} - -void Solver::saveOTFData() -{ - assert(decisionLevel() == 1); - - Lit lev0Lit = trail[trail_lim[0]]; - Solver::TransCache& oTFCache = transOTFCache[(~lev0Lit).toInt()]; - oTFCache.conflictLastUpdated = conflicts; - oTFCache.lits.clear(); - - for (int sublevel = trail.size()-1; sublevel > (int)trail_lim[0]; sublevel--) { - Lit lit = trail[sublevel]; - oTFCache.lits.push_back(lit); - } -} - -//********************************** -// Major methods: -//********************************** - -/** -@brief Picks a branching variable and its value (True/False) - -We do three things here: --# Try to do random decision (rare, less than 2%) --# Try acitivity-based decision - -Then, we pick a sign (True/False): -\li If we are in search-burst mode ("simplifying" is set), we pick a sign -totally randomly -\li Otherwise, we simply take the saved polarity -*/ -Lit Solver::pickBranchLit() -{ - #ifdef VERBOSE_DEBUG - cout << "decision level: " << decisionLevel() << " "; - #endif - - Var next = var_Undef; - - /* Skip variables which have already been defined (this will usually happen - * because of propagations/implicit assignments) */ - for (unsigned int i = decisionLevel(); i < branching_variables.size(); ++i) { - Var v = branching_variables[i]; - if (v < nVars() - && !subsumer->getVarElimed()[v] - && !xorSubsumer->getVarElimed()[v] - && assigns[v] == l_Undef) { - next = v; - break; - } - } - - bool random = mtrand.randDblExc() < conf.random_var_freq; - - // Random decision: - if (next == var_Undef && random && !order_heap.empty()) { - if (conf.restrictPickBranch == 0) - next = order_heap[mtrand.randInt(order_heap.size()-1)]; - else - next = order_heap[mtrand.randInt(std::min((uint32_t)order_heap.size()-1, conf.restrictPickBranch))]; - - if (assigns[next] == l_Undef && decision_var[next]) - rnd_decisions++; - } - - bool signSet = false; - bool signSetTo = false; - // Activity based decision: - while (next == var_Undef - || assigns[next] != l_Undef - || !decision_var[next]) { - if (order_heap.empty()) { - next = var_Undef; - break; - } - - next = order_heap.removeMin(); - if (!simplifying && value(next) == l_Undef && decision_var[next]) { - signSet = true; - if (avgBranchDepth.isvalid()) - signSetTo = polarity[next] ^ (mtrand.randInt(avgBranchDepth.getAvgUInt() * ((lastSelectedRestartType == static_restart) ? 2 : 1) ) == 1); - else - signSetTo = polarity[next]; - Lit nextLit = Lit(next, signSetTo); - Lit lit2 = litReachable[nextLit.toInt()].lit; - if (lit2 != lit_Undef && value(lit2.var()) == l_Undef && decision_var[lit2.var()] && mtrand.randInt(1) == 1) { - insertVarOrder(next); - next = litReachable[nextLit.toInt()].lit.var(); - signSetTo = litReachable[nextLit.toInt()].lit.sign(); - } - } - } - - //if "simplifying" is set, i.e. if we are in a burst-search mode, then - //randomly pick a sign. Otherwise, if RANDOM_LOOKAROUND_SEARCHSPACE is - //defined, we check the default polarity, and we may change it a bit - //randomly based on the average branch depth. Otherwise, we just go for the - //polarity that has been saved - bool sign; - if (next != var_Undef) { - if (signSet) { - sign = signSetTo; - } else { - if (simplifying && random) - sign = mtrand.randInt(1); - else if (avgBranchDepth.isvalid()) - sign = polarity[next] ^ (mtrand.randInt(avgBranchDepth.getAvgUInt() * ((lastSelectedRestartType == static_restart) ? 2 : 1) ) == 1); - else - sign = polarity[next]; - } - } - - assert(next == var_Undef || value(next) == l_Undef); - - if (next == var_Undef) { - #ifdef VERBOSE_DEBUG - cout << "SAT!" << endl; - #endif - return lit_Undef; - } else { - Lit lit(next,sign); - #ifdef VERBOSE_DEBUG - assert(decision_var[lit.var()]); - cout << "decided on: " << lit.var()+1 << " to set:" << !lit.sign() << endl; - #endif - return lit; - } -} - -/** -@brief Checks subsumption. Used in on-the-fly subsumption code - -Assumes 'seen' is cleared (will leave it cleared) -*/ -template<class T1, class T2> -bool subset(const T1& A, const T2& B, vector<char>& seen) -{ - for (uint32_t i = 0; i != B.size(); i++) - seen[B[i].toInt()] = 1; - for (uint32_t i = 0; i != A.size(); i++) { - if (!seen[A[i].toInt()]) { - for (uint32_t i = 0; i != B.size(); i++) - seen[B[i].toInt()] = 0; - return false; - } - } - for (uint32_t i = 0; i != B.size(); i++) - seen[B[i].toInt()] = 0; - return true; -} - - -/** -@brief Analyze conflict and produce a reason clause. - -Pre-conditions: -\li 'out_learnt' is assumed to be cleared. -\li Current decision level must be greater than root level. - -Post-conditions: -\li 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. - -Effect: Will undo part of the trail, upto but not beyond the assumption of the -current decision level. - -@return NULL if the conflict doesn't on-the-fly subsume the last clause, and -the pointer of the clause if it does -*/ -Clause* Solver::analyze(PropBy conflHalf, vec<Lit>& out_learnt, int& out_btlevel, uint32_t &glue, const bool update) -{ - int pathC = 0; - Lit p = lit_Undef; - - // Generate conflict clause: - // - out_learnt.push(); // (leave room for the asserting literal) - int index = trail.size() - 1; - out_btlevel = 0; - - PropByFull confl(conflHalf, failBinLit, clauseAllocator); - PropByFull oldConfl; - - do { - assert(!confl.isNULL()); // (otherwise should be UIP) - - if (update && restartType == static_restart && confl.isClause() && confl.getClause()->learnt()) - claBumpActivity(*confl.getClause()); - - for (uint32_t j = (p == lit_Undef) ? 0 : 1, size = confl.size(); j != size; j++) { - Lit q = confl[j]; - const Var my_var = q.var(); - - if (!seen[my_var] && level[my_var] > 0) { - varBumpActivity(my_var); - seen[my_var] = 1; - assert(level[my_var] <= (int)decisionLevel()); - if (level[my_var] >= (int)decisionLevel()) { - pathC++; - if (lastSelectedRestartType == dynamic_restart - && reason[q.var()].isClause() - && !reason[q.var()].isNULL() - && clauseAllocator.getPointer(reason[q.var()].getClause())->learnt()) - lastDecisionLevel.push(q.var()); - } else { - out_learnt.push(q); - if (level[my_var] > out_btlevel) - out_btlevel = level[my_var]; - } - } - } - - // Select next clause to look at: - while (!seen[trail[index--].var()]); - p = trail[index+1]; - oldConfl = confl; - confl = PropByFull(reason[p.var()], failBinLit, clauseAllocator); - if (confl.isClause()) __builtin_prefetch(confl.getClause()); - seen[p.var()] = 0; - pathC--; - - } while (pathC > 0); - assert(pathC == 0); - out_learnt[0] = ~p; - - // Simplify conflict clause: - // - uint32_t i, j; - if (conf.expensive_ccmin) { - uint32_t abstract_level = 0; - for (i = 1; i < out_learnt.size(); i++) - abstract_level |= abstractLevel(out_learnt[i].var()); // (maintain an abstraction of levels involved in conflict) - - out_learnt.copyTo(analyze_toclear); - for (i = j = 1; i < out_learnt.size(); i++) - if (reason[out_learnt[i].var()].isNULL() || !litRedundant(out_learnt[i], abstract_level)) - out_learnt[j++] = out_learnt[i]; - } else { - out_learnt.copyTo(analyze_toclear); - for (i = j = 1; i < out_learnt.size(); i++) { - PropByFull c(reason[out_learnt[i].var()], failBinLit, clauseAllocator); - - for (uint32_t k = 1, size = c.size(); k < size; k++) { - if (!seen[c[k].var()] && level[c[k].var()] > 0) { - out_learnt[j++] = out_learnt[i]; - break; - } - } - } - } - max_literals += out_learnt.size(); - out_learnt.shrink(i - j); - for (uint32_t j = 0; j != analyze_toclear.size(); j++) - seen[analyze_toclear[j].var()] = 0; // ('seen[]' is now cleared) - - if (conf.doMinimLearntMore && out_learnt.size() > 1) - minimiseLeartFurther(out_learnt, calcNBLevels(out_learnt)); - - glue = calcNBLevels(out_learnt); - tot_literals += out_learnt.size(); - - // Find correct backtrack level: - // - if (out_learnt.size() == 1) - out_btlevel = 0; - else { - uint32_t max_i = 1; - for (uint32_t i = 2; i < out_learnt.size(); i++) - if (level[out_learnt[i].var()] > level[out_learnt[max_i].var()]) - max_i = i; - std::swap(out_learnt[max_i], out_learnt[1]); - out_btlevel = level[out_learnt[1].var()]; - } - - if (lastSelectedRestartType == dynamic_restart) { - #ifdef UPDATE_VAR_ACTIVITY_BASED_ON_GLUE - for(uint32_t i = 0; i != lastDecisionLevel.size(); i++) { - PropBy cl = reason[lastDecisionLevel[i]]; - if (cl.isClause() && clauseAllocator.getPointer(cl.getClause())->getGlue() < glue) - varBumpActivity(lastDecisionLevel[i]); - } - lastDecisionLevel.clear(); - #endif - } - - //We can only on-the-fly subsume clauses that are not 2- or 3-long - //furthermore, we cannot subsume a clause that is marked for deletion - //due to its high glue value - if (!conf.doOTFSubsume - || out_learnt.size() == 1 - || !oldConfl.isClause() - || oldConfl.getClause()->isXor() - #ifdef ENABLE_UNWIND_GLUE - || (conf.doMaxGlueDel && oldConfl.getClause()->getGlue() > conf.maxGlue) - #endif //ENABLE_UNWIND_GLUE - || out_learnt.size() >= oldConfl.getClause()->size()) return NULL; - - if (!subset(out_learnt, *oldConfl.getClause(), seen)) return NULL; - - improvedClauseNo++; - improvedClauseSize += oldConfl.getClause()->size() - out_learnt.size(); - return oldConfl.getClause(); -} - -/** -@brief Performs on-the-fly self-subsuming resolution - -Only uses binary and tertiary clauses already in the watchlists in native -form to carry out the forward-self-subsuming resolution -*/ -void Solver::minimiseLeartFurther(vec<Lit>& cl, const uint32_t glue) -{ - //80 million is kind of a hack. It seems that the longer the solving - //the slower this operation gets. So, limiting the "time" with total - //number of conflict literals is maybe a good way of doing this - bool clDoMinLRec = false; - if (conf.doCacheOTFSSR && conf.doMinimLMoreRecur) { - switch(lastSelectedRestartType) { - case dynamic_restart : - clDoMinLRec |= glue < 0.6*glueHistory.getAvgAllDouble(); - //NOTE: No "break;" here on purpose - case static_restart : - clDoMinLRec |= cl.size() < 0.6*conflSizeHist.getAvgDouble(); - break; - default : - assert(false); - } - } - - if (clDoMinLRec) moreRecurMinLDo++; - uint64_t thisUpdateTransOTFSSCache = UPDATE_TRANSOTFSSR_CACHE; - if (tot_literals > 80000000) thisUpdateTransOTFSSCache *= 2; - - //To count the "amount of time" invested in doing transitive on-the-fly - //self-subsuming resolution - uint32_t moreRecurProp = 0; - - for (uint32_t i = 0; i < cl.size(); i++) seen[cl[i].toInt()] = 1; - for (Lit *l = cl.getData(), *end = cl.getDataEnd(); l != end; l++) { - if (seen[l->toInt()] == 0) continue; - Lit lit = *l; - - if (clDoMinLRec) { - if (moreRecurProp > 450 - || (transOTFCache[l->toInt()].conflictLastUpdated != std::numeric_limits<uint64_t>::max() - && (transOTFCache[l->toInt()].conflictLastUpdated + thisUpdateTransOTFSSCache >= conflicts)) - ) { - for (vector<Lit>::const_iterator it = transOTFCache[l->toInt()].lits.begin(), end2 = transOTFCache[l->toInt()].lits.end(); it != end2; it++) { - seen[(~(*it)).toInt()] = 0; - } - } else { - updateTransCache++; - transMinimAndUpdateCache(lit, moreRecurProp); - } - } - - //watched is messed: lit is in watched[~lit] - vec<Watched>& ws = watches[(~lit).toInt()]; - for (vec<Watched>::iterator i = ws.getData(), end = ws.getDataEnd(); i != end; i++) { - if (i->isBinary()) { - seen[(~i->getOtherLit()).toInt()] = 0; - continue; - } - - if (i->isTriClause()) { - if (seen[(~i->getOtherLit()).toInt()] && seen[i->getOtherLit2().toInt()]) { - seen[(~i->getOtherLit()).toInt()] = 0; - } - if (seen[(~i->getOtherLit2()).toInt()] && seen[i->getOtherLit().toInt()]) { - seen[(~i->getOtherLit2()).toInt()] = 0; - } - continue; - } - - //watches are mostly sorted, so it's more-or-less OK to break - // if non-bi or non-tri is encountered - break; - } - } - - uint32_t removedLits = 0; - Lit *i = cl.getData(); - Lit *j= i; - //never remove the 0th literal - seen[cl[0].toInt()] = 1; - for (Lit* end = cl.getDataEnd(); i != end; i++) { - if (seen[i->toInt()]) *j++ = *i; - else removedLits++; - seen[i->toInt()] = 0; - } - numShrinkedClause += (removedLits > 0); - numShrinkedClauseLits += removedLits; - cl.shrink_(i-j); - - #ifdef VERBOSE_DEBUG - std::cout << "c Removed further " << removedLits << " lits" << std::endl; - #endif -} - -void Solver::transMinimAndUpdateCache(const Lit lit, uint32_t& moreRecurProp) -{ - vector<Lit>& allAddedToSeen2 = transOTFCache[lit.toInt()].lits; - allAddedToSeen2.clear(); - - toRecursiveProp.push(lit); - while(!toRecursiveProp.empty()) { - Lit thisLit = toRecursiveProp.top(); - toRecursiveProp.pop(); - //watched is messed: lit is in watched[~lit] - vec<Watched>& ws = watches[(~thisLit).toInt()]; - moreRecurProp += ws.size() +10; - for (vec<Watched>::iterator i = ws.getData(), end = ws.getDataEnd(); i != end; i++) { - if (i->isBinary()) { - moreRecurProp += 5; - Lit otherLit = i->getOtherLit(); - //don't do indefinite recursion, and don't remove "a" when doing self-subsuming-resolution with 'a OR b' - if (seen2[otherLit.toInt()] != 0 || otherLit == ~lit) break; - seen2[otherLit.toInt()] = 1; - allAddedToSeen2.push_back(otherLit); - toRecursiveProp.push(~otherLit); - } else { - break; - } - } - } - assert(toRecursiveProp.empty()); - - for (vector<Lit>::const_iterator it = allAddedToSeen2.begin(), end = allAddedToSeen2.end(); it != end; it++) { - seen[(~(*it)).toInt()] = 0; - seen2[it->toInt()] = 0; - } - - transOTFCache[lit.toInt()].conflictLastUpdated = conflicts; -} - -/** -@brief Check if 'p' can be removed from a learnt clause - -'abstract_levels' is used to abort early if the algorithm is -visiting literals at levels that cannot be removed later. -*/ -bool Solver::litRedundant(Lit p, uint32_t abstract_levels) -{ - analyze_stack.clear(); - analyze_stack.push(p); - int top = analyze_toclear.size(); - while (analyze_stack.size() > 0) { - assert(!reason[analyze_stack.last().var()].isNULL()); - PropByFull c(reason[analyze_stack.last().var()], failBinLit, clauseAllocator); - - analyze_stack.pop(); - - for (uint32_t i = 1, size = c.size(); i < size; i++) { - Lit p = c[i]; - if (!seen[p.var()] && level[p.var()] > 0) { - if (!reason[p.var()].isNULL() && (abstractLevel(p.var()) & abstract_levels) != 0) { - seen[p.var()] = 1; - analyze_stack.push(p); - analyze_toclear.push(p); - } else { - for (uint32_t j = top; j != analyze_toclear.size(); j++) - seen[analyze_toclear[j].var()] = 0; - analyze_toclear.shrink(analyze_toclear.size() - top); - return false; - } - } - } - } - - return true; -} - - -/*_________________________________________________________________________________________________ -| -| analyzeFinal : (p : Lit) -> [void] -| -| Description: -| Specialized analysis procedure to express the final conflict in terms of assumptions. -| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and -| stores the result in 'out_conflict'. -|________________________________________________________________________________________________@*/ -void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) -{ - out_conflict.clear(); - out_conflict.push(p); - - if (decisionLevel() == 0) - return; - - seen[p.var()] = 1; - - for (int32_t i = (int32_t)trail.size()-1; i >= (int32_t)trail_lim[0]; i--) { - Var x = trail[i].var(); - if (seen[x]) { - if (reason[x].isNULL()) { - assert(level[x] > 0); - out_conflict.push(~trail[i]); - } else { - PropByFull c(reason[x], failBinLit, clauseAllocator); - for (uint32_t j = 1, size = c.size(); j < size; j++) - if (level[c[j].var()] > 0) - seen[c[j].var()] = 1; - } - seen[x] = 0; - } - } - - seen[p.var()] = 0; -} - -/*_________________________________________________________________________________________________ -| -| propagate : [void] -> [Clause*] -| -| Description: -| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, -| otherwise NULL. -| -| Post-conditions: -| * the propagation queue is empty, even if there was a conflict. -|________________________________________________________________________________________________@*/ -/** -@brief Propagates a binary clause - -Need to be somewhat tricky if the clause indicates that current assignement -is incorrect (i.e. both literals evaluate to FALSE). If conflict if found, -sets failBinLit -*/ -template<bool full> -inline bool Solver::propBinaryClause(vec<Watched>::iterator &i, const Lit p, PropBy& confl) -{ - lbool val = value(i->getOtherLit()); - if (val.isUndef()) { - if (full) uncheckedEnqueue(i->getOtherLit(), PropBy(p)); - else uncheckedEnqueueLight(i->getOtherLit()); - #ifdef DUMP_STATS_FULL - assert(((i->glue > 0) == i->getLearnt())); - if (full && i->glue > 0 && !simplifying) { - std::cout << "Prop by learnt size: " << 2 << std::endl; - std::cout << "Prop by learnt glue: " << i->glue << std::endl; - } - #endif //DUMP_STATS_FULL - } else if (val == l_False) { - confl = PropBy(p); - failBinLit = i->getOtherLit(); - qhead = trail.size(); - #ifdef DUMP_STATS_FULL - assert(((i->glue > 0) == i->getLearnt())); - if (full && i->glue > 0 && !simplifying) { - std::cout << "Confl by learnt size: " << 2 << std::endl; - std::cout << "Confl by learnt glue: " << i->glue << std::endl; - } - #endif //DUMP_STATS_FULL - - return false; - } - - return true; -} - -/** -@brief Propagates a tertiary (3-long) clause - -Need to be somewhat tricky if the clause indicates that current assignement -is incorrect (i.e. all 3 literals evaluate to FALSE). If conflict is found, -sets failBinLit -*/ -template<bool full> -inline bool Solver::propTriClause(vec<Watched>::iterator &i, const Lit p, PropBy& confl) -{ - lbool val = value(i->getOtherLit()); - if (val == l_True) return true; - - lbool val2 = value(i->getOtherLit2()); - if (val.isUndef() && val2 == l_False) { - if (full) uncheckedEnqueue(i->getOtherLit(), PropBy(p, i->getOtherLit2())); - else uncheckedEnqueueLight(i->getOtherLit()); - #ifdef DUMP_STATS_FULL - assert(conf.isPlain); - if (full && i->glue > 0 && !simplifying) { - std::cout << "Prop by learnt size: " << 3 << std::endl; - std::cout << "Prop by learnt glue: " << i->glue << std::endl; - } - #endif //DUMP_STATS_FULL - } else if (val == l_False && val2.isUndef()) { - if (full) uncheckedEnqueue(i->getOtherLit2(), PropBy(p, i->getOtherLit())); - else uncheckedEnqueueLight(i->getOtherLit2()); - #ifdef DUMP_STATS_FULL - assert(conf.isPlain); - if (full && i->glue > 0 && !simplifying) { - std::cout << "Prop by learnt size: " << 3 << std::endl; - std::cout << "Prop by learnt glue: " << i->glue << std::endl; - } - #endif //DUMP_STATS_FULL - } else if (val == l_False && val2 == l_False) { - confl = PropBy(p, i->getOtherLit2()); - failBinLit = i->getOtherLit(); - qhead = trail.size(); - #ifdef DUMP_STATS_FULL - assert(conf.isPlain); - if (full && i->glue > 0 && !simplifying) { - std::cout << "Confl by learnt size: " << 3 << std::endl; - std::cout << "Confl by learnt glue: " << i->glue << std::endl; - } - #endif //DUMP_STATS_FULL - - return false; - } - - return true; -} - -/** -@brief Propagates a tertiary (3-long) clause - -We have blocked literals in this case in the watchlist. That must be checked -and updated. -*/ -template<bool full> -inline bool Solver::propNormalClause(vec<Watched>::iterator &i, vec<Watched>::iterator &j, const Lit p, PropBy& confl, const bool update) -{ - if (value(i->getBlockedLit()).getBool()) { - // Clause is sat - *j++ = *i; - return true; - } - const uint32_t offset = i->getNormOffset(); - Clause& c = *clauseAllocator.getPointer(offset); - - // Make sure the false literal is data[1]: - if (c[0] == ~p) { - std::swap(c[0], c[1]); - } - - assert(c[1] == ~p); - - // If 0th watch is true, then clause is already satisfied. - if (value(c[0]).getBool()) { - *j = Watched(offset, c[0]); - j++; - return true; - } - // Look for new watch: - for (Lit *k = c.getData() + 2, *end2 = c.getDataEnd(); k != end2; k++) { - if (value(*k) != l_False) { - c[1] = *k; - *k = ~p; - watches[(~c[1]).toInt()].push(Watched(offset, c[0])); - return true; - } - } - - // Did not find watch -- clause is unit under assignment: - *j++ = *i; - if (value(c[0]) == l_False) { - #ifdef DUMP_STATS_FULL - if (full && c.learnt() && !simplifying) { - std::cout << "Confl by learnt size: " << c.size() << std::endl; - std::cout << "Confl by learnt glue: " << c.getGlue() << std::endl; - assert(!conf.isPlain || c.getGlue() > 1); - } - #endif //DUMP_STATS_FULL - confl = PropBy(offset); - qhead = trail.size(); - return false; - } else { - #ifdef DUMP_STATS_FULL - if (full && c.learnt() && !simplifying) { - std::cout << "Prop by learnt size: " << c.size() << std::endl; - std::cout << "Prop by learnt glue: " << c.getGlue() << std::endl; - assert(!conf.isPlain || c.getGlue() > 1); - } - #endif //DUMP_STATS_FULL - - if (full) uncheckedEnqueue(c[0], offset); - else uncheckedEnqueueLight(c[0]); - #ifdef DYNAMICALLY_UPDATE_GLUE - if (update && full && c.learnt() && c.getGlue() > 2) { - uint32_t glue = calcNBLevels(c); - if (glue+1 < c.getGlue()) { - //c.setGlue(std::min(nbLevels, MAX_THEORETICAL_GLUE); - c.setGlue(glue); - } - } - #endif - } - - return true; -} - -/** -@brief Propagates a tertiary (3-long) clause - -Strangely enough, we need to have 4 literals in the wathclists: -for the first two varialbles, BOTH negations (v and ~v). This means quite some -pain, since we need to remove v when moving ~v and vica-versa. However, it means -better memory-accesses since the watchlist is already in the memory... - -\todo maybe not worth it, and a variable-based watchlist should be used -*/ -template<bool full> -inline bool Solver::propXorClause(vec<Watched>::iterator &i, vec<Watched>::iterator &j, const Lit p, PropBy& confl) -{ - ClauseOffset offset = i->getXorOffset(); - XorClause& c = *(XorClause*)clauseAllocator.getPointer(offset); - - // Make sure the false literal is data[1]: - if (c[0].var() == p.var()) { - Lit tmp(c[0]); - c[0] = c[1]; - c[1] = tmp; - } - assert(c[1].var() == p.var()); - - bool final = c.xorEqualFalse(); - for (uint32_t k = 0, size = c.size(); k != size; k++ ) { - const lbool& val = assigns[c[k].var()]; - if (val.isUndef() && k >= 2) { - Lit tmp(c[1]); - c[1] = c[k]; - c[k] = tmp; - removeWXCl(watches[(~p).toInt()], offset); - watches[Lit(c[1].var(), false).toInt()].push(offset); - watches[Lit(c[1].var(), true).toInt()].push(offset); - return true; - } - - c[k] = c[k].unsign() ^ val.getBool(); - final ^= val.getBool(); - } - - // Did not find watch -- clause is unit under assignment: - *j++ = *i; - - if (assigns[c[0].var()].isUndef()) { - c[0] = c[0].unsign()^final; - if (full) uncheckedEnqueue(c[0], offset); - else uncheckedEnqueueLight(c[0]); - } else if (!final) { - confl = PropBy(offset); - qhead = trail.size(); - return false; - } else { - Lit tmp(c[0]); - c[0] = c[1]; - c[1] = tmp; - } - - return true; -} - -/** -@brief Does the propagation - -Basically, it goes through the watchlists recursively, and calls the appropirate -propagaton function -*/ -template<bool full> -PropBy Solver::propagate(const bool update) -{ - PropBy confl; - uint32_t num_props = 0; - - #ifdef VERBOSE_DEBUG - cout << "Propagation started" << endl; - #endif - - while (qhead < trail.size()) { - Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. - vec<Watched>& ws = watches[p.toInt()]; - num_props += ws.size()/2 + 2; - - #ifdef VERBOSE_DEBUG - cout << "Propagating lit " << p << endl; - cout << "ws origSize: "<< ws.size() << endl; - #endif - - vec<Watched>::iterator i = ws.getData(); - vec<Watched>::iterator j = i; - - vec<Watched>::iterator end = ws.getDataEnd(); - for (; i != end; i++) { - if (i->isBinary()) { - *j++ = *i; - if (!propBinaryClause<full>(i, p, confl)) break; - else continue; - } //end BINARY - - if (i->isTriClause()) { - *j++ = *i; - if (!propTriClause<full>(i, p, confl)) break; - else continue; - } //end TRICLAUSE - - if (i->isClause()) { - num_props += 4; - if (!propNormalClause<full>(i, j, p, confl, update)) break; - else continue; - } //end CLAUSE - - if (i->isXorClause()) { - num_props += 10; - if (!propXorClause<full>(i, j, p, confl)) break; - else continue; - } //end XORCLAUSE - } - if (i != end) { - i++; - //copy remaining watches - vec<Watched>::iterator j2 = i; - vec<Watched>::iterator i2 = j; - for(i2 = i, j2 = j; i2 != end; i2++) { - *j2++ = *i2; - } - //memmove(j, i, sizeof(Watched)*(end-i)); - } - //assert(i >= j); - ws.shrink_(i-j); - } - propagations += num_props; - simpDB_props -= num_props; - - #ifdef VERBOSE_DEBUG - cout << "Propagation ended." << endl; - #endif - - return confl; -} -template PropBy Solver::propagate<true>(const bool update); -template PropBy Solver::propagate<false>(const bool update); - -PropBy Solver::propagateBin(vec<Lit>& uselessBin) -{ - #ifdef DEBUG_USELESS_LEARNT_BIN_REMOVAL - assert(uselessBin.empty()); - #endif - - while (qhead < trail.size()) { - Lit p = trail[qhead++]; - - //setting up binPropData - uint32_t lev = binPropData[p.var()].lev; - Lit lev1Ancestor; - switch (lev) { - case 0 : - lev1Ancestor = lit_Undef; - break; - case 1: - lev1Ancestor = p; - break; - default: - lev1Ancestor = binPropData[p.var()].lev1Ancestor; - } - lev++; - const bool learntLeadHere = binPropData[p.var()].learntLeadHere; - bool& hasChildren = binPropData[p.var()].hasChildren; - hasChildren = false; - - //std::cout << "lev: " << lev << " ~p: " << ~p << std::endl; - const vec<Watched> & ws = watches[p.toInt()]; - propagations += 2; - for(vec<Watched>::const_iterator k = ws.getData(), end = ws.getDataEnd(); k != end; k++) { - hasChildren = true; - if (!k->isBinary()) continue; - - //std::cout << (~p) << ", " << k->getOtherLit() << " learnt: " << k->getLearnt() << std::endl; - lbool val = value(k->getOtherLit()); - if (val.isUndef()) { - uncheckedEnqueueLight2(k->getOtherLit(), lev, lev1Ancestor, learntLeadHere || k->getLearnt()); - } else if (val == l_False) { - return PropBy(p); - } else { - assert(val == l_True); - Lit lit2 = k->getOtherLit(); - if (lev > 1 - && level[lit2.var()] != 0 - && binPropData[lit2.var()].lev == 1 - && lev1Ancestor != lit2) { - //Was propagated at level 1, and again here, original level 1 binary clause is useless - binPropData[lit2.var()].lev = lev; - binPropData[lit2.var()].lev1Ancestor = lev1Ancestor; - binPropData[lit2.var()].learntLeadHere = learntLeadHere || k->getLearnt(); - uselessBin.push(lit2); - } - } - } - } - //std::cout << " -----------" << std::endl; - - return PropBy(); -} - -/** -@brief Only propagates binary clauses - -This is used in special algorithms outside the main Solver class -*/ -PropBy Solver::propagateNonLearntBin() -{ - multiLevelProp = false; - uint32_t origQhead = qhead + 1; - - while (qhead < trail.size()) { - Lit p = trail[qhead++]; - const vec<Watched> & ws = watches[p.toInt()]; - propagations += ws.size()/2 + 2; - for(vec<Watched>::const_iterator k = ws.getData(), end = ws.getDataEnd(); k != end; k++) { - if (!k->isNonLearntBinary()) break; - - lbool val = value(k->getOtherLit()); - if (val.isUndef()) { - if (qhead != origQhead) multiLevelProp = true; - uncheckedEnqueueLight(k->getOtherLit()); - } else if (val == l_False) { - return PropBy(p); - } - } - } - - return PropBy(); -} - -/** -@brief Propagate recursively on non-learnt binaries, but do not propagate exceptLit if we reach it -*/ -bool Solver::propagateBinExcept(const Lit exceptLit) -{ - while (qhead < trail.size()) { - Lit p = trail[qhead++]; - const vec<Watched> & ws = watches[p.toInt()]; - propagations += ws.size()/2 + 2; - for(vec<Watched>::const_iterator i = ws.getData(), end = ws.getDataEnd(); i != end; i++) { - if (!i->isNonLearntBinary()) break; - - lbool val = value(i->getOtherLit()); - if (val.isUndef() && i->getOtherLit() != exceptLit) { - uncheckedEnqueueLight(i->getOtherLit()); - } else if (val == l_False) { - return false; - } - } - } - - return true; -} - -/** -@brief Propagate only for one hop(=non-recursively) on non-learnt bins -*/ -bool Solver::propagateBinOneLevel() -{ - Lit p = trail[qhead]; - const vec<Watched> & ws = watches[p.toInt()]; - propagations += ws.size()/2 + 2; - for(vec<Watched>::const_iterator i = ws.getData(), end = ws.getDataEnd(); i != end; i++) { - if (!i->isNonLearntBinary()) break; - - lbool val = value(i->getOtherLit()); - if (val.isUndef()) { - uncheckedEnqueueLight(i->getOtherLit()); - } else if (val == l_False) { - return false; - } - } - - return true; -} - -struct LevelSorter -{ - LevelSorter(const vec<int32_t>& _level) : - level(_level) - {} - - bool operator()(const Lit lit1, const Lit lit2) const { - return level[lit1.var()] < level[lit2.var()]; - } - - const vec<int32_t>& level; -}; - -/** -@brief Calculates the glue of a clause - -Used to calculate the Glue of a new clause, or to update the glue of an -existing clause. Only used if the glue-based activity heuristic is enabled, -i.e. if we are in GLUCOSE mode (not MiniSat mode) -*/ -template<class T> -inline uint32_t Solver::calcNBLevels(const T& ps) -{ - uint32_t nbLevels = 0; - for(const Lit *l = ps.getData(), *end = ps.getDataEnd(); l != end; l++) { - int32_t lev = level[l->var()]; - if (!seen[lev]) { - nbLevels++; - seen[lev] = 1; - } - } - for(const Lit *l = ps.getData(), *end = ps.getDataEnd(); l != end; l++) { - int32_t lev = level[l->var()]; - seen[lev] = 0; - } - return nbLevels; -} - -/*_________________________________________________________________________________________________ -| -| reduceDB : () -> [void] -| -| Description: -| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked -| clauses are clauses that are reason to some assignment. Binary clauses are never removed. -|________________________________________________________________________________________________@*/ -bool reduceDB_ltMiniSat::operator () (const Clause* x, const Clause* y) { - const uint32_t xsize = x->size(); - const uint32_t ysize = y->size(); - - assert(xsize > 2 && ysize > 2); - if (x->getMiniSatAct() == y->getMiniSatAct()) - return xsize > ysize; - else return x->getMiniSatAct() < y->getMiniSatAct(); -} - -bool reduceDB_ltGlucose::operator () (const Clause* x, const Clause* y) { - const uint32_t xsize = x->size(); - const uint32_t ysize = y->size(); - - assert(xsize > 2 && ysize > 2); - if (x->getGlue() > y->getGlue()) return 1; - if (x->getGlue() < y->getGlue()) return 0; - return xsize > ysize; -} - -/** -@brief Removes learnt clauses that have been found not to be too good - -Either based on glue or MiniSat-style learnt clause activities, the clauses are -sorted and then removed -*/ -void Solver::reduceDB() -{ - uint32_t i, j; - - nbReduceDB++; - if (lastSelectedRestartType == dynamic_restart) - std::sort(learnts.getData(), learnts.getDataEnd(), reduceDB_ltGlucose()); - else - std::sort(learnts.getData(), learnts.getDataEnd(), reduceDB_ltMiniSat()); - - #ifdef VERBOSE_DEBUG - std::cout << "Cleaning clauses" << std::endl; - for (uint32_t i = 0; i != learnts.size(); i++) { - std::cout << "activity:" << learnts[i]->getGlue() - << " \toldActivity:" << learnts[i]->getMiniSatAct() - << " \tsize:" << learnts[i]->size() << std::endl; - } - #endif - - - const uint32_t removeNum = (double)learnts.size() * (double)RATIOREMOVECLAUSES; - uint32_t totalNumRemoved = 0; - uint32_t totalNumNonRemoved = 0; - uint64_t totalGlueOfRemoved = 0; - uint64_t totalSizeOfRemoved = 0; - uint64_t totalGlueOfNonRemoved = 0; - uint64_t totalSizeOfNonRemoved = 0; - for (i = j = 0; i != removeNum; i++){ - if (i+1 < removeNum) __builtin_prefetch(learnts[i+1]); - assert(learnts[i]->size() > 2); - if (!locked(*learnts[i]) - && (lastSelectedRestartType == static_restart || learnts[i]->getGlue() > 2) - && learnts[i]->size() > 3) { //we cannot update activity of 3-longs because of wathclists - - totalGlueOfRemoved += learnts[i]->getGlue(); - totalSizeOfRemoved += learnts[i]->size(); - totalNumRemoved++; - removeClause(*learnts[i]); - } else { - totalGlueOfNonRemoved += learnts[i]->getGlue(); - totalSizeOfNonRemoved += learnts[i]->size(); - totalNumNonRemoved++; - learnts[j++] = learnts[i]; - } - } - for (; i < learnts.size(); i++) { - totalGlueOfNonRemoved += learnts[i]->getGlue(); - totalSizeOfNonRemoved += learnts[i]->size(); - totalNumNonRemoved++; - learnts[j++] = learnts[i]; - } - learnts.shrink_(i - j); - - if (conf.verbosity >= 3) { - std::cout << "c rem-learnts " << std::setw(6) << totalNumRemoved - << " avgGlue " - << std::fixed << std::setw(5) << std::setprecision(2) << ((double)totalGlueOfRemoved/(double)totalNumRemoved) - << " avgSize " - << std::fixed << std::setw(6) << std::setprecision(2) << ((double)totalSizeOfRemoved/(double)totalNumRemoved) - << " || remain " << std::setw(6) << totalNumNonRemoved - << " avgGlue " - << std::fixed << std::setw(5) << std::setprecision(2) << ((double)totalGlueOfNonRemoved/(double)totalNumNonRemoved) - << " avgSize " - << std::fixed << std::setw(6) << std::setprecision(2) << ((double)totalSizeOfNonRemoved/(double)totalNumNonRemoved) - << std::endl; - } - - clauseAllocator.consolidate(this); -} - -inline int64_t abs64(int64_t a) -{ - if (a < 0) return -a; - return a; -} - -/** -@brief Simplify the clause database according to the current top-level assigment. - -We remove satisfied clauses, clean clauses from assigned literals, find -binary xor-clauses and replace variables with one another. Heuristics are -used to check if we need to find binary xor clauses or not. -*/ -bool Solver::simplify() -{ - testAllClauseAttach(); - assert(decisionLevel() == 0); - - if (!ok || !propagate<false>().isNULL()) { - ok = false; - return false; - } - - if (simpDB_props > 0) { - return true; - } - double myTime = cpuTime(); - - double slowdown = (100000.0/((double)numBins * 30000.0/((double)order_heap.size()))); - slowdown = std::min(1.5, slowdown); - slowdown = std::max(0.01, slowdown); - - double speedup = 200000000.0/(double)(propagations-lastSearchForBinaryXor); - speedup = std::min(3.5, speedup); - speedup = std::max(0.2, speedup); - - /*std::cout << "new:" << nbBin - lastNbBin + becameBinary << std::endl; - std::cout << "left:" << ((double)(nbBin - lastNbBin + becameBinary)/BINARY_TO_XOR_APPROX) * slowdown << std::endl; - std::cout << "right:" << (double)order_heap.size() * PERCENTAGEPERFORMREPLACE * speedup << std::endl;*/ - - if (conf.doFindEqLits && conf.doRegFindEqLits && - (((double)abs64((int64_t)numNewBin - (int64_t)lastNbBin)/BINARY_TO_XOR_APPROX) * slowdown) > - ((double)order_heap.size() * PERCENTAGEPERFORMREPLACE * speedup)) { - lastSearchForBinaryXor = propagations; - - clauseCleaner->cleanClauses(clauses, ClauseCleaner::clauses); - clauseCleaner->cleanClauses(learnts, ClauseCleaner::learnts); - clauseCleaner->removeSatisfiedBins(); - if (!ok) return false; - - if (!sCCFinder->find2LongXors()) return false; - - lastNbBin = numNewBin; - } - - // Remove satisfied clauses: - clauseCleaner->removeAndCleanAll(); - if (!ok) return false; - - if (conf.doReplace && !varReplacer->performReplace()) - return false; - - // Remove fixed variables from the variable heap: - order_heap.filter(VarFilter(*this)); - - #ifdef USE_GAUSS - for (vector<Gaussian*>::iterator gauss = gauss_matrixes.begin(), end = gauss_matrixes.end(); gauss != end; gauss++) { - if (!(*gauss)->full_init()) return false; - } - #endif //USE_GAUSS - - simpDB_assigns = nAssigns(); - simpDB_props = std::min((uint64_t)80000000, 4*clauses_literals + 4*learnts_literals); //at most 6 sec wait - simpDB_props = std::max((int64_t)30000000, simpDB_props); //at least 2 sec wait - totalSimplifyTime += cpuTime() - myTime; - - testAllClauseAttach(); - return true; -} - -/** -@brief Search for a model - -Limits: must be below the specified number of conflicts and must keep the -number of learnt clauses below the provided limit - -Use negative value for 'nof_conflicts' or 'nof_learnts' to indicate infinity. - -Output: 'l_True' if a partial assigment that is consistent with respect to the -clauseset is found. If all variables are decision variables, this means -that the clause set is satisfiable. 'l_False' if the clause set is -unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. -*/ -lbool Solver::search(const uint64_t nof_conflicts, const uint64_t nof_conflicts_fullrestart, const bool update) -{ - assert(ok); - uint64_t conflictC = 0; - vec<Lit> learnt_clause; - llbool ret; - - if (!simplifying && update) { - starts++; - if (restartType == static_restart) staticStarts++; - else dynStarts++; - } - glueHistory.fastclear(); - - #ifdef USE_GAUSS - for (vector<Gaussian*>::iterator gauss = gauss_matrixes.begin(), end = gauss_matrixes.end(); gauss != end; gauss++) { - if (!(*gauss)->full_init()) - return l_False; - } - #endif //USE_GAUSS - - testAllClauseAttach(); - findAllAttach(); - #ifdef VERBOSE_DEBUG - std::cout << "c started Solver::search()" << std::endl; - //printAllClauses(); - #endif //VERBOSE_DEBUG - for (;;) { - assert(ok); - PropBy confl = propagate<true>(update); - #ifdef VERBOSE_DEBUG - std::cout << "c Solver::search() has finished propagation" << std::endl; - //printAllClauses(); - #endif //VERBOSE_DEBUG - - if (conflicts > conf.maxConfl) { - if (conf.verbosity >= 0) { - std::cout << "c Interrupting: limit on number of conflicts, " - << conf.maxConfl - << " reached! " << std::endl; - } - needToInterrupt = true; - return l_Undef; - } - - if (!confl.isNULL()) { - ret = handle_conflict(learnt_clause, confl, conflictC, update); - if (ret != l_Nothing) return ret; - } else { - #ifdef USE_GAUSS - bool at_least_one_continue = false; - for (vector<Gaussian*>::iterator gauss = gauss_matrixes.begin(), end= gauss_matrixes.end(); gauss != end; gauss++) { - ret = (*gauss)->find_truths(learnt_clause, conflictC); - if (ret == l_Continue) at_least_one_continue = true; - else if (ret != l_Nothing) return ret; - } - if (at_least_one_continue) continue; - #endif //USE_GAUSS - - assert(ok); - if (conf.doCacheOTFSSR && decisionLevel() == 1) saveOTFData(); - ret = new_decision(nof_conflicts, nof_conflicts_fullrestart, conflictC); - if (ret != l_Nothing) return ret; - } - } -} - -/** -@brief Picks a new decision variable to branch on - -@returns l_Undef if it should restart instead. l_False if it reached UNSAT - (through simplification) -*/ -llbool Solver::new_decision(const uint64_t nof_conflicts, const uint64_t nof_conflicts_fullrestart, const uint64_t conflictC) -{ - - if (conflicts >= nof_conflicts_fullrestart || needToInterrupt) { - cancelUntil(0); - return l_Undef; - } - - // Reached bound on number of conflicts? - switch (restartType) { - case dynamic_restart: - if (glueHistory.isvalid() && - 0.95*glueHistory.getAvgDouble() > glueHistory.getAvgAllDouble()) { - - #ifdef DEBUG_DYNAMIC_RESTART - if (glueHistory.isvalid()) { - std::cout << "glueHistory.getavg():" << glueHistory.getavg() <<std::endl; - std::cout << "totalSumOfGlue:" << totalSumOfGlue << std::endl; - std::cout << "conflicts:" << conflicts<< std::endl; - std::cout << "compTotSumGlue:" << compTotSumGlue << std::endl; - std::cout << "conflicts-compTotSumGlue:" << conflicts-compTotSumGlue<< std::endl; - } - #endif - - cancelUntil(0); - return l_Undef; - } - break; - case static_restart: - if (conflictC >= nof_conflicts) { - cancelUntil(0); - return l_Undef; - } - break; - case auto_restart: - assert(false); - break; - } - - // Simplify the set of problem clauses: - if (decisionLevel() == 0) { - if (!dataSync->syncData()) return l_False; - if (!simplify()) return l_False; - } - - // Reduce the set of learnt clauses: - if (conflicts >= numCleanedLearnts * nbClBeforeRed + nbCompensateSubsumer) { - numCleanedLearnts ++; - reduceDB(); - nbClBeforeRed += 500; - } - - Lit next = lit_Undef; - while (decisionLevel() < assumptions.size()) { - // Perform user provided assumption: - Lit p = assumptions[decisionLevel()]; - if (value(p) == l_True) { - // Dummy decision level: - newDecisionLevel(); - } else if (value(p) == l_False) { - analyzeFinal(~p, conflict); - return l_False; - } else { - next = p; - break; - } - } - - if (next == lit_Undef) { - // New variable decision: - decisions++; - next = pickBranchLit(); - - if (next == lit_Undef) - return l_True; - } - - // Increase decision level and enqueue 'next' - assert(value(next) == l_Undef); - newDecisionLevel(); - uncheckedEnqueue(next); - - return l_Nothing; -} - -/** -@brief Handles a conflict that we reached through propagation - -Handles on-the-fly subsumption: the OTF subsumption check is done in -conflict analysis, but this is the code that actually replaces the original -clause with that of the shorter one -@returns l_False if UNSAT -*/ -llbool Solver::handle_conflict(vec<Lit>& learnt_clause, PropBy confl, uint64_t& conflictC, const bool update) -{ - #ifdef VERBOSE_DEBUG - cout << "Handling conflict: "; - for (uint32_t i = 0; i < learnt_clause.size(); i++) - cout << learnt_clause[i].var()+1 << ","; - cout << endl; - #endif - - int backtrack_level; - uint32_t glue; - - conflicts++; - conflictC++; - if (decisionLevel() == 0) - return l_False; - learnt_clause.clear(); - Clause* c = analyze(confl, learnt_clause, backtrack_level, glue, update); - if (update) { - avgBranchDepth.push(decisionLevel()); - if (restartType == dynamic_restart) glueHistory.push(glue); - conflSizeHist.push(learnt_clause.size()); - } - cancelUntil(backtrack_level); - #ifdef DUMP_STATS - std::cout << "Learnt clause: " << learnt_clause - << " glue: " << glue - << " declevel: " << decisionLevel() - << " traillen: " << trail.size() - << " abst: " << calcAbstraction(learnt_clause) - << std::endl; - assert(learnt_clause.size() == 1 || glue > 1); - #endif //#ifdef DUMP_STATS - - #ifdef VERBOSE_DEBUG - cout << "Learning:"; - for (uint32_t i = 0; i < learnt_clause.size(); i++) printLit(learnt_clause[i]), cout << " "; - cout << endl; - cout << "reverting var " << learnt_clause[0].var()+1 << " to " << !learnt_clause[0].sign() << endl; - #endif - - assert(value(learnt_clause[0]) == l_Undef); - //Unitary learnt - if (learnt_clause.size() == 1) { - uncheckedEnqueue(learnt_clause[0]); - assert(backtrack_level == 0 && "Unit clause learnt, so must cancel until level 0, right?"); - - #ifdef VERBOSE_DEBUG - cout << "Unit clause learnt." << endl; - #endif - //Normal learnt - } else { - if (learnt_clause.size() == 2) { - attachBinClause(learnt_clause[0], learnt_clause[1], true); - numNewBin++; - dataSync->signalNewBinClause(learnt_clause); - uncheckedEnqueue(learnt_clause[0], PropBy(learnt_clause[1])); - goto end; - } - - if (learnt_clause.size() > 3) { - std::sort(learnt_clause.getData()+1, learnt_clause.getDataEnd(), PolaritySorter(polarity)); - } - if (c) { //On-the-fly subsumption - uint32_t origSize = c->size(); - detachClause(*c); - for (uint32_t i = 0; i != learnt_clause.size(); i++) - (*c)[i] = learnt_clause[i]; - c->shrink(origSize - learnt_clause.size()); - if (c->learnt() && c->getGlue() > glue) - c->setGlue(glue); // LS - attachClause(*c); - uncheckedEnqueue(learnt_clause[0], clauseAllocator.getOffset(c)); - } else { //no on-the-fly subsumption - c = clauseAllocator.Clause_new(learnt_clause, true); - #ifdef ENABLE_UNWIND_GLUE - if (conf.doMaxGlueDel && glue > conf.maxGlue) { - nbClOverMaxGlue++; - nbCompensateSubsumer++; - unWindGlue[learnt_clause[0].var()] = c; - #ifdef UNWINDING_DEBUG - std::cout << "unwind, var:" << learnt_clause[0].var() << std::endl; - c->plainPrint(); - #endif //VERBOSE_DEBUG - } else { - #endif //ENABLE_UNWIND_GLUE - learnts.push(c); - #ifdef ENABLE_UNWIND_GLUE - } - #endif //ENABLE_UNWIND_GLUE - c->setGlue(std::min(glue, MAX_THEORETICAL_GLUE)); - attachClause(*c); - uncheckedEnqueue(learnt_clause[0], clauseAllocator.getOffset(c)); - } - end:; - } - - varDecayActivity(); - if (update && restartType == static_restart) claDecayActivity(); - - return l_Nothing; -} - -/** -@brief After a full restart, determines which restar type to use - -Uses class RestartTypeChooser to do the heavy-lifting -*/ -bool Solver::chooseRestartType(const uint32_t& lastFullRestart) -{ - uint32_t relativeStart = starts - lastFullRestart; - - if (relativeStart > RESTART_TYPE_DECIDER_FROM && relativeStart < RESTART_TYPE_DECIDER_UNTIL) { - if (conf.fixRestartType == auto_restart) - restartTypeChooser->addInfo(); - - if (relativeStart == (RESTART_TYPE_DECIDER_UNTIL-1)) { - RestartType tmp; - if (conf.fixRestartType == auto_restart) - tmp = restartTypeChooser->choose(); - else - tmp = conf.fixRestartType; - - if (tmp == dynamic_restart) { - glueHistory.fastclear(); - if (conf.verbosity >= 3) - std::cout << "c Decided on dynamic restart strategy" - << std::endl; - } else { - if (conf.verbosity >= 1) - std::cout << "c Decided on static restart strategy" - << std::endl; - - if (!matrixFinder->findMatrixes()) return false; - } - lastSelectedRestartType = tmp; - restartType = tmp; - restartTypeChooser->reset(); - } - } - - return true; -} - -inline void Solver::setDefaultRestartType() -{ - if (conf.fixRestartType != auto_restart) restartType = conf.fixRestartType; - else restartType = static_restart; - - glueHistory.clear(); - glueHistory.initSize(MIN_GLUE_RESTART); - conflSizeHist.clear(); - conflSizeHist.initSize(1000); - - lastSelectedRestartType = restartType; -} - -/** -@brief The function that brings together almost all CNF-simplifications - -It burst-searches for given number of conflicts, then it tries all sorts of -things like variable elimination, subsumption, failed literal probing, etc. -to try to simplifcy the problem at hand. -*/ -lbool Solver::simplifyProblem(const uint32_t numConfls) -{ - testAllClauseAttach(); - bool gaussWasCleared = clearGaussMatrixes(); - - StateSaver savedState(*this);; - - #ifdef BURST_SEARCH - if (conf.verbosity >= 3) - std::cout << "c " << std::setw(24) << " " - << "Simplifying problem for " << std::setw(8) << numConfls << " confls" - << std::endl; - conf.random_var_freq = 1; - simplifying = true; - uint64_t origConflicts = conflicts; - #endif //BURST_SEARCH - - lbool status = l_Undef; - - #ifdef BURST_SEARCH - restartType = static_restart; - - printRestartStat("S"); - while(status == l_Undef && conflicts-origConflicts < numConfls && needToInterrupt == false) { - status = search(100, std::numeric_limits<uint64_t>::max(), false); - } - if (needToInterrupt) return l_Undef; - printRestartStat("S"); - if (status != l_Undef) goto end; - #endif //BURST_SEARCH - - if (conf.doXorSubsumption && !xorSubsumer->simplifyBySubsumption()) goto end; - - if (conf.doFailedLit && conf.doCacheOTFSSR) { - BothCache both(*this); - if (!both.tryBoth()) goto end; - } - if (conf.doCacheOTFSSR) cleanCache(); - if (conf.doClausVivif && !clauseVivifier->vivifyClauses()) goto end; - - if (conf.doCacheOTFSSRSet && order_heap.size() < 200000) { - if (conf.doCacheOTFSSR == false && conf.verbosity > 0) { - std::cout << "c turning cache ON because the number of active variables is lower now" << std::endl; - } - conf.doCacheOTFSSR = true; - } - if (conf.doFailedLit && !failedLitSearcher->search()) goto end; - - if (conf.doSatELite && !subsumer->simplifyBySubsumption()) goto end; - - /*if (findNormalXors && xorclauses.size() > 200 && clauses.size() < MAX_CLAUSENUM_XORFIND/8) { - XorFinder xorFinder(*this, clauses, ClauseCleaner::clauses); - if (!xorFinder.doNoPart(3, 7)) { - status = l_False; - goto end; - } - } else*/ if (xorclauses.size() <= 200 && xorclauses.size() > 0 && nClauses() > 10000) { - XorFinder x(*this, clauses); - x.addAllXorAsNorm(); - } - - if (conf.doClausVivif && !clauseVivifier->vivifyClauses()) goto end; - - //addSymmBreakClauses(); - - if (conf.doSortWatched) sortWatched(); - if (conf.doCacheOTFSSR && conf.doCalcReach) calcReachability(); - -end: - #ifdef BURST_SEARCH - if (conf.verbosity >= 3) - std::cout << "c Simplifying finished" << std::endl; - #endif //#ifdef BURST_SEARCH - - savedState.restore(); - simplifying = false; - - if (status == l_Undef && ok && gaussWasCleared && !matrixFinder->findMatrixes()) - status = l_False; - - testAllClauseAttach(); - - if (!ok) return l_False; - return status; -} - -/** -@brief Should we perform a full restart? - -If so, we also do the things to be done if the full restart is effected. -*/ -bool Solver::checkFullRestart(uint64_t& nof_conflicts, uint64_t& nof_conflicts_fullrestart, uint32_t& lastFullRestart) -{ - if (nof_conflicts_fullrestart > 0 && conflicts >= nof_conflicts_fullrestart) { - #ifdef USE_GAUSS - clearGaussMatrixes(); - #endif //USE_GAUSS - nof_conflicts = conf.restart_first + (double)conf.restart_first*conf.restart_inc; - nof_conflicts_fullrestart = (double)nof_conflicts_fullrestart * FULLRESTART_MULTIPLIER_MULTIPLIER; - restartType = static_restart; - lastFullRestart = starts; - - if (conf.verbosity >= 3) - std::cout << "c Fully restarting" << std::endl; - printRestartStat("F"); - - /*if (findNormalXors && clauses.size() < MAX_CLAUSENUM_XORFIND) { - XorFinder xorFinder(this, clauses, ClauseCleaner::clauses); - if (!xorFinder.doNoPart(3, 10)) - return false; - }*/ - - //calculateDefaultPolarities(); - if (conf.polarity_mode != polarity_auto) { - for (uint32_t i = 0; i < polarity.size(); i++) { - polarity[i] = defaultPolarity(); - } - } - - fullStarts++; - } - - return true; -} - -/** -@brief Performs a set of pre-optimisations before the beggining of solving - -This is somewhat different than the set of optimisations carried out during -solving in simplifyProblem(). For instance, binary xors are searched fully -here, while there, no search for them is carried out. Also, the ordering -is different. - -\todo experiment to use simplifyProblem() instead of this, with the only -addition of binary clause search. Maybe it will do just as good (or better). -*/ -void Solver::performStepsBeforeSolve() -{ - assert(qhead == trail.size()); - testAllClauseAttach(); - - printRestartStat(); - if (conf.doReplace && !varReplacer->performReplace()) return; - - order_heap.filter(Solver::VarFilter(*this)); - if (order_heap.size() > 300000) { - if (conf.verbosity > 0) { - std::cout << "c turning cache OFF because there are too many active variables" << std::endl; - } - conf.doCacheOTFSSR = false; - } - - bool saveDoHyperBin = conf.doHyperBinRes; - conf.doHyperBinRes = false; - clauseAllocator.consolidate(this, true); - if (conf.doFailedLit && !failedLitSearcher->search()) return; - conf.doHyperBinRes = saveDoHyperBin; - if (conf.doClausVivif && !conf.libraryUsage - && !clauseVivifier->vivifyClauses()) return; - - #ifdef VERBOSE_DEBUG - printAllClauses(); - #endif //VERBOSE_DEBUG - if (conf.doSatELite - && !conf.libraryUsage - && clauses.size() < 4800000 - && !subsumer->simplifyBySubsumption()) - return; - - if (conf.doFindEqLits) { - if (!sCCFinder->find2LongXors()) return; - lastNbBin = numNewBin; - if (conf.doReplace && !varReplacer->performReplace(true)) return; - } - - if (conf.doFindXors && clauses.size() < MAX_CLAUSENUM_XORFIND) { - XorFinder xorFinder(*this, clauses); - if (!xorFinder.fullFindXors(3, 7)) return; - } - - if (xorclauses.size() > 1) { - if (conf.doXorSubsumption && !xorSubsumer->simplifyBySubsumption()) - return; - - if (conf.doReplace && !varReplacer->performReplace()) - return; - } - - if (conf.doSortWatched) sortWatched(); - if (conf.doCacheOTFSSR && conf.doCalcReach) calcReachability(); - - testAllClauseAttach(); -} - -/** -@brief Initialises model, restarts, learnt cluause cleaning, burst-search, etc. -*/ -void Solver::initialiseSolver() -{ - //Clear up previous stuff like model, final conflict, matrixes - model.clear(); - conflict.clear(); - clearGaussMatrixes(); - - //Initialise restarts & dynamic restart datastructures - setDefaultRestartType(); - - //Initialise avg. branch depth - avgBranchDepth.clear(); - avgBranchDepth.initSize(500); - - //Initialise number of restarts&full restarts - starts = 0; - fullStarts = 0; - - if (nClauses() * conf.learntsize_factor < nbClBeforeRed) { - if (nClauses() * conf.learntsize_factor < nbClBeforeRed/2) - nbClBeforeRed /= 4; - else - nbClBeforeRed = (nClauses() * conf.learntsize_factor)/2; - } - - testAllClauseAttach(); - findAllAttach(); -} - -/** -@brief The main solve loop that glues everything together - -We clear everything needed, pre-simplify the problem, calculate default -polarities, and start the loop. Finally, we either report UNSAT or extend the -found solution with all the intermediary simplifications (e.g. variable -elimination, etc.) and output the solution. -*/ -lbool Solver::solve(const vec<Lit>& assumps) -{ - #ifdef VERBOSE_DEBUG - std::cout << "Solver::solve() called" << std::endl; - #endif - if (!ok) return l_False; - assert(qhead == trail.size()); - assert(subsumer->checkElimedUnassigned()); - assert(xorSubsumer->checkElimedUnassigned()); - - if (libraryCNFFile) - fprintf(libraryCNFFile, "c Solver::solve() called\n"); - - assumps.copyTo(assumptions); - initialiseSolver(); - uint64_t nof_conflicts = conf.restart_first; //Geometric restart policy, start with this many - uint64_t nof_conflicts_fullrestart = conf.restart_first * FULLRESTART_MULTIPLIER + conflicts; //at this point, do a full restart - uint32_t lastFullRestart = starts; //last time a full restart was made was at this number of restarts - lbool status = l_Undef; //Current status - uint64_t nextSimplify = conf.restart_first * conf.simpStartMult + conflicts; //Do simplifyProblem() at this number of conflicts - if (!conf.doSchedSimp) nextSimplify = std::numeric_limits<uint64_t>::max(); - - if (conflicts == 0) { - if (conf.doPerformPreSimp) performStepsBeforeSolve(); - if (!ok) return l_False; - - calculateDefaultPolarities(); - } - - printStatHeader(); - printRestartStat("B"); - uint64_t lastConflPrint = conflicts; - // Search: - while (status == l_Undef && starts < conf.maxRestarts) { - #ifdef DEBUG_VARELIM - assert(subsumer->checkElimedUnassigned()); - assert(xorSubsumer->checkElimedUnassigned()); - #endif //DEBUG_VARELIM - - if ((conflicts - lastConflPrint) > std::min(std::max(conflicts/100*6, (uint64_t)4000), (uint64_t)20000)) { - printRestartStat("N"); - lastConflPrint = conflicts; - } - - if (conf.doSchedSimp && conflicts >= nextSimplify) { - status = simplifyProblem(conf.simpBurstSConf); - printRestartStat(); - lastConflPrint = conflicts; - nextSimplify = std::min((uint64_t)((double)conflicts * conf.simpStartMMult), conflicts + MAX_CONFL_BETWEEN_SIMPLIFY); - if (status != l_Undef) break; - } - - status = search(nof_conflicts, std::min(nof_conflicts_fullrestart, nextSimplify)); - if (needToInterrupt) { - cancelUntil(0); - return l_Undef; - } - - nof_conflicts = (double)nof_conflicts * conf.restart_inc; - if (status != l_Undef) break; - if (!checkFullRestart(nof_conflicts, nof_conflicts_fullrestart , lastFullRestart)) - return l_False; - if (!chooseRestartType(lastFullRestart)) - return l_False; - } - printEndSearchStat(); - - #ifdef VERBOSE_DEBUG - if (status == l_True) - std::cout << "Solution is SAT" << std::endl; - else if (status == l_False) - std::cout << "Solution is UNSAT" << std::endl; - else - std::cout << "Solutions is UNKNOWN" << std::endl; - #endif //VERBOSE_DEBUG - - if (status == l_True) handleSATSolution(); - else if (status == l_False) handleUNSATSolution(); - - cancelUntil(0); - restartTypeChooser->reset(); - if (status == l_Undef) clauseCleaner->removeAndCleanAll(true); - - #ifdef VERBOSE_DEBUG - std::cout << "Solver::solve() finished" << std::endl; - #endif - return status; -} - -/** -@brief Extends a SAT solution to the full solution - -variable elimination, variable replacement, sub-part solving, etc. all need to -be handled correctly to arrive at a solution that is a solution to ALL of the -original problem, not just of what remained of it at the end inside this class -(i.e. we need to combine things from the helper classes) -*/ -void Solver::handleSATSolution() -{ - - /*if (greedyUnbound) { - double time = cpuTime(); - FindUndef finder(*this); - const uint32_t unbounded = finder.unRoll(); - if (conf.verbosity >= 1) - printf("c Greedy unbounding :%5.2lf s, unbounded: %7d vars\n", cpuTime()-time, unbounded); - }*/ - assert(subsumer->checkElimedUnassigned()); - assert(xorSubsumer->checkElimedUnassigned()); - - varReplacer->extendModelPossible(); - checkSolution(); - - if (subsumer->getNumElimed() || xorSubsumer->getNumElimed()) { - if (conf.verbosity >= 1) { - std::cout << "c Solution needs extension. Extending." << std::endl; - } - Solver s; - s.conf = conf; - s.conf.doSatELite = false; - s.conf.doReplace = false; - s.conf.doFindEqLits = false; - s.conf.doRegFindEqLits = false; - s.conf.doFailedLit= false; - s.conf.doConglXors = false; - s.conf.doSubsWNonExistBins = false; - s.conf.doRemUselessBins = false; - s.conf.doClausVivif = false; - s.conf.doSortWatched = false; - s.conf.verbosity = 0; - - vec<Lit> tmp; - for (Var var = 0; var < nVars(); var++) { - s.newVar(decision_var[var] - || subsumer->getVarElimed()[var] - || varReplacer->varHasBeenReplaced(var) - || xorSubsumer->getVarElimed()[var] - ); - - //assert(!(xorSubsumer->getVarElimed()[var] && (decision_var[var] || subsumer->getVarElimed()[var] || varReplacer->varHasBeenReplaced(var)))); - - if (value(var) != l_Undef) { - #ifdef VERBOSE_DEBUG - std::cout << "Setting var " << var + 1 - << " in extend-solver to " << value(var) << std::endl; - #endif - tmp.clear(); - tmp.push(Lit(var, value(var) == l_False)); - s.addClause(tmp); - } - } - varReplacer->extendModelImpossible(s); - subsumer->extendModel(s); - xorSubsumer->extendModel(s); - - lbool status = s.solve(); - release_assert(status == l_True && "c ERROR! Extension of model failed!"); -#ifdef VERBOSE_DEBUG - std::cout << "Solution extending finished. Enqueuing results" << std::endl; -#endif - //need to start new decision level, otherwise uncheckedEnqueue will - //enqueue to decision level 0 in certain cases :S - newDecisionLevel(); - for (Var var = 0; var < nVars(); var++) { - if (assigns[var] == l_Undef && s.model[var] != l_Undef) - uncheckedEnqueue(Lit(var, s.model[var] == l_False)); - } - ok = (propagate<false>().isNULL()); - release_assert(ok && "c ERROR! Extension of model failed!"); - } - checkSolution(); - //Copy model: - model.growTo(nVars()); - for (Var var = 0; var != nVars(); var++) model[var] = value(var); -} - -/** -@brief When problem is decided to be UNSAT, this is called - -There is basically nothing to be handled for the moment, but this could be -made extensible -*/ -void Solver::handleUNSATSolution() -{ - if (conflict.size() == 0) - ok = false; -} - -void Solver::cleanCache() -{ - for(uint32_t i = 0; i < nVars(); i++) { - if (subsumer->getVarElimed()[i] || value(i) != l_Undef) { - vector<Lit> tmp1; - transOTFCache[Lit(i, false).toInt()].lits.swap(tmp1); - vector<Lit> tmp2; - transOTFCache[Lit(i, true).toInt()].lits.swap(tmp2); - continue; - } - - for(int which = 0; which < 2; which++) { - cleanCachePart(Lit(i, which)); - - } - } -} - -void Solver::cleanCachePart(const Lit vertLit) -{ - vector<Lit>& transCache = transOTFCache[(~vertLit).toInt()].lits; - assert(seen_vec.empty()); - - vector<Lit>::iterator it = transCache.begin(); - vector<Lit>::iterator it2 = it; - - size_t newSize = 0; - for (vector<Lit>::iterator end = transCache.end(); it != end; it++) { - Lit lit = *it; - lit = varReplacer->getReplaceTable()[lit.var()] ^ lit.sign(); - if (lit == vertLit - || seen[lit.toInt()] - || subsumer->getVarElimed()[lit.var()] - || subsumer->getVarElimed()[lit.var()] - ) continue; - - *it2++ = lit; - - //Don't allow the same value to be in the cache twice - seen[lit.toInt()] = 1; - seen_vec.push_back(lit); - - //Increase valid size - newSize++; - } - transCache.resize(newSize); - - //Clear up seen - for(vector<Lit>::const_iterator it = seen_vec.begin(), end = seen_vec.end(); it != end; it++) { - seen[it->toInt()] = 0; - } - seen_vec.clear(); -} |