diff options
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 292 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 49 | ||||
-rw-r--r-- | src/prop/minisat/core/SolverTypes.h | 1 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 8 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 4 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 9 |
6 files changed, 197 insertions, 166 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index ba36ac879..f7d67d445 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -157,7 +157,7 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) watches .init(mkLit(v, false)); watches .init(mkLit(v, true )); assigns .push(l_Undef); - vardata .push(mkVarData(CRef_Undef, 0, assertionLevel, -1)); + vardata .push(VarData(CRef_Undef, -1, -1, assertionLevel, -1)); activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0); seen .push(0); polarity .push(sign); @@ -177,6 +177,33 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) return v; } +void Solver::resizeVars(int newSize) { + assert(enable_incremental); + assert(decisionLevel() == 0); + Assert(newSize >= 2, "always keep true/false"); + if (newSize < nVars()) { + int shrinkSize = nVars() - newSize; + + // Resize watches up to the negated last literal + watches.resizeTo(mkLit(newSize-1, true)); + + // Resize all info arrays + assigns.shrink(shrinkSize); + vardata.shrink(shrinkSize); + activity.shrink(shrinkSize); + seen.shrink(shrinkSize); + polarity.shrink(shrinkSize); + decision.shrink(shrinkSize); + theory.shrink(shrinkSize); + + } + + if (Debug.isOn("minisat::pop")) { + for (int i = 0; i < trail.size(); ++ i) { + assert(var(trail[i]) < nVars()); + } + } +} CRef Solver::reason(Var x) { @@ -202,18 +229,31 @@ CRef Solver::reason(Var x) { int i, j; Lit prev = lit_Undef; for (i = 0, j = 0; i < explanation.size(); ++ i) { - int varLevel = intro_level(var(explanation[i])); - if (varLevel > explLevel) { - explLevel = varLevel; - } + // This clause is valid theory propagation, so it's level is the level of the top literal + explLevel = std::max(explLevel, intro_level(var(explanation[i]))); + Assert(value(explanation[i]) != l_Undef); Assert(i == 0 || trail_index(var(explanation[0])) > trail_index(var(explanation[i]))); - // ignore zero level literals - if (i == 0 || (level(var(explanation[i])) > 0 && explanation[i] != prev)) { + + // Always keep the first literal + if (i == 0) { prev = explanation[j++] = explanation[i]; + continue; + } + // Ignore duplicate literals + if (explanation[i] == prev) { + continue; + } + // Ignore zero level literals + if (level(var(explanation[i])) == 0 && user_level(var(explanation[i]) == 0)) { + continue; } + // Keep this literal + prev = explanation[j++] = explanation[i]; } explanation.shrink(i - j); + + // We need an explanation clause so we add a fake literal if (j == 1) { // Add not TRUE to the clause explanation.push(mkLit(varTrue, true)); @@ -221,9 +261,10 @@ CRef Solver::reason(Var x) { // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); - vardata[x] = mkVarData(real_reason, level(x), intro_level(x), trail_index(x)); + vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); attachClause(real_reason); + return real_reason; } @@ -235,16 +276,38 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) sort(ps); Lit p; int i, j; + // Which user-level to assert this clause at + int clauseLevel = removable ? 0 : assertionLevel; + // Check the clause for tautologies and similar + int falseLiteralsCount = 0; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { - if ((ps[i] == ~p) || (value(ps[i]) == l_True && level(var(ps[i])) == 0)) { + // Update the level + clauseLevel = std::max(clauseLevel, intro_level(var(ps[i]))); + // Tautologies are ignored + if (ps[i] == ~p) { // Clause can be ignored return true; } - if ((ps[i] != p) && (value(ps[i]) != l_False || level(var(ps[i])) > 0)) { - // This literal is a keeper - ps[j++] = p = ps[i]; + // Clauses with 0-level true literals are also ignored + if (value(ps[i]) == l_True && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { + return true; } + // Ignore repeated literals + if (ps[i] == p) { + continue; + } + // If a literals is false at 0 level (both sat and user level) we also ignore it + if (value(ps[i]) == l_False) { + if (level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { + continue; + } else { + // If we decide to keep it, we count it into the false literals + falseLiteralsCount ++; + } + } + // This literal is a keeper + ps[j++] = p = ps[i]; } // Fit to size @@ -256,24 +319,35 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) ps.copyTo(lemmas.last()); lemmas_removable.push(removable); } else { - // Add the clause and attach if not a lemma - if (ps.size() == 0) { + // If all false, we're in conflict + if (ps.size() == falseLiteralsCount) { return ok = false; - } else if (ps.size() == 1) { - if(assigns[var(ps[0])] == l_Undef) { - uncheckedEnqueue(ps[0]); - - PROOF( ProofManager::getSatProof()->registerUnitClause(ps[0], true); ) + } - return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef); - } else return ok; - } else { - CRef cr = ca.alloc(assertionLevel, ps, false); + CRef cr = CRef_Undef; + + // If not unit, add the clause + if (ps.size() > 1) { + + lemma_lt lt(*this); + sort(ps, lt); + + cr = ca.alloc(clauseLevel, ps, false); clauses_persistent.push(cr); attachClause(cr); - + PROOF( ProofManager::getSatProof()->registerClause(cr, true); ) } + + // Check if it propagates + if (ps.size() == falseLiteralsCount + 1) { + if(assigns[var(ps[0])] == l_Undef) { + assert(assigns[var(ps[0])] != l_False); + uncheckedEnqueue(ps[0], cr); + PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], true); } ) + return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef); + } else return ok; + } } return true; @@ -313,7 +387,7 @@ void Solver::detachClause(CRef cr, bool strict) { void Solver::removeClause(CRef cr) { Clause& c = ca[cr]; - Debug("minisat") << "Solver::removeClause(" << c << ")" << std::endl; + Debug("minisat::remove-clause") << "Solver::removeClause(" << c << ")" << std::endl; detachClause(cr); // Don't leave pointers to free'd memory! if (locked(c)) vardata[var(c[0])].reason = CRef_Undef; @@ -348,9 +422,7 @@ void Solver::cancelUntil(int level) { vardata[x].trail_index = -1; if ((phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) && (polarity[x] & 0x2) == 0) polarity[x] = sign(trail[c]); - if(intro_level(x) != -1) {// might be unregistered - insertVarOrder(x); - } + insertVarOrder(x); } qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); @@ -413,7 +485,7 @@ Lit Solver::pickBranchLit() rnd_decisions++; } // Activity based decision: - while (next == var_Undef || value(next) != l_Undef || !decision[next]) { + while (next >= nVars() || next == var_Undef || value(next) != l_Undef || !decision[next]) { if (order_heap.empty()){ next = var_Undef; break; @@ -473,15 +545,13 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) out_learnt.push(); // (leave room for the asserting literal) int index = trail.size() - 1; - int max_level = 0; // Maximal level of the resolved clauses + int max_resolution_level = 0; // Maximal level of the resolved clauses PROOF( ProofManager::getSatProof()->startResChain(confl); ) do{ assert(confl != CRef_Undef); // (otherwise should be UIP) Clause& c = ca[confl]; - if (c.level() > max_level) { - max_level = c.level(); - } + max_resolution_level = std::max(max_resolution_level, c.level()); if (c.removable()) claBumpActivity(c); @@ -497,6 +567,12 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) else out_learnt.push(q); } else { + // We could be resolving a literal propagated by a clause/theory using + // information from a higher level + if (!seen[var(q)] && level(var(q)) == 0) { + max_resolution_level = std::max(max_resolution_level, user_level(var(q))); + } + // FIXME: can we do it lazily if we actually need the proof? if (level(var(q)) == 0) { PROOF( ProofManager::getSatProof()->resolveOutUnit(q); ) @@ -531,22 +607,20 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) out_learnt[j++] = out_learnt[i]; } else { // Check if the literal is redundant - int red_level = litRedundant(out_learnt[i], abstract_level); - if (red_level < 0) { + if (!litRedundant(out_learnt[i], abstract_level)) { // Literal is not redundant out_learnt[j++] = out_learnt[i]; } else { - // PROOF( ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); ) - // Literal is redundant, mark the level of the redundancy derivation - if (max_level < red_level) { - max_level = red_level; - } + // Literal is redundant, to be safe, mark the level as current assertion level + // TODO: maybe optimize + max_resolution_level = std::max(max_resolution_level, user_level(var(out_learnt[i]))); } } } }else if (ccmin_mode == 1){ + Unreachable(); for (i = j = 1; i < out_learnt.size(); i++){ Var x = var(out_learnt[i]); @@ -587,26 +661,22 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) // Return the maximal resolution level - return max_level; + return max_resolution_level; } // Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is // visiting literals at levels that cannot be removed later. -int Solver::litRedundant(Lit p, uint32_t abstract_levels) +bool Solver::litRedundant(Lit p, uint32_t abstract_levels) { analyze_stack.clear(); analyze_stack.push(p); int top = analyze_toclear.size(); - int max_level = 0; while (analyze_stack.size() > 0){ CRef c_reason = reason(var(analyze_stack.last())); assert(c_reason != CRef_Undef); Clause& c = ca[c_reason]; int c_size = c.size(); analyze_stack.pop(); - if (c.level() > max_level) { - max_level = c.level(); - } // Since calling reason might relocate to resize, c is not necesserily the right reference, we must // use the allocator each time @@ -621,13 +691,13 @@ int Solver::litRedundant(Lit p, uint32_t abstract_levels) for (int j = top; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; analyze_toclear.shrink(analyze_toclear.size() - top); - return -1; + return false; } } } } - return max_level; + return true; } @@ -674,18 +744,14 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) { Debug("minisat") << "unchecked enqueue of " << p << " (" << trail_index(var(p)) << ") trail size is " << trail.size() << " cap is " << trail.capacity() << std::endl; assert(value(p) == l_Undef); + assert(var(p) < nVars()); assigns[var(p)] = lbool(!sign(p)); - vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size()); + vardata[var(p)] = VarData(from, decisionLevel(), assertionLevel, intro_level(var(p)), trail.size()); trail.push_(p); if (theory[var(p)]) { // Enqueue to the theory proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p)); } - if (from == CRef_Undef) { - if (assertionLevel > 0) { - trail_user.push(p); - } - } } @@ -943,26 +1009,12 @@ void Solver::removeClausesAboveLevel(vec<CRef>& cs, int level) for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; if (c.level() > level) { - if(Debug.isOn("minisat")) { - Debug("minisat") << "removeClausesAboveLevel(" << level << "): removing level-" << c.level() << " clause: " << c << ":"; - for(int i = 0; i < c.size(); ++i) { - Debug("minisat") << " " << c[i]; - } - Debug("minisat") << std::endl; - } - removeClause(cs[i]); + assert(!locked(c)); + removeClause(cs[i]); } else { - if(Debug.isOn("minisat")) { - Debug("minisat") << "removeClausesAboveLevel(" << level << "): leaving level-" << c.level() << " clause: " << c << ":"; - for(int i = 0; i < c.size(); ++i) { - Debug("minisat") << " " << c[i]; - } - Debug("minisat") << std::endl; - } cs[j++] = cs[i]; } } - Debug("minisat") << "removeClausesAboveLevel(" << level << "): removed " << i - j << " clauses in all, left " << j << std::endl; cs.shrink(i - j); } @@ -1408,10 +1460,8 @@ void Solver::push() popTrail(); ++assertionLevel; Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl; - trail_user.push(lit_Undef); trail_ok.push(ok); - trail_user_lim.push(trail.size()); - assert(trail_user_lim.size() == assertionLevel); + assigns_lim.push(assigns.size()); context->push(); // SAT context for CVC4 @@ -1422,83 +1472,44 @@ void Solver::pop() { assert(enable_incremental); - Debug("minisat") << "MINISAT POP at level " << decisionLevel() << " (context " << context->getLevel() << "), popping trail..." << std::endl; + // Pop the trail to 0 level popTrail(); - Debug("minisat") << "MINISAT POP now at " << decisionLevel() << " (context " << context->getLevel() << ")" << std::endl; - assert(decisionLevel() == 0); - assert(trail_user_lim.size() == assertionLevel); + // Pop the trail below the user level --assertionLevel; - - Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", need to get down to " << trail_user_lim.last() << std::endl; - Debug("minisat") << "in user pop, reducing assertion level to " << assertionLevel << " and removing clauses above this from db" << std::endl; - - // Remove all the clauses asserted (and implied) above the new base level - removeClausesAboveLevel(clauses_removable, assertionLevel); - removeClausesAboveLevel(clauses_persistent, assertionLevel); - - Debug("minisat") << "in user pop, at " << trail_lim.size() << " : " << assertionLevel << std::endl; - - int downto = trail_user_lim.last(); - while(downto < trail.size()) { + while (true) { Debug("minisat") << "== unassigning " << trail.last() << std::endl; Var x = var(trail.last()); - assigns [x] = l_Undef; - vardata[x].trail_index = -1; - if(phase_saving >= 1 && (polarity[x] & 0x2) == 0) - polarity[x] = sign(trail.last()); - if(intro_level(x) != -1) {// might be unregistered + if (user_level(x) > assertionLevel) { + assigns [x] = l_Undef; + vardata[x] = VarData(CRef_Undef, -1, -1, intro_level(x), -1); + if(phase_saving >= 1 && (polarity[x] & 0x2) == 0) + polarity[x] = sign(trail.last()); insertVarOrder(x); + trail.pop(); + } else { + break; } - trail.pop(); } + // The head should be at the trail top qhead = trail.size(); - Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", should be at " << trail_user_lim.last() << std::endl; - assert(trail_user_lim.last() == qhead); - trail_user_lim.pop(); - - // Unset any units learned or added at this level - Debug("minisat") << "in user pop, unsetting level units for level " << assertionLevel << std::endl; - while(trail_user.last() != lit_Undef) { - Lit l = trail_user.last(); - Debug("minisat") << "== unassigning " << l << std::endl; - Var x = var(l); - assigns [x] = l_Undef; - vardata[x].trail_index = -1; - if (phase_saving >= 1 && (polarity[x] & 0x2) == 0) - polarity[x] = sign(l); - if(intro_level(x) != -1) {// might be unregistered - insertVarOrder(x); - } - trail_user.pop(); - } - trail_user.pop(); - ok = trail_ok.last(); - trail_ok.pop(); - Debug("minisat") << "in user pop, done unsetting level units" << std::endl; - Debug("minisat") << "about to removeClausesAboveLevel(" << assertionLevel << ") in CNF" << std::endl; + // Remove the clause + removeClausesAboveLevel(clauses_persistent, assertionLevel); + removeClausesAboveLevel(clauses_removable, assertionLevel); + // Pop the SAT context to notify everyone context->pop(); // SAT context for CVC4 - // Notify the cnf - proxy->removeClausesAboveLevel(assertionLevel); -} - -void Solver::unregisterVar(Lit lit) { - Debug("minisat") << "unregisterVar " << lit << std::endl; - Var v = var(lit); - vardata[v].intro_level = -1; - setDecisionVar(v, false); -} + // Pop the created variables + resizeVars(assigns_lim.last()); + assigns_lim.pop(); + variables_to_register.clear(); -void Solver::renewVar(Lit lit, int level) { - Debug("minisat") << "renewVar " << lit << " " << level << std::endl; - Var v = var(lit); - vardata[v].intro_level = (level == -1 ? getAssertionLevel() : level); - setDecisionVar(v, true); - // explicitly not resetting polarity phase-locking here + // Pop the OK + ok = trail_ok.last(); + trail_ok.pop(); } bool Solver::flipDecision() { @@ -1599,7 +1610,16 @@ CRef Solver::updateLemmas() { // Attach it if non-unit CRef lemma_ref = CRef_Undef; if (lemma.size() > 1) { - lemma_ref = ca.alloc(assertionLevel, lemma, removable); + // If the lemmas is removable, we can compute its level by the level + int clauseLevel = assertionLevel; + if (removable) { + clauseLevel = 0; + for (int i = 0; i < lemma.size(); ++ i) { + clauseLevel = std::max(clauseLevel, intro_level(var(lemma[i]))); + } + } + + lemma_ref = ca.alloc(clauseLevel, lemma, removable); if (removable) { clauses_removable.push(lemma_ref); } else { diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index fdc9a98b7..0dad68a08 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -105,6 +105,9 @@ protected: /** Variables to re-register with theory solvers on backtracks */ vec<VarIntroInfo> variables_to_register; + /** Keep only newSize variables */ + void resizeVars(int newSize); + public: // Constructor/Destructor: @@ -151,9 +154,6 @@ public: void push (); void pop (); - void unregisterVar(Lit lit); // Unregister the literal (set assertion level to -1) - void renewVar(Lit lit, int level = -1); // Register the literal (set assertion level to the given level, or current level if -1) - bool addClause (const vec<Lit>& ps, bool removable); // Add a clause to the solver. bool addEmptyClause(bool removable); // Add the empty clause, making the solver contradictory. bool addClause (Lit p, bool removable); // Add a unit clause to the solver. @@ -258,8 +258,26 @@ protected: // Helper structures: // - struct VarData { CRef reason; int level; int intro_level; int trail_index; }; - static inline VarData mkVarData(CRef cr, int l, int intro_l, int trail_i){ VarData d = {cr, l, intro_l, trail_i}; return d; } + struct VarData { + // Reason for the literal being in the trail + CRef reason; + // Sat level when the literal was added to the trail + int level; + // User level when the literal was added to the trail + int user_level; + // Use level at which this literal was introduced + int intro_level; + // The index in the trail + int trail_index; + + VarData(CRef reason, int level, int user_level, int intro_level, int trail_index) + : reason(reason) + , level(level) + , user_level(user_level) + , intro_level(intro_level) + , trail_index(trail_index) + {} + }; struct Watcher { CRef cref; @@ -293,13 +311,12 @@ protected: OccLists<Lit, vec<Watcher>, WatcherDeleted> watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). vec<lbool> assigns; // The current assignments. + vec<int> assigns_lim; // The size by levels of the current assignment vec<char> polarity; // The preferred polarity of each variable (bit 0) and whether it's locked (bit 1). vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic. vec<int> flipped; // Which trail_lim decisions have been flipped in this context. vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made. vec<int> trail_lim; // Separator indices for different decision levels in 'trail'. - vec<Lit> trail_user; // Stack of assignments to UNdo on user pop. - vec<int> trail_user_lim; // Separator indices for different user levels in 'trail'. vec<bool> trail_ok; // Stack of "whether we're in conflict" flags. vec<VarData> vardata; // Stores reason and level for each variable. int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). @@ -361,7 +378,7 @@ protected: void popTrail (); // Backtrack the trail to the previous push position int analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack) void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? - int litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') - returns the maximal level of the clauses proving redundancy of p + bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') - true if p is redundant lbool search (int nof_conflicts); // Search for a given number of conflicts. lbool solve_ (); // Main solve method (assumptions given in 'assumptions'). void reduceDB (); // Reduce the set of learnt clauses. @@ -396,7 +413,8 @@ protected: bool isPropagatedBy (Var x, const Clause& c) const; // Is the value of the variable propagated by the clause Clause C int level (Var x) const; - int intro_level (Var x) const; // Level at which this variable was introduced + int user_level (Var x) const; // User level at which this variable was asserted + int intro_level (Var x) const; // User level at which this variable was created int trail_index (Var x) const; // Index in the trail double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... bool withinBudget () const; @@ -429,13 +447,16 @@ inline bool Solver::isPropagatedBy(Var x, const Clause& c) const { return vardat inline bool Solver::isDecision(Var x) const { Debug("minisat") << "var " << x << " is a decision iff " << (vardata[x].reason == CRef_Undef) << " && " << level(x) << " > 0" << std::endl; return vardata[x].reason == CRef_Undef && level(x) > 0; } -inline int Solver::level (Var x) const { return vardata[x].level; } +inline int Solver::level (Var x) const { assert(x < vardata.size()); return vardata[x].level; } + +inline int Solver::user_level(Var x) const { assert(x < vardata.size()); return vardata[x].user_level; } -inline int Solver::intro_level(Var x) const { return vardata[x].intro_level; } +inline int Solver::intro_level(Var x) const { assert(x < vardata.size()); return vardata[x].intro_level; } -inline int Solver::trail_index(Var x) const { return vardata[x].trail_index; } +inline int Solver::trail_index(Var x) const { assert(x < vardata.size()); return vardata[x].trail_index; } inline void Solver::insertVarOrder(Var x) { + assert(x < vardata.size()); if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); } inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); } @@ -476,8 +497,8 @@ inline void Solver::newDecisionLevel() { trail_lim.push inline int Solver::decisionLevel () const { return trail_lim.size(); } inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } -inline lbool Solver::value (Var x) const { return assigns[x]; } -inline lbool Solver::value (Lit p) const { return assigns[var(p)] ^ sign(p); } +inline lbool Solver::value (Var x) const { assert(x < nVars()); return assigns[x]; } +inline lbool Solver::value (Lit p) const { assert(var(p) < nVars()); return assigns[var(p)] ^ sign(p); } inline lbool Solver::modelValue (Var x) const { return model[x]; } inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); } inline int Solver::nAssigns () const { return trail.size(); } diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 9cd0d8848..fac4c92c1 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -340,6 +340,7 @@ class OccLists OccLists(const Deleted& d) : deleted(d) {} void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); } + void resizeTo (const Idx& idx){ int shrinkSize = occs.size() - (toInt(idx) + 1); occs.shrink(shrinkSize); } // Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; } Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; } Vec& lookup (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; } diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index e550d5ef2..886dc0f72 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -212,14 +212,6 @@ void MinisatSatSolver::pop(){ d_minisat->pop(); } -void MinisatSatSolver::unregisterVar(SatLiteral lit) { - d_minisat->unregisterVar(toMinisatLit(lit)); -} - -void MinisatSatSolver::renewVar(SatLiteral lit, int level) { - d_minisat->renewVar(toMinisatLit(lit), level); -} - /// Statistics for MinisatSatSolver MinisatSatSolver::Statistics::Statistics() : diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index f87e4ae53..723f257f7 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -80,10 +80,6 @@ public: void pop(); - void unregisterVar(SatLiteral lit); - - void renewVar(SatLiteral lit, int level = -1); - void requirePhase(SatLiteral lit); bool flipDecision(); diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index bf04cec8d..ed2dc04b9 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -98,10 +98,9 @@ SimpSolver::~SimpSolver() Var SimpSolver::newVar(bool sign, bool dvar, bool theoryAtom) { Var v = Solver::newVar(sign, dvar,theoryAtom); - frozen .push((char)theoryAtom); - eliminated.push((char)false); - if (use_simplification){ + frozen .push((char)theoryAtom); + eliminated.push((char)false); n_occ .push(0); n_occ .push(0); occurs .init(v); @@ -159,8 +158,10 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) bool SimpSolver::addClause_(vec<Lit>& ps, bool removable) { #ifndef NDEBUG - for (int i = 0; i < ps.size(); i++) + if (use_simplification) { + for (int i = 0; i < ps.size(); i++) assert(!isEliminated(var(ps[i]))); + } #endif int nclauses = clauses_persistent.size(); |