From: Dejan Jovanović Date: Wed, 17 Aug 2011 15:20:19 +0000 (+0000) Subject: new implementation of lemmas on demand X-Git-Tag: cvc5-1.0.0~8493 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=32e1d3558f17d12f2631175776209a5f8cabbdd9;p=cvc5.git new implementation of lemmas on demand comparison --- diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 36df53ca3..629e44e3e 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -46,9 +46,7 @@ CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar) } void CnfStream::recordTranslation(TNode node) { - if (d_assertingLemma) { - d_lemmas.push_back(stripNot(node)); - } else { + if (!d_removable) { d_translationTrail.push_back(stripNot(node)); } } @@ -59,7 +57,7 @@ TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registr void CnfStream::assertClause(TNode node, SatClause& c) { Debug("cnf") << "Inserting into stream " << c << endl; - d_satSolver->addClause(c, d_assertingLemma); + d_satSolver->addClause(c, d_removable); } void CnfStream::assertClause(TNode node, SatLiteral a) { @@ -123,9 +121,9 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { // If a theory literal, we pre-register it if (theoryLiteral) { - bool backup = d_assertingLemma; + bool backup = d_removable; d_registrar.preRegister(node); - d_assertingLemma = backup; + d_removable = backup; } // Here, you can have it @@ -372,10 +370,6 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { // If the non-negated node has already been translated, get the translation if(isTranslated(node)) { nodeLit = getLiteral(node); - // If we are asserting a lemma, we need to take the whole tree to level 0 - if (d_assertingLemma) { - moveToBaseLevel(node); - } } else { // Handle each Boolean operator case switch(node.getKind()) { @@ -425,13 +419,13 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { else return ~nodeLit; } -void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated) { +void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) { Assert(node.getKind() == AND); if (!negated) { // If the node is a conjunction, we handle each conjunct separately for(TNode::const_iterator conjunct = node.begin(), node_end = node.end(); conjunct != node_end; ++conjunct ) { - convertAndAssert(*conjunct, lemma, false); + convertAndAssert(*conjunct, false); } } else { // If the node is a disjunction, we construct a clause and assert it @@ -448,7 +442,7 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated) } } -void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool negated) { +void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) { Assert(node.getKind() == OR); if (!negated) { // If the node is a disjunction, we construct a clause and assert it @@ -466,12 +460,12 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool negated) // If the node is a conjunction, we handle each conjunct separately for(TNode::const_iterator conjunct = node.begin(), node_end = node.end(); conjunct != node_end; ++conjunct ) { - convertAndAssert(*conjunct, lemma, true); + convertAndAssert(*conjunct, true); } } } -void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated) { +void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) { if (!negated) { // p XOR q SatLiteral p = toCNF(node[0], false); @@ -503,7 +497,7 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated) recordTranslation(node[1]); } -void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated) { +void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) { if (!negated) { // p <=> q SatLiteral p = toCNF(node[0], false); @@ -535,7 +529,7 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated) recordTranslation(node[1]); } -void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool negated) { +void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) { if (!negated) { // p => q SatLiteral p = toCNF(node[0], false); @@ -549,12 +543,12 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool nega recordTranslation(node[1]); } else {// Construct the // !(p => q) is the same as (p && ~q) - convertAndAssert(node[0], lemma, false); - convertAndAssert(node[1], lemma, true); + convertAndAssert(node[0], false); + convertAndAssert(node[1], true); } } -void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated) { +void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) { // ITE(p, q, r) SatLiteral p = toCNF(node[0], false); SatLiteral q = toCNF(node[1], negated); @@ -578,30 +572,35 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated) // At the top level we must ensure that all clauses that are asserted are // not unit, except for the direct assertions. This allows us to remove the // clauses later when they are not needed anymore (lemmas for example). -void TseitinCnfStream::convertAndAssert(TNode node, bool lemma, bool negated) { - Debug("cnf") << "convertAndAssert(" << node << ", lemma = " << lemma << ", negated = " << (negated ? "true" : "false") << ")" << endl; - d_assertingLemma = lemma; +void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated) { + Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; + d_removable = removable; + convertAndAssert(node, negated); +} + +void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { + Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl; switch(node.getKind()) { case AND: - convertAndAssertAnd(node, lemma, negated); + convertAndAssertAnd(node, negated); break; case OR: - convertAndAssertOr(node, lemma, negated); + convertAndAssertOr(node, negated); break; case IFF: - convertAndAssertIff(node, lemma, negated); + convertAndAssertIff(node, negated); break; case XOR: - convertAndAssertXor(node, lemma, negated); + convertAndAssertXor(node, negated); break; case IMPLIES: - convertAndAssertImplies(node, lemma, negated); + convertAndAssertImplies(node, negated); break; case ITE: - convertAndAssertIte(node, lemma, negated); + convertAndAssertIte(node, negated); break; case NOT: - convertAndAssert(node[0], lemma, !negated); + convertAndAssert(node[0], !negated); break; default: // Atoms diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index e53b46d9b..fd0ab6291 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -77,9 +77,6 @@ protected: /** Top level nodes that we translated */ std::vector d_translationTrail; - /** Nodes belonging to asserted lemmas */ - std::vector d_lemmas; - /** Remove nots from the node */ TNode stripNot(TNode node) { while (node.getKind() == kind::NOT) { @@ -102,11 +99,11 @@ protected: void undoTranslate(TNode node, int level); /** - * Are we asserting a lemma (true) or a permanent clause (false). + * Are we asserting a removable clause (true) or a permanent clause (false). * This is set at the begining of convertAndAssert so that it doesn't * need to be passed on over the stack. */ - bool d_assertingLemma; + bool d_removable; /** * Asserts the given clause to the sat solver. @@ -187,10 +184,10 @@ public: /** * Converts and asserts a formula. * @param node node to convert and assert - * @param lemma whether the sat solver can choose to remove the clauses + * @param removable whether the sat solver can choose to remove the clauses * @param negated wheather we are asserting the node negated */ - virtual void convertAndAssert(TNode node, bool lemma, bool negated = false) = 0; + virtual void convertAndAssert(TNode node, bool removable, bool negated) = 0; /** * Get the node that is represented by the given SatLiteral. @@ -248,10 +245,10 @@ public: /** * Convert a given formula to CNF and assert it to the SAT solver. * @param node the formula to assert - * @param lemma is this a lemma that is erasable + * @param removable is this something that can be erased * @param negated true if negated */ - void convertAndAssert(TNode node, bool lemma, bool negated = false); + void convertAndAssert(TNode node, bool removable, bool negated); /** * Constructs the stream to use the given sat solver. @@ -262,6 +259,11 @@ public: private: + /** + * Same as above, except that removable is rememebered. + */ + void convertAndAssert(TNode node, bool negated); + // Each of these formulas handles takes care of a Node of each Kind. // // Each handleX(Node &n) is responsible for: @@ -280,12 +282,12 @@ private: SatLiteral handleAnd(TNode node); SatLiteral handleOr(TNode node); - void convertAndAssertAnd(TNode node, bool lemma, bool negated); - void convertAndAssertOr(TNode node, bool lemma, bool negated); - void convertAndAssertXor(TNode node, bool lemma, bool negated); - void convertAndAssertIff(TNode node, bool lemma, bool negated); - void convertAndAssertImplies(TNode node, bool lemma, bool negated); - void convertAndAssertIte(TNode node, bool lemma, bool negated); + void convertAndAssertAnd(TNode node, bool negated); + void convertAndAssertOr(TNode node, bool negated); + void convertAndAssertXor(TNode node, bool negated); + void convertAndAssertIff(TNode node, bool negated); + void convertAndAssertImplies(TNode node, bool negated); + void convertAndAssertIte(TNode node, bool negated); /** * Transforms the node into CNF recursively. diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 0c4f00875..a5774ee7b 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -47,6 +47,20 @@ static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interv static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false)); +class ScopedBool { + bool& watch; + bool oldValue; +public: + ScopedBool(bool& watch, bool newValue) + : watch(watch), oldValue(watch) { + watch = newValue; + } + ~ScopedBool() { + watch = oldValue; + } +}; + + //================================================================================================= // Constructor/Destructor: @@ -55,8 +69,7 @@ Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bo , context(context) , assertionLevel(0) , enable_incremental(enable_incremental) - , problem_extended(false) - , in_solve(false) + , minisat_busy(false) // Parameters (user settable): // , verbosity (0) @@ -121,30 +134,26 @@ Solver::~Solver() Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) { int v = nVars(); + watches .init(mkLit(v, false)); watches .init(mkLit(v, true )); assigns .push(l_Undef); - vardata .push(mkVarData(CRef_Undef, 0, assertionLevel)); - //activity .push(0); + vardata .push(mkVarData(CRef_Undef, 0, assertionLevel, 0)); activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0); seen .push(0); polarity .push(sign); decision .push(); trail .capacity(v+1); - setDecisionVar(v, dvar); theory .push(theoryAtom); - // We have extended the problem - if (in_solve) { - problem_extended = true; - insertVarOrder(v); - } + setDecisionVar(v, dvar); return v; } -CRef Solver::reason(Var x) const { +CRef Solver::reason(Var x) { + // If we already have a reason, just return it if (vardata[x].reason != CRef_Lazy) return vardata[x].reason; @@ -154,11 +163,12 @@ CRef Solver::reason(Var x) const { // Get the explanation from the theory SatClause explanation; proxy->explainPropagation(l, explanation); + + // Sort the literals by trail index level + lemma_lt lt(*this); + sort(explanation, lt); Assert(explanation[0] == l); - // We're actually changing the state, so we hack it into non-const - Solver* nonconst_this = const_cast(this); - // Compute the assertion level for this clause int explLevel = 0; for (int i = 0; i < explanation.size(); ++ i) { @@ -169,105 +179,54 @@ CRef Solver::reason(Var x) const { } // Construct the reason (level 0) - // TODO compute the level - CRef real_reason = nonconst_this->ca.alloc(explLevel, explanation, true); - nonconst_this->vardata[x] = mkVarData(real_reason, level(x), intro_level(x)); - nonconst_this->learnts.push(real_reason); - nonconst_this->attachClause(real_reason); + CRef real_reason = ca.alloc(explLevel, explanation, true); + vardata[x] = mkVarData(real_reason, level(x), intro_level(x), trail_index(x)); + clauses_removable.push(real_reason); + attachClause(real_reason); return real_reason; } -bool Solver::addClause_(vec& ps, ClauseType type) +bool Solver::addClause_(vec& ps, bool removable) { if (!ok) return false; - bool propagate_first_literal = false; - // Check if clause is satisfied and remove false/duplicate literals: sort(ps); Lit p; int i, j; - if (type != CLAUSE_LEMMA) { - // Problem clause - for (i = j = 0, p = lit_Undef; i < ps.size(); i++) - if (value(ps[i]) == l_True || ps[i] == ~p) - return true; - else if (value(ps[i]) != l_False && ps[i] != p) - ps[j++] = p = ps[i]; - ps.shrink(i - j); - } else { - // Lemma - vec assigned_lits; - Debug("minisat::lemmas") << "Asserting lemma with " << ps.size() << " literals." << std::endl; - bool lemmaSatisfied = false; - for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { - if (ps[i] == ~p) { - // We don't add clauses that represent splits directly, they are decision literals - // so they will get decided upon and sent to the theory - Debug("minisat::lemmas") << "Lemma is a tautology." << std::endl; - return true; - } - if (value(ps[i]) == l_Undef) { - // Anything not having a value gets added - if (ps[i] != p) { - ps[j++] = p = ps[i]; - } - } else { - // If the literal has a value it gets added to the end of the clause - p = ps[i]; - if (value(p) == l_True) lemmaSatisfied = true; - assigned_lits.push(p); - Debug("minisat::lemmas") << proxy->getNode(p) << " has value " << value(p) << std::endl; - } - } - Assert(j >= 1 || lemmaSatisfied, "You are asserting a falsified lemma, produce a conflict instead!"); - // If only one literal we could have unit propagation - if (j == 1 && !lemmaSatisfied) propagate_first_literal = true; - int max_level = -1; - int max_level_j = -1; - for (int assigned_i = 0; assigned_i < assigned_lits.size(); ++ assigned_i) { - ps[j++] = p = assigned_lits[assigned_i]; - if (level(var(p)) > max_level && value(p) == l_False) { - max_level = level(var(p)); - max_level_j = j - 1; - } - } - if (value(ps[1]) != l_Undef && max_level != -1) { - std::swap(ps[1], ps[max_level_j]); - } - ps.shrink(i - j); + + // Check the clause for tautologies and similar + 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)) { + // 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]; + } } - if (ps.size() == 0) - return ok = false; - else if (ps.size() == 1){ - if(in_solve) { - assert(type != CLAUSE_LEMMA); - assert(value(ps[0]) == l_Undef); - } else { - // [MGD] at "pre-solve" time we allow unit T-lemmas - if(value(ps[0]) == l_True) { - // this unit T-lemma is extraneous (perhaps it was - // discovered twice at presolve time) - return true; - } - assert(value(ps[0]) == l_Undef); - } + // Fit to size + ps.shrink(i - j); + + + // If we are in solve or decision level > 0 + if (minisat_busy || decisionLevel() > 0) { + lemmas.push(); + ps.copyTo(lemmas.last()); + lemmas_removable.push(removable); + } else { + // Add the clause and attach if not a lemma + if (ps.size() == 0) { + return ok = false; + } else if (ps.size() == 1) { uncheckedEnqueue(ps[0]); return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef); - }else{ - CRef cr = ca.alloc(type == CLAUSE_LEMMA ? 0 : assertionLevel, ps, false); - clauses.push(cr); + } else { + CRef cr = ca.alloc(assertionLevel, ps, false); + clauses_persistent.push(cr); attachClause(cr); - if (propagate_first_literal) { - Debug("minisat::lemmas") << "Lemma propagating: " << (theory[var(ps[0])] ? proxy->getNode(ps[0]).toString() : "bool") << std::endl; - lemma_propagated_literals.push(ps[0]); - lemma_propagated_reasons.push(cr); - propagating_lemmas.push(cr); - } - } - - if (type == CLAUSE_LEMMA) { - problem_extended = true; + } } return true; @@ -280,7 +239,7 @@ void Solver::attachClause(CRef cr) { Assert(c.size() > 1); watches[~c[0]].push(Watcher(cr, c[1])); watches[~c[1]].push(Watcher(cr, c[0])); - if (c.learnt()) learnts_literals += c.size(); + if (c.removable()) learnts_literals += c.size(); else clauses_literals += c.size(); } @@ -298,7 +257,7 @@ void Solver::detachClause(CRef cr, bool strict) { watches.smudge(~c[1]); } - if (c.learnt()) learnts_literals -= c.size(); + if (c.removable()) learnts_literals -= c.size(); else clauses_literals -= c.size(); } @@ -322,7 +281,7 @@ bool Solver::satisfied(const Clause& c) const { // Revert to the state at given level (keeping all assignment at 'level' but not beyond). // -void Solver::cancelUntil(int level, bool re_propagate) { +void Solver::cancelUntil(int level) { if (decisionLevel() > level){ // Pop the SMT context for (int l = trail_lim.size() - level; l > 0; --l) @@ -336,49 +295,7 @@ void Solver::cancelUntil(int level, bool re_propagate) { qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); - - // Re-Propagate the lemmas if asked - if (re_propagate) { - rePropagate(level); - } - } -} - -CRef Solver::rePropagate(int level) { - // Propagate the lemma literals - int i, j; - for (i = j = propagating_lemmas_lim[level]; i < propagating_lemmas.size(); ++ i) { - Clause& lemma = ca[propagating_lemmas[i]]; - bool propagating = value(var(lemma[0])) == l_Undef;; - for(int lit = 1; lit < lemma.size() && propagating; ++ lit) { - if (value(var(lemma[lit])) != l_False) { - propagating = false; - break; - } - } - if (propagating) { - if (value(lemma[0]) != l_Undef) { - if (value(lemma[0]) == l_False) { - // Conflict - return propagating_lemmas[i]; - } else { - // Already there - continue; - } - } - // Propagate - uncheckedEnqueue(lemma[0], propagating_lemmas[i]); - // Remember the lemma - propagating_lemmas[j++] = propagating_lemmas[i]; } - } - Assert(i >= j); - propagating_lemmas.shrink(propagating_lemmas.size() - j); - Assert(propagating_lemmas_lim.size() >= level); - propagating_lemmas_lim.shrink(propagating_lemmas_lim.size() - level); - - // No conflict - return CRef_Undef; } void Solver::popTrail() { @@ -470,7 +387,7 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) max_level = c.level(); } - if (c.learnt()) + if (c.removable()) claBumpActivity(c); for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ @@ -650,7 +567,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) { assert(value(p) == l_Undef); assigns[var(p)] = lbool(!sign(p)); - vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p))); + vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size()); trail.push_(p); if (theory[var(p)]) { // Enqueue to the theory @@ -663,11 +580,25 @@ CRef Solver::propagate(TheoryCheckType type) { CRef confl = CRef_Undef; + ScopedBool scoped_bool(minisat_busy, true); + + // If we are not in the quick mode add the lemmas that were left begind + if (type != CHECK_WITHOUTH_PROPAGATION_QUICK && lemmas.size() > 0) { + confl = updateLemmas(); + if (confl != CRef_Undef) { + return confl; + } + } + // If this is the final check, no need for Boolean propagation and // theory propagation if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) { - confl = theoryCheck(CVC4::theory::Theory::FULL_EFFORT); - return confl; + // Do the theory check + theoryCheck(CVC4::theory::Theory::FULL_EFFORT); + // If there are lemmas (or conflicts) update them + if (lemmas.size() > 0) { + return updateLemmas(); + } } // The effort we will be using to theory check @@ -677,26 +608,36 @@ CRef Solver::propagate(TheoryCheckType type) // Keep running until we have checked everything, we // have no conflict and no new literals have been asserted - bool new_assertions; do { - new_assertions = false; - while(qhead < trail.size()) { - confl = propagateBool(); - if (confl != CRef_Undef) break; - confl = theoryCheck(effort); - if (confl != CRef_Undef) break; - } + do { + // Propagate on the clauses + confl = propagateBool(); + + // If no conflict, do the theory check + if (confl == CRef_Undef) { + // Do the theory check + theoryCheck(effort); + // If there are lemmas (or conflicts) update them + if (lemmas.size() > 0) { + confl = updateLemmas(); + } + } + } while (confl == CRef_Undef && qhead < trail.size()); + // If still consistent do some theory propagation if (confl == CRef_Undef && type == CHECK_WITH_PROPAGATION_STANDARD) { - new_assertions = propagateTheory(); - if (!new_assertions) break; + propagateTheory(); + if (lemmas.size() > 0) { + confl = updateLemmas(); + } } - } while (new_assertions); + + } while (confl == CRef_Undef && qhead < trail.size()); return confl; } -bool Solver::propagateTheory() { +void Solver::propagateTheory() { std::vector propagatedLiterals; proxy->theoryPropagate(propagatedLiterals); const unsigned i_end = propagatedLiterals.size(); @@ -705,7 +646,6 @@ bool Solver::propagateTheory() { uncheckedEnqueue(propagatedLiterals[i], CRef_Lazy); } proxy->clearPropagatedLiterals(); - return propagatedLiterals.size() > 0; } /*_________________________________________________________________________________________________ @@ -718,43 +658,9 @@ bool Solver::propagateTheory() { | | Note: the propagation queue might be NOT empty |________________________________________________________________________________________________@*/ -CRef Solver::theoryCheck(CVC4::theory::Theory::Effort effort) +void Solver::theoryCheck(CVC4::theory::Theory::Effort effort) { - CRef c = CRef_Undef; - SatClause clause; - proxy->theoryCheck(effort, clause); - int clause_size = clause.size(); - if(clause_size > 0) { - // Find the max level of the conflict - int max_level = 0; - int max_intro_level = 0; - for (int i = 0; i < clause_size; ++i) { - Var v = var(clause[i]); - int current_level = level(v); - int current_intro_level = intro_level(v); - Debug("minisat") << "Literal: " << clause[i] << " with reason " << reason(v) << " at level " << current_level << std::endl; - Assert(value(clause[i]) != l_Undef, "Got an unassigned literal in conflict!"); - if (current_level > max_level) max_level = current_level; - if (current_intro_level > max_intro_level) max_intro_level = current_intro_level; - } - // Unit conflict, we just duplicate the first literal - if (clause_size == 1) { - clause.push(clause[0]); - Debug("unit-conflict") << "Unit conflict" << proxy->getNode(clause[0]) << std::endl; - } - // If smaller than the decision level then pop back so we can analyse - Debug("minisat") << "Max-level is " << max_level << " in decision level " << decisionLevel() << std::endl; - Assert(max_level <= decisionLevel(), "What is going on, can't get literals of a higher level as conflict!"); - if (max_level < decisionLevel()) { - Debug("minisat") << "Max-level is " << max_level << " in decision level " << decisionLevel() << std::endl; - cancelUntil(max_level); - } - // Create the new clause and attach all the information (level 0) - c = ca.alloc(max_intro_level, clause, true); - learnts.push(c); - attachClause(c); - } - return c; + proxy->theoryCheck(effort); } /*_________________________________________________________________________________________________ @@ -848,19 +754,19 @@ struct reduceDB_lt { void Solver::reduceDB() { int i, j; - double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity + double extra_lim = cla_inc / clauses_removable.size(); // Remove any clause below this activity - sort(learnts, reduceDB_lt(ca)); + sort(clauses_removable, reduceDB_lt(ca)); // Don't delete binary or locked clauses. From the rest, delete clauses from the first half // and clauses with activity smaller than 'extra_lim': - for (i = j = 0; i < learnts.size(); i++){ - Clause& c = ca[learnts[i]]; - if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim)) - removeClause(learnts[i]); + for (i = j = 0; i < clauses_removable.size(); i++){ + Clause& c = ca[clauses_removable[i]]; + if (c.size() > 2 && !locked(c) && (i < clauses_removable.size() / 2 || c.activity() < extra_lim)) + removeClause(clauses_removable[i]); else - learnts[j++] = learnts[i]; + clauses_removable[j++] = clauses_removable[i]; } - learnts.shrink(i - j); + clauses_removable.shrink(i - j); checkGarbage(); } @@ -920,9 +826,9 @@ bool Solver::simplify() return true; // Remove satisfied clauses: - removeSatisfied(learnts); + removeSatisfied(clauses_removable); if (remove_satisfied) // Can be turned off. - removeSatisfied(clauses); + removeSatisfied(clauses_persistent); checkGarbage(); rebuildOrderHeap(); @@ -955,57 +861,33 @@ lbool Solver::search(int nof_conflicts) starts++; TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD; - for (;;){ + for (;;) { - // If we have more assertions from lemmas, we continue - if (problem_extended) { - - Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << std::endl; + // Propagate and call the theory solvers + CRef confl = propagate(check_type); + Assert(lemmas.size() == 0); - for (int i = 0, i_end = lemma_propagated_literals.size(); i < i_end; ++ i) { - if (value(var(lemma_propagated_literals[i])) == l_Undef) { - Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << std::endl; - uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]); - } - } + if (confl != CRef_Undef) { - lemma_propagated_literals.clear(); - lemma_propagated_reasons.clear(); + conflicts++; conflictC++; - check_type = CHECK_WITH_PROPAGATION_STANDARD; - problem_extended = false; - } + if (decisionLevel() == 0) return l_False; - CRef confl = propagate(check_type); - if (confl != CRef_Undef){ - // Clear the propagated literals - lemma_propagated_literals.clear(); - lemma_propagated_reasons.clear(); - - // CONFLICT - while (confl != CRef_Undef) { - conflicts++; conflictC++; - if (decisionLevel() == 0) return l_False; - - // Analyze the conflict - learnt_clause.clear(); - int max_level = analyze(confl, learnt_clause, backtrack_level); - cancelUntil(backtrack_level, false); - - // Assert the conflict clause and the asserting literal - if (learnt_clause.size() == 1){ - uncheckedEnqueue(learnt_clause[0]); - }else{ - CRef cr = ca.alloc(max_level, learnt_clause, true); - learnts.push(cr); - attachClause(cr); - claBumpActivity(ca[cr]); - uncheckedEnqueue(learnt_clause[0], cr); - } + // Analyze the conflict + learnt_clause.clear(); + int max_level = analyze(confl, learnt_clause, backtrack_level); + cancelUntil(backtrack_level); - // We repropagate lemmas - confl = rePropagate(backtrack_level); - }; + // Assert the conflict clause and the asserting literal + if (learnt_clause.size() == 1) { + uncheckedEnqueue(learnt_clause[0]); + } else { + CRef cr = ca.alloc(max_level, learnt_clause, true); + clauses_removable.push(cr); + attachClause(cr); + claBumpActivity(ca[cr]); + uncheckedEnqueue(learnt_clause[0], cr); + } varDecayActivity(); claDecayActivity(); @@ -1022,52 +904,59 @@ lbool Solver::search(int nof_conflicts) (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); } - // We have a conflict so, we are going back to standard checks + // We have a conflict so, we are going back to standard checks check_type = CHECK_WITH_PROPAGATION_STANDARD; - }else{ - - // NO CONFLICT - if (problem_extended) - continue; + } else { // If this was a final check, we are satisfiable - if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) - return l_True; + if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) { + // Unless a lemma has added more stuff to the queues + if (!order_heap.empty() || qhead < trail.size()) { + check_type = CHECK_WITH_PROPAGATION_STANDARD; + continue; + } else { + // Yes, we're truly satisfiable + return l_True; + } + } - if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){ + if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()) { // Reached bound on number of conflicts: progress_estimate = progressEstimate(); cancelUntil(0); // [mdeters] notify theory engine of restarts for deferred // theory processing proxy->notifyRestart(); - return l_Undef; } + return l_Undef; + } // Simplify the set of problem clauses: - if (decisionLevel() == 0 && !simplify()) + if (decisionLevel() == 0 && !simplify()) { return l_False; + } - if (learnts.size()-nAssigns() >= max_learnts) + if (clauses_removable.size()-nAssigns() >= max_learnts) { // Reduce the set of learnt clauses: reduceDB(); + } Lit next = lit_Undef; - while (decisionLevel() < assumptions.size()){ + while (decisionLevel() < assumptions.size()) { // Perform user provided assumption: Lit p = assumptions[decisionLevel()]; - if (value(p) == l_True){ + if (value(p) == l_True) { // Dummy decision level: newDecisionLevel(); - }else if (value(p) == l_False){ + } else if (value(p) == l_False) { analyzeFinal(~p, conflict); return l_False; - }else{ + } else { next = p; break; } } - if (next == lit_Undef){ + if (next == lit_Undef) { // New variable decision: decisions++; next = pickBranchLit(); @@ -1138,12 +1027,12 @@ lbool Solver::solve_() { Debug("minisat") << "nvars = " << nVars() << std::endl; - in_solve = true; + ScopedBool scoped_bool(minisat_busy, true); model.clear(); conflict.clear(); if (!ok){ - in_solve = false; + minisat_busy = false; return l_False; } @@ -1187,8 +1076,6 @@ lbool Solver::solve_() // Cancel the trail downto previous push popTrail(); - in_solve = false; - return status; } @@ -1240,13 +1127,13 @@ void Solver::toDimacs(FILE* f, const vec& assumps) // Cannot use removeClauses here because it is not safe // to deallocate them at this point. Could be improved. int cnt = 0; - for (int i = 0; i < clauses.size(); i++) - if (!satisfied(ca[clauses[i]])) + for (int i = 0; i < clauses_persistent.size(); i++) + if (!satisfied(ca[clauses_persistent[i]])) cnt++; - for (int i = 0; i < clauses.size(); i++) - if (!satisfied(ca[clauses[i]])){ - Clause& c = ca[clauses[i]]; + for (int i = 0; i < clauses_persistent.size(); i++) + if (!satisfied(ca[clauses_persistent[i]])){ + Clause& c = ca[clauses_persistent[i]]; for (int j = 0; j < c.size(); j++) if (value(c[j]) != l_False) mapVar(var(c[j]), map, max); @@ -1262,8 +1149,8 @@ void Solver::toDimacs(FILE* f, const vec& assumps) fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1); } - for (int i = 0; i < clauses.size(); i++) - toDimacs(f, ca[clauses[i]], map, max); + for (int i = 0; i < clauses_persistent.size(); i++) + toDimacs(f, ca[clauses_persistent[i]], map, max); if (verbosity > 0) printf("Wrote %d clauses with %d variables.\n", cnt, max); @@ -1293,26 +1180,19 @@ void Solver::relocAll(ClauseAllocator& to) for (int i = 0; i < trail.size(); i++){ Var v = var(trail[i]); - if (hasReason(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) + if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) ca.reloc(vardata[v].reason, to); } // All learnt: // - for (int i = 0; i < learnts.size(); i++) - ca.reloc(learnts[i], to); + for (int i = 0; i < clauses_removable.size(); i++) + ca.reloc(clauses_removable[i], to); // All original: // - for (int i = 0; i < clauses.size(); i++) - ca.reloc(clauses[i], to); - - // All lemmas - // - for (int i = 0; i < lemma_propagated_reasons.size(); i ++) - ca.reloc(lemma_propagated_reasons[i], to); - for (int i = 0; i < propagating_lemmas.size(); i ++) - ca.reloc(propagating_lemmas[i], to); + for (int i = 0; i < clauses_persistent.size(); i++) + ca.reloc(clauses_persistent[i], to); } @@ -1342,8 +1222,8 @@ void Solver::pop() if (enable_incremental) { -- assertionLevel; // Remove all the clauses asserted (and implied) above the new base level - removeClausesAboveLevel(learnts, assertionLevel); - removeClausesAboveLevel(clauses, assertionLevel); + removeClausesAboveLevel(clauses_removable, assertionLevel); + removeClausesAboveLevel(clauses_persistent, assertionLevel); // Pop the user trail size popTrail(); @@ -1366,4 +1246,101 @@ void Solver::renewVar(Lit lit, int level) { setDecisionVar(v, true); } +CRef Solver::updateLemmas() { + + Debug("minisat::lemmas") << "Solver::updateLemmas()" << std::endl; + + CRef conflict = CRef_Undef; + + // Decision level to backtrack to + int backtrackLevel = decisionLevel(); + + // We use this comparison operator + lemma_lt lt(*this); + + // Check for propagation and level to backtrack to + for (int i = 0; i < lemmas.size(); ++ i) + { + // The current lemma + vec& lemma = lemmas[i]; + // If it's an empty lemma, we have a conflict at zero level + if (lemma.size() == 0) { + conflict = CRef_Lazy; + backtrackLevel = 0; + Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl; + continue; + } + // Sort the lemma to be able to attach + sort(lemma, lt); + // See if the lemma propagates something + if (lemma.size() == 1 || value(lemma[1]) == l_False) { + // This lemma propagates, see which level we need to backtrack to + int currentBacktrackLevel = lemma.size() == 1 ? 0 : level(var(lemma[1])); + // Even if the first literal is true, we should propagate it at this level (unless it's set at a lower level) + if (value(lemma[0]) != l_True || level(var(lemma[0])) > currentBacktrackLevel) { + if (currentBacktrackLevel < backtrackLevel) { + backtrackLevel = currentBacktrackLevel; + } + } + } + } + + // Pop so that propagation would be current + Debug("minisat::lemmas") << "Solver::updateLemmas(): backtracking to " << backtrackLevel << " from " << decisionLevel() << std::endl; + cancelUntil(backtrackLevel); + + // Last index in the trail + int backtrack_index = trail.size(); + + // Attach all the clauses and enqueue all the propagations + for (int i = 0; i < lemmas.size(); ++ i) + { + // The current lemma + vec& lemma = lemmas[i]; + bool removable = lemmas_removable[i]; + + // Attach it if non-unit + CRef lemma_ref = CRef_Undef; + if (lemma.size() > 1) { + lemma_ref = ca.alloc(assertionLevel, lemma, removable); + if (removable) { + clauses_removable.push(lemma_ref); + } else { + clauses_persistent.push(lemma_ref); + } + attachClause(lemma_ref); + } + + // If the lemma is propagating enqueue it's literal (or set the conflict) + if (conflict == CRef_Undef && value(lemma[0]) != l_True) { + if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) { + if (value(lemma[0]) == l_False) { + // We have a conflict + if (lemma.size() > 1) { + Debug("minisat::lemmas") << "Solver::updateLemmas(): conflict" << std::endl; + conflict = lemma_ref; + } else { + Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl; + conflict = CRef_Lazy; + } + } else { +// if (Debug.isOn("minisat::lemmas")) { +// Debug("minisat::lemmas") << "Solver::updateLemmas(): " << lemma[0] << " from "; +// Clause& c = ca[lemma_ref]; +// for (int i = 0; i < c.size(); ++ i) { +// Debug("minisat::lemmas") << c[i] << "(" << value(c[i]) << "," << level(var(c[i])) << "," << trail_index(var(c[i])) << ") "; +// } +// Debug("minisat::lemmas") << std::endl; +// } + uncheckedEnqueue(lemma[0], lemma_ref); + } + } + } + } + + // Clear the lemmas + lemmas.clear(); + lemmas_removable.clear(); + return conflict; +} diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 1eb407c62..8eb82d9f1 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -65,22 +65,17 @@ protected: /** Do we allow incremental solving */ bool enable_incremental; - /** Did the problem get extended in the meantime (i.e. by adding a lemma) */ - bool problem_extended; - /** Literals propagated by lemmas */ - vec lemma_propagated_literals; - /** Reasons of literals propagated by lemmas */ - vec lemma_propagated_reasons; - /** Lemmas that propagated something, we need to recheck them after backtracking */ - vec propagating_lemmas; - vec propagating_lemmas_lim; + vec< vec > lemmas; + + /** Is the lemma removable */ + vec lemmas_removable; /** Shrink 'cs' to contain only clauses below given level */ void removeClausesAboveLevel(vec& cs, int level); /** True if we are currently solving. */ - bool in_solve; + bool minisat_busy; public: @@ -93,16 +88,35 @@ public: // Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode. - // Types of clauses - enum ClauseType { - // Clauses defined by the problem - CLAUSE_PROBLEM, - // Lemma clauses added by the theories - CLAUSE_LEMMA, - // Conflict clauses - CLAUSE_CONFLICT + // Less than for literals in a lemma + struct lemma_lt { + Solver& solver; + lemma_lt(Solver& solver) : solver(solver) {} + bool operator () (Lit x, Lit y) { + lbool x_value = solver.value(x); + lbool y_value = solver.value(y); + // Two unassigned literals are sorted arbitrarily + if (x_value == l_Undef && y_value == l_Undef) { + return x < y; + } + // Unassigned literals are put to front + if (x_value == l_Undef) return true; + if (y_value == l_Undef) return false; + // Literals of the same value are sorted by decreasing levels + if (x_value == y_value) { + return solver.trail_index(var(x)) > solver.trail_index(var(y)); + } else { + // True literals go up front + if (x_value == l_True) { + return true; + } else { + return false; + } + } + } }; + // CVC4 context push/pop void push (); void pop (); @@ -110,12 +124,12 @@ public: 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& ps, ClauseType type); // Add a clause to the solver. - bool addEmptyClause(ClauseType type); // Add the empty clause, making the solver contradictory. - bool addClause (Lit p, ClauseType type); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, ClauseType type); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, ClauseType type); // Add a ternary clause to the solver. - bool addClause_( vec& ps, ClauseType type); // Add a clause to the solver without making superflous internal copy. Will + bool addClause (const vec& 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. + bool addClause (Lit p, Lit q, bool removable); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver. + bool addClause_( vec& ps, bool removable); // Add a clause to the solver without making superflous internal copy. Will // change the passed vector 'ps'. // Solving: @@ -207,8 +221,8 @@ protected: // Helper structures: // - struct VarData { CRef reason; int level; int intro_level; }; - static inline VarData mkVarData(CRef cr, int l, int intro_l){ VarData d = {cr, l, intro_l}; return d; } + 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 Watcher { CRef cref; @@ -233,28 +247,28 @@ protected: // Solver state: // - bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! - vec clauses; // List of problem clauses. - vec learnts; // List of learnt clauses. - double cla_inc; // Amount to bump next clause with. - vec activity; // A heuristic measurement of the activity of a variable. - double var_inc; // Amount to bump next variable with. + bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! + vec clauses_persistent; // List of problem clauses. + vec clauses_removable; // List of learnt clauses. + double cla_inc; // Amount to bump next clause with. + vec activity; // A heuristic measurement of the activity of a variable. + double var_inc; // Amount to bump next variable with. OccLists, WatcherDeleted> - watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). - vec assigns; // The current assignments. - vec polarity; // The preferred polarity of each variable. - vec decision; // Declares if a variable is eligible for selection in the decision heuristic. - vec trail; // Assignment stack; stores all assigments made in the order they were made. - vec trail_lim; // Separator indices for different decision levels in 'trail'. - vec trail_user_lim; // Separator indices for different user push levels in 'trail'. - vec 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). - int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'. - int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'. - vec assumptions; // Current set of assumptions provided to solve by the user. - Heap order_heap; // A priority queue of variables ordered with respect to the variable activity. - double progress_estimate;// Set by 'search()'. - bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'. + watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). + vec assigns; // The current assignments. + vec polarity; // The preferred polarity of each variable. + vec decision; // Declares if a variable is eligible for selection in the decision heuristic. + vec trail; // Assignment stack; stores all assigments made in the order they were made. + vec trail_lim; // Separator indices for different decision levels in 'trail'. + vec trail_user_lim; // Separator indices for different user push levels in 'trail'. + vec 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). + int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'. + int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'. + vec assumptions; // Current set of assumptions provided to solve by the user. + Heap order_heap; // A priority queue of variables ordered with respect to the variable activity. + double progress_estimate; // Set by 'search()'. + bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'. ClauseAllocator ca; @@ -297,10 +311,10 @@ protected: bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise. CRef propagate (TheoryCheckType type); // Perform Boolean and Theory. Returns possibly conflicting clause. CRef propagateBool (); // Perform Boolean propagation. Returns possibly conflicting clause. - bool propagateTheory (); // Perform Theory propagation. Return true if any literals were asserted. - CRef theoryCheck (CVC4::theory::Theory::Effort effort); // Perform a theory satisfiability check. Returns possibly conflicting clause. - void cancelUntil (int level, bool re_propagate = true); // Backtrack until a certain level. - CRef rePropagate (int level); // Re-propagate on lemmas, returns a concflict clause if it introduces a conflict + void propagateTheory (); // Perform Theory propagation. + void theoryCheck (CVC4::theory::Theory::Effort effort); // Perform a theory satisfiability check. Adds lemmas. + CRef updateLemmas (); // Add the lemmas, backtraking if necessary and return a conflict if there is one + void cancelUntil (int level); // Backtrack until a certain level. void popTrail (); // Backtrack the trail to the previous push position int analyze (CRef confl, vec& out_learnt, int& out_btlevel); // (bt = backtrack) void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? @@ -333,10 +347,14 @@ protected: // int decisionLevel () const; // Gives the current decisionlevel. uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels. - CRef reason (Var x) const; - bool hasReason (Var x) const; // Does the variable have a reason + CRef reason (Var x); // Get the reason of the variable (non const as it might create the explanation on the fly) + bool hasReasonClause (Var x) const; // Does the variable have a reason + bool isPropagated (Var x) const; // Does the variable have a propagated variables + 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 trail_index (Var x) const; // Index in the trail double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... bool withinBudget () const; @@ -360,12 +378,18 @@ protected: //================================================================================================= // Implementation of inline methods: -inline bool Solver::hasReason(Var x) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy; } +inline bool Solver::hasReasonClause(Var x) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy; } + +inline bool Solver::isPropagated(Var x) const { return vardata[x].reason != CRef_Undef; } + +inline bool Solver::isPropagatedBy(Var x, const Clause& c) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy && ca.lea(vardata[var(c[0])].reason) == &c; } inline int Solver::level (Var x) const { return vardata[x].level; } inline int Solver::intro_level(Var x) const { return vardata[x].intro_level; } +inline int Solver::trail_index(Var x) const { return vardata[x].trail_index; } + inline void Solver::insertVarOrder(Var x) { if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); } @@ -386,8 +410,8 @@ inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); } inline void Solver::claBumpActivity (Clause& c) { if ( (c.activity() += cla_inc) > 1e20 ) { // Rescale: - for (int i = 0; i < learnts.size(); i++) - ca[learnts[i]].activity() *= 1e-20; + for (int i = 0; i < clauses_removable.size(); i++) + ca[clauses_removable[i]].activity() *= 1e-20; cla_inc *= 1e-20; } } inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); } @@ -397,13 +421,13 @@ inline void Solver::checkGarbage(double gf){ // NOTE: enqueue does not set the ok flag! (only public methods do) inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); } -inline bool Solver::addClause (const vec& ps, ClauseType type) { ps.copyTo(add_tmp); return addClause_(add_tmp, type); } -inline bool Solver::addEmptyClause (ClauseType type) { add_tmp.clear(); return addClause_(add_tmp, type); } -inline bool Solver::addClause (Lit p, ClauseType type) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, type); } -inline bool Solver::addClause (Lit p, Lit q, ClauseType type) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, type); } -inline bool Solver::addClause (Lit p, Lit q, Lit r, ClauseType type) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, type); } -inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; } -inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); propagating_lemmas_lim.push(propagating_lemmas.size()); context->push(); } +inline bool Solver::addClause (const vec& ps, bool removable) { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); } +inline bool Solver::addEmptyClause (bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable); } +inline bool Solver::addClause (Lit p, bool removable) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); } +inline bool Solver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); } +inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); } +inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); } +inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); context->push(); } inline int Solver::decisionLevel () const { return trail_lim.size(); } inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } @@ -412,8 +436,8 @@ inline lbool Solver::value (Lit p) const { return assigns[var(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(); } -inline int Solver::nClauses () const { return clauses.size(); } -inline int Solver::nLearnts () const { return learnts.size(); } +inline int Solver::nClauses () const { return clauses_persistent.size(); } +inline int Solver::nLearnts () const { return clauses_removable.size(); } inline int Solver::nVars () const { return vardata.size(); } inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); } inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; } diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 5fdabb2f1..1aff5094d 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -124,7 +124,7 @@ typedef RegionAllocator::Ref CRef; class Clause { struct { unsigned mark : 2; - unsigned learnt : 1; + unsigned removable : 1; unsigned has_extra : 1; unsigned reloced : 1; unsigned size : 27; @@ -135,9 +135,9 @@ class Clause { // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). template - Clause(const V& ps, bool use_extra, bool learnt, int level) { + Clause(const V& ps, bool use_extra, bool removable, int level) { header.mark = 0; - header.learnt = learnt; + header.removable = removable; header.has_extra = use_extra; header.reloced = 0; header.size = ps.size(); @@ -147,7 +147,7 @@ class Clause { data[i].lit = ps[i]; if (header.has_extra){ - if (header.learnt) + if (header.removable) data[header.size].act = 0; else calcAbstraction(); } @@ -166,7 +166,7 @@ public: int size () const { return header.size; } void shrink (int i) { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; } void pop () { shrink(1); } - bool learnt () const { return header.learnt; } + bool removable () const { return header.removable; } bool has_extra () const { return header.has_extra; } uint32_t mark () const { return header.mark; } void mark (uint32_t m) { header.mark = m; } @@ -211,14 +211,14 @@ class ClauseAllocator : public RegionAllocator RegionAllocator::moveTo(to); } template - CRef alloc(int level, const Lits& ps, bool learnt = false) + CRef alloc(int level, const Lits& ps, bool removable = false) { assert(sizeof(Lit) == sizeof(uint32_t)); assert(sizeof(float) == sizeof(uint32_t)); - bool use_extra = learnt | extra_clause_field; + bool use_extra = removable | extra_clause_field; CRef cid = RegionAllocator::alloc(clauseWord32Size(ps.size(), use_extra)); - new (lea(cid)) Clause(ps, use_extra, learnt, level); + new (lea(cid)) Clause(ps, use_extra, removable, level); return cid; } @@ -244,13 +244,13 @@ class ClauseAllocator : public RegionAllocator if (c.reloced()) { cr = c.relocation(); return; } - cr = to.alloc(c.level(), c, c.learnt()); + cr = to.alloc(c.level(), c, c.removable()); c.relocate(cr); // Copy extra data-fields: // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?) to[cr].mark(c.mark()); - if (to[cr].learnt()) to[cr].activity() = c.activity(); + if (to[cr].removable()) to[cr].activity() = c.activity(); else if (to[cr].has_extra()) to[cr].calcAbstraction(); } }; @@ -380,7 +380,7 @@ inline Lit Clause::subsumes(const Clause& other) const //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0) //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0)) - assert(!header.learnt); assert(!other.header.learnt); + assert(!header.removable); assert(!other.header.removable); assert(header.has_extra); assert(other.header.has_extra); if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0) return lit_Error; diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 8bcd9fe76..271aabb52 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -134,23 +134,23 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) -bool SimpSolver::addClause_(vec& ps, ClauseType type) +bool SimpSolver::addClause_(vec& ps, bool removable) { #ifndef NDEBUG for (int i = 0; i < ps.size(); i++) assert(!isEliminated(var(ps[i]))); #endif - int nclauses = clauses.size(); + int nclauses = clauses_persistent.size(); if (use_rcheck && implied(ps)) return true; - if (!Solver::addClause_(ps, type)) + if (!Solver::addClause_(ps, removable)) return false; - if (use_simplification && clauses.size() == nclauses + 1){ - CRef cr = clauses.last(); + if (use_simplification && clauses_persistent.size() == nclauses + 1){ + CRef cr = clauses_persistent.last(); const Clause& c = ca[cr]; // NOTE: the clause is added to the queue immediately and then @@ -516,9 +516,12 @@ bool SimpSolver::eliminateVar(Var v) // Produce clauses in cross product: vec& resolvent = add_tmp; for (int i = 0; i < pos.size(); i++) - for (int j = 0; j < neg.size(); j++) - if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, CLAUSE_CONFLICT)) + for (int j = 0; j < neg.size(); j++) { + bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable(); + if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable)) { return false; + } + } // Free occurs list for this variable: occurs[v].clear(true); @@ -555,8 +558,9 @@ bool SimpSolver::substitute(Var v, Lit x) removeClause(cls[i]); - if (!addClause_(subst_clause, CLAUSE_PROBLEM)) + if (!addClause_(subst_clause, c.removable())) { return ok = false; + } } return true; @@ -669,10 +673,10 @@ void SimpSolver::cleanUpClauses() { occurs.cleanAll(); int i,j; - for (i = j = 0; i < clauses.size(); i++) - if (ca[clauses[i]].mark() == 0) - clauses[j++] = clauses[i]; - clauses.shrink(i - j); + for (i = j = 0; i < clauses_persistent.size(); i++) + if (ca[clauses_persistent[i]].mark() == 0) + clauses_persistent[j++] = clauses_persistent[i]; + clauses_persistent.shrink(i - j); } diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index a7359e28e..9b5e5d45c 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -47,12 +47,12 @@ class SimpSolver : public Solver { // Problem specification: // Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); - bool addClause (const vec& ps, ClauseType type); - bool addEmptyClause(ClauseType type); // Add the empty clause to the solver. - bool addClause (Lit p, ClauseType type); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, ClauseType type); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, ClauseType type); // Add a ternary clause to the solver. - bool addClause_(vec& ps, ClauseType type); + bool addClause (const vec& ps, bool removable); + bool addEmptyClause(bool removable); // Add the empty clause to the solver. + bool addClause (Lit p, bool removable); // Add a unit clause to the solver. + bool addClause (Lit p, Lit q, bool removable); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver. + bool addClause_(vec& ps, bool removable); bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). // Variable mode: @@ -181,11 +181,11 @@ inline void SimpSolver::updateElimHeap(Var v) { elim_heap.update(v); } -inline bool SimpSolver::addClause (const vec& ps, ClauseType type) { ps.copyTo(add_tmp); return addClause_(add_tmp, type); } -inline bool SimpSolver::addEmptyClause(ClauseType type) { add_tmp.clear(); return addClause_(add_tmp, type); } -inline bool SimpSolver::addClause (Lit p, ClauseType type) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, type); } -inline bool SimpSolver::addClause (Lit p, Lit q, ClauseType type) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, type); } -inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, ClauseType type) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, type); } +inline bool SimpSolver::addClause (const vec& ps, bool removable) { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); } +inline bool SimpSolver::addEmptyClause(bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable); } +inline bool SimpSolver::addClause (Lit p, bool removable) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); } +inline bool SimpSolver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); } +inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); } inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 3aa014782..046e4ef7e 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -86,7 +86,7 @@ void PropEngine::assertFormula(TNode node) { d_cnfStream->convertAndAssert(d_theoryEngine->preprocess(node), false, false); } -void PropEngine::assertLemma(TNode node) { +void PropEngine::assertLemma(TNode node, bool negated, bool removable) { //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; @@ -102,7 +102,7 @@ void PropEngine::assertLemma(TNode node) { //TODO This comment is now false // Assert as removable - d_cnfStream->convertAndAssert(node, true, false); + d_cnfStream->convertAndAssert(node, removable, negated); } void PropEngine::printSatisfyingAssignment(){ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index f6e66bef1..599439987 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -99,7 +99,7 @@ public: * * @param node the formula to assert */ - void assertLemma(TNode node); + void assertLemma(TNode node, bool negated, bool removable); /** * Checks the current context for satisfiability. diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index f34699e2b..62558cac1 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -27,33 +27,8 @@ namespace CVC4 { namespace prop { -void SatSolver::theoryCheck(theory::Theory::Effort effort, SatClause& conflict) { - Assert(conflict.size() == 0); - // Try theory propagation - bool ok = d_theoryEngine->check(effort); - // If in conflict construct the conflict clause - if (!ok) { - // We have a conflict, get it - Node conflictNode = d_theoryEngine->getConflict(); - Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl; - if(conflictNode.getKind() == kind::AND) { - // Go through the literals and construct the conflict clause - Node::const_iterator literal_it = conflictNode.begin(); - Node::const_iterator literal_end = conflictNode.end(); - while (literal_it != literal_end) { - // Get the literal corresponding to the node - SatLiteral l = d_cnfStream->getLiteral(*literal_it); - // Add the negation to the conflict clause and continue - conflict.push(~l); - literal_it ++; - } - } else { // unit conflict - // Get the literal corresponding to the node - SatLiteral l = d_cnfStream->getLiteral(conflictNode); - // construct the unit conflict clause - conflict.push(~l); - } - } +void SatSolver::theoryCheck(theory::Theory::Effort effort) { + d_theoryEngine->check(effort); } void SatSolver::theoryPropagate(std::vector& output) { diff --git a/src/prop/sat.h b/src/prop/sat.h index c00115cd8..2521f3ee7 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -101,7 +101,7 @@ public: /** Virtual destructor to make g++ happy */ virtual ~SatInputInterface() { } /** Assert a clause in the solver. */ - virtual void addClause(SatClause& clause, bool lemma) = 0; + virtual void addClause(SatClause& clause, bool removable) = 0; /** Create a new boolean variable in the solver. */ virtual SatVariable newVar(bool theoryAtom = false) = 0; /** Get the current decision level of the solver */ @@ -212,11 +212,11 @@ public: bool solve(); - void addClause(SatClause& clause, bool lemma); + void addClause(SatClause& clause, bool removable); SatVariable newVar(bool theoryAtom = false); - void theoryCheck(theory::Theory::Effort effort, SatClause& conflict); + void theoryCheck(theory::Theory::Effort effort); void explainPropagation(SatLiteral l, SatClause& explanation); @@ -290,8 +290,8 @@ inline bool SatSolver::solve() { return d_minisat->solve(); } -inline void SatSolver::addClause(SatClause& clause, bool lemma) { - d_minisat->addClause(clause, lemma ? Minisat::Solver::CLAUSE_LEMMA : Minisat::Solver::CLAUSE_PROBLEM); +inline void SatSolver::addClause(SatClause& clause, bool removable) { + d_minisat->addClause(clause, removable); } inline SatVariable SatSolver::newVar(bool theoryAtom) { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 28d7ab2c0..b1b4d67dd 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -235,8 +235,8 @@ void TheoryEngine::preRegister(TNode preprocessed) { * Check all (currently-active) theories for conflicts. * @param effort the effort level to use */ -bool TheoryEngine::check(theory::Theory::Effort effort) { - d_theoryOut.d_conflictNode = Node::null(); +void TheoryEngine::check(theory::Theory::Effort effort) { + d_theoryOut.d_propagatedLiterals.clear(); #ifdef CVC4_FOR_EACH_THEORY_STATEMENT @@ -245,8 +245,8 @@ bool TheoryEngine::check(theory::Theory::Effort effort) { #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::hasCheck && d_theoryIsActive[THEORY]) { \ reinterpret_cast::theory_class*>(d_theoryTable[THEORY])->check(effort); \ - if (!d_theoryOut.d_conflictNode.get().isNull()) { \ - return false; \ + if (d_theoryOut.d_inConflict) { \ + return; \ } \ } @@ -256,8 +256,6 @@ bool TheoryEngine::check(theory::Theory::Effort effort) { } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::check() => conflict" << std::endl; } - - return true; } void TheoryEngine::propagate() { @@ -296,7 +294,6 @@ bool TheoryEngine::presolve() { // at doing something with the input formula, even if it wouldn't // otherwise be active. - d_theoryOut.d_conflictNode = Node::null(); d_theoryOut.d_propagatedLiterals.clear(); try { @@ -307,7 +304,7 @@ bool TheoryEngine::presolve() { #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::hasPresolve) { \ reinterpret_cast::theory_class*>(d_theoryTable[THEORY])->presolve(); \ - if(!d_theoryOut.d_conflictNode.get().isNull()) { \ + if(d_theoryOut.d_inConflict) { \ return true; \ } \ } @@ -318,7 +315,7 @@ bool TheoryEngine::presolve() { Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl; } // return whether we have a conflict - return !d_theoryOut.d_conflictNode.get().isNull(); + return false; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 3507723f9..1e5653564 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -98,7 +98,7 @@ class TheoryEngine { TheoryEngine* d_engine; context::Context* d_context; - context::CDO d_conflictNode; + context::CDO d_inConflict; context::CDO d_explanationNode; /** @@ -113,12 +113,29 @@ class TheoryEngine { d_newFactTimer, "theory::newFactTimer"); + /** + * Check if the node is in conflict for debug purposes + */ + bool isProperConflict(TNode conflictNode) { + bool value; + if (conflictNode.getKind() == kind::AND) { + for (unsigned i = 0; i < conflictNode.getNumChildren(); ++ i) { + if (!d_engine->getPropEngine()->hasValue(conflictNode[i], value)) return false; + if (!value) return false; + } + } else { + if (!d_engine->getPropEngine()->hasValue(conflictNode, value)) return false; + return value; + } + return true; + } + public: EngineOutputChannel(TheoryEngine* engine, context::Context* context) : d_engine(engine), d_context(context), - d_conflictNode(context), + d_inConflict(context, false), d_explanationNode(context) { } @@ -126,10 +143,15 @@ class TheoryEngine { void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) { - Trace("theory") << "EngineOutputChannel::conflict(" - << conflictNode << ")" << std::endl; - d_conflictNode = conflictNode; + Trace("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl; + d_inConflict = true; + ++(d_engine->d_statistics.d_statConflicts); + + // Construct the lemma (note that no CNF caching should happen as all the literals already exists) + Assert(isProperConflict(conflictNode)); + d_engine->newLemma(conflictNode, true, true); + if(safe) { throw theory::Interrupted(); } @@ -143,12 +165,13 @@ class TheoryEngine { ++(d_engine->d_statistics.d_statPropagate); } - void lemma(TNode node, bool) + void lemma(TNode node, bool removable = false) throw(theory::Interrupted, AssertionException) { Trace("theory") << "EngineOutputChannel::lemma(" << node << ")" << std::endl; ++(d_engine->d_statistics.d_statLemma); - d_engine->newLemma(node); + + d_engine->newLemma(node, false, removable); } void explanation(TNode explanationNode, bool) @@ -387,7 +410,7 @@ public: * Check all (currently-active) theories for conflicts. * @param effort the effort level to use */ - bool check(theory::Theory::Effort effort); + void check(theory::Theory::Effort effort); /** * Calls staticLearning() on all theories, accumulating their @@ -414,23 +437,17 @@ public: d_theoryOut.d_propagatedLiterals.clear(); } - inline void newLemma(TNode node) { + inline void newLemma(TNode node, bool negated, bool removable) { // Remove the ITEs and assert to prop engine std::vector additionalLemmas; additionalLemmas.push_back(node); RemoveITE::run(additionalLemmas); - for (unsigned i = 0; i < additionalLemmas.size(); ++ i) { - d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[i])); + d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[0]), negated, removable); + for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { + d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[i]), false, removable); } } - /** - * Returns the last conflict (if any). - */ - inline Node getConflict() { - return d_theoryOut.d_conflictNode; - } - void propagate(); inline Node getExplanation(TNode node, theory::Theory* theory) { diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index f6118d85c..0a49e6a3e 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -140,7 +140,7 @@ void testAnd() { Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::AND, a, b, c), false); + d_nodeManager->mkNode(kind::AND, a, b, c), false, false); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -161,13 +161,13 @@ void testComplexExpr() { d_nodeManager->mkNode(kind::OR, c, d), d_nodeManager->mkNode( kind::NOT, - d_nodeManager->mkNode(kind::XOR, e, f)))), false ); + d_nodeManager->mkNode(kind::XOR, e, f)))), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } void testFalse() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -176,7 +176,7 @@ void testIff() { Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::IFF, a, b), false ); + d_nodeManager->mkNode(kind::IFF, a, b), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -185,7 +185,7 @@ void testImplies() { Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::IMPLIES, a, b), false ); + d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -201,7 +201,7 @@ void testIte() { d_nodeManager->mkVar(d_nodeManager->integerType()) ), d_nodeManager->mkVar(d_nodeManager->integerType()) - ), false); + ), false, false); } @@ -209,7 +209,7 @@ void testNot() { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::NOT, a), false ); + d_nodeManager->mkNode(kind::NOT, a), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -219,13 +219,13 @@ void testOr() { Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::OR, a, b, c), false ); + d_nodeManager->mkNode(kind::OR, a, b, c), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } void testTrue() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -233,10 +233,10 @@ void testVar() { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(a, false); + d_cnfStream->convertAndAssert(a, false, false); TS_ASSERT( d_satSolver->addClauseCalled() ); d_satSolver->reset(); - d_cnfStream->convertAndAssert(b, false); + d_cnfStream->convertAndAssert(b, false, false); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -245,7 +245,7 @@ void testXor() { Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::XOR, a, b), false ); + d_nodeManager->mkNode(kind::XOR, a, b), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } };