From e87c14798b99ccb586751d291b0eeb3208265bd8 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Tue, 25 May 2010 05:30:40 +0000 Subject: [PATCH] Some initial changes to allow for lemmas on demand. To be done: * Add erasable map Clause* to bool to minisat (backtracks with the solver) * Add map from Clause* to Node (clauses that came from a node) * Add reference counting Literal -> Node to CNFManager * If Literal -> Node refcount goes to zero, the clauses of Node can be erased (if eresable) * If clause is erased for each L in clause L -> Node refcount goes down --- src/prop/cnf_stream.cpp | 75 +++++++++++++++--------------- src/prop/cnf_stream.h | 22 ++++++--- src/prop/minisat/core/Solver.C | 11 ++++- src/prop/minisat/core/Solver.h | 18 ++++++- src/prop/minisat/simp/SimpSolver.C | 8 ++-- src/prop/minisat/simp/SimpSolver.h | 2 +- src/prop/prop_engine.cpp | 26 ++++++++++- src/prop/prop_engine.h | 8 +++- src/prop/sat.cpp | 4 +- src/prop/sat.h | 8 ++-- src/smt/smt_engine.cpp | 7 ++- src/theory/arith/theory_arith.cpp | 4 +- src/theory/theory_engine.h | 29 ++++++++---- 13 files changed, 151 insertions(+), 71 deletions(-) diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 31afa986c..51ae695cf 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -37,30 +37,30 @@ TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver) : CnfStream(satSolver) { } -void CnfStream::assertClause(SatClause& c) { +void CnfStream::assertClause(TNode node, SatClause& c) { Debug("cnf") << "Inserting into stream " << c << endl; - d_satSolver->addClause(c); + d_satSolver->addClause(c, d_assertingLemma); } -void CnfStream::assertClause(SatLiteral a) { +void CnfStream::assertClause(TNode node, SatLiteral a) { SatClause clause(1); clause[0] = a; - assertClause(clause); + assertClause(node, clause); } -void CnfStream::assertClause(SatLiteral a, SatLiteral b) { +void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) { SatClause clause(2); clause[0] = a; clause[1] = b; - assertClause(clause); + assertClause(node, clause); } -void CnfStream::assertClause(SatLiteral a, SatLiteral b, SatLiteral c) { +void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c) { SatClause clause(3); clause[0] = a; clause[1] = b; clause[2] = c; - assertClause(clause); + assertClause(node, clause); } bool CnfStream::isCached(TNode n) const { @@ -74,7 +74,7 @@ SatLiteral CnfStream::lookupInCache(TNode n) const { void CnfStream::cacheTranslation(TNode node, SatLiteral lit) { Debug("cnf") << "caching translation " << node << " to " << lit << endl; - // We always cash bot the node and the negation at the same time + // We always cash both the node and the negation at the same time d_translationCache[node] = lit; d_translationCache[node.notNode()] = ~lit; } @@ -125,9 +125,9 @@ SatLiteral TseitinCnfStream::handleAtom(TNode node) { if(node.getKind() == kind::CONST_BOOLEAN) { if(node.getConst()) { - assertClause(lit); + assertClause(node, lit); } else { - assertClause(~lit); + assertClause(node, ~lit); } } @@ -144,10 +144,10 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { SatLiteral xorLit = newLiteral(xorNode); - assertClause(a, b, ~xorLit); - assertClause(~a, ~b, ~xorLit); - assertClause(a, ~b, xorLit); - assertClause(~a, b, xorLit); + assertClause(xorNode, a, b, ~xorLit); + assertClause(xorNode, ~a, ~b, ~xorLit); + assertClause(xorNode, a, ~b, xorLit); + assertClause(xorNode, ~a, b, xorLit); return xorLit; } @@ -175,14 +175,14 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) { // lit | ~(a_1 | a_2 | a_3 | ... | a_n) // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n) for(unsigned i = 0; i < n_children; ++i) { - assertClause(orLit, ~clause[i]); + assertClause(orNode, orLit, ~clause[i]); } // lit -> (a_1 | a_2 | a_3 | ... | a_n) // ~lit | a_1 | a_2 | a_3 | ... | a_n clause[n_children] = ~orLit; // This needs to go last, as the clause might get modified by the SAT solver - assertClause(clause); + assertClause(orNode, clause); // Return the literal return orLit; @@ -211,7 +211,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { // ~lit | (a_1 & a_2 & a_3 & ... & a_n) // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n) for(unsigned i = 0; i < n_children; ++i) { - assertClause(~andLit, ~clause[i]); + assertClause(andNode, ~andLit, ~clause[i]); } // lit <- (a_1 & a_2 & a_3 & ... a_n) @@ -219,7 +219,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n clause[n_children] = andLit; // This needs to go last, as the clause might get modified by the SAT solver - assertClause(clause); + assertClause(andNode, clause); return andLit; } @@ -236,13 +236,13 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { // lit -> (a->b) // ~lit | ~ a | b - assertClause(~impliesLit, ~a, b); + assertClause(impliesNode, ~impliesLit, ~a, b); // (a->b) -> lit // ~(~a | b) | lit // (a | l) & (~b | l) - assertClause(a, impliesLit); - assertClause(~b, impliesLit); + assertClause(impliesNode, a, impliesLit); + assertClause(impliesNode, ~b, impliesLit); return impliesLit; } @@ -263,16 +263,16 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { // lit -> ((a-> b) & (b->a)) // ~lit | ((~a | b) & (~b | a)) // (~a | b | ~lit) & (~b | a | ~lit) - assertClause(~a, b, ~iffLit); - assertClause(a, ~b, ~iffLit); + assertClause(iffNode, ~a, b, ~iffLit); + assertClause(iffNode, a, ~b, ~iffLit); // (a<->b) -> lit // ~((a & b) | (~a & ~b)) | lit // (~(a & b)) & (~(~a & ~b)) | lit // ((~a | ~b) & (a | b)) | lit // (~a | ~b | lit) & (a | b | lit) - assertClause(~a, ~b, iffLit); - assertClause(a, b, iffLit); + assertClause(iffNode, ~a, ~b, iffLit); + assertClause(iffNode, a, b, iffLit); return iffLit; } @@ -309,9 +309,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { // lit -> (t | e) & (b -> t) & (!b -> e) // lit -> (t | e) & (!b | t) & (b | e) // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e) - assertClause(~iteLit, thenLit, elseLit); - assertClause(~iteLit, ~condLit, thenLit); - assertClause(~iteLit, condLit, elseLit); + assertClause(iteNode, ~iteLit, thenLit, elseLit); + assertClause(iteNode, ~iteLit, ~condLit, thenLit); + assertClause(iteNode, ~iteLit, condLit, elseLit); // If ITE is false then one of the branches is false and the condition // implies which one @@ -319,9 +319,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { // !lit -> (!t | !e) & (b -> !t) & (!b -> !e) // !lit -> (!t | !e) & (!b | !t) & (b | !e) // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e) - assertClause(iteLit, ~thenLit, ~elseLit); - assertClause(iteLit, ~condLit, ~thenLit); - assertClause(iteLit, condLit, ~elseLit); + assertClause(iteNode, iteLit, ~thenLit, ~elseLit); + assertClause(iteNode, iteLit, ~condLit, ~thenLit); + assertClause(iteNode, iteLit, condLit, ~elseLit); return iteLit; } @@ -347,7 +347,7 @@ Node TseitinCnfStream::handleNonAtomicNode(TNode node) { nodeManager->mkNode(EQUAL, skolem, node[1]), nodeManager->mkNode(EQUAL, skolem, node[2])); nodeManager->setAttribute(node, IteRewriteAttr(), skolem); - convertAndAssert( newAssertion ); + convertAndAssert(newAssertion, d_assertingLemma); return skolem; } else { std::vector newChildren; @@ -403,15 +403,16 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) { } } -void TseitinCnfStream::convertAndAssert(TNode node) { +void TseitinCnfStream::convertAndAssert(TNode node, bool lemma) { Debug("cnf") << "convertAndAssert(" << node << ")" << endl; + d_assertingLemma = lemma; if(node.getKind() == AND) { // 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); + convertAndAssert(*conjunct, lemma); } } else if(node.getKind() == OR) { // If the node is a disjunction, we construct a clause and assert it @@ -423,10 +424,10 @@ void TseitinCnfStream::convertAndAssert(TNode node) { clause[i] = toCNF(*disjunct); } Assert( disjunct == node.end() ); - assertClause(clause); + assertClause(node, clause); } else { // Otherwise, we just convert using the definitional transformation - assertClause(toCNF(node)); + assertClause(node, toCNF(node)); } } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 7546a8880..1ea600322 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -39,7 +39,9 @@ class PropEngine; * @author Tim King */ class CnfStream { + public: + /** Cache of what nodes have been registered to a literal. */ typedef __gnu_cxx::hash_map NodeCache; @@ -56,24 +58,31 @@ private: protected: + /** + * Are we asserting a lemma (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; + /** * Asserts the given clause to the sat solver. * @param clause the clasue to assert */ - void assertClause(SatClause& clause); + void assertClause(TNode node, SatClause& clause); /** * Asserts the unit clause to the sat solver. * @param a the unit literal of the clause */ - void assertClause(SatLiteral a); + void assertClause(TNode node, SatLiteral a); /** * Asserts the binary clause to the sat solver. * @param a the first literal in the clause * @param b the second literal in the clause */ - void assertClause(SatLiteral a, SatLiteral b); + void assertClause(TNode node, SatLiteral a, SatLiteral b); /** * Asserts the ternary clause to the sat solver. @@ -81,7 +90,7 @@ protected: * @param b the second literal in the clause * @param c the thirs literal in the clause */ - void assertClause(SatLiteral a, SatLiteral b, SatLiteral c); + void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c); /** * Returns true if the node has been cashed in the translation cache. @@ -137,7 +146,7 @@ public: * @param node node to convert and assert * @param whether the sat solver can choose to remove this clause */ - virtual void convertAndAssert(TNode node) = 0; + virtual void convertAndAssert(TNode node, bool lemma = false) = 0; /** * Get the node that is represented by the given SatLiteral. @@ -175,8 +184,9 @@ 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 */ - void convertAndAssert(TNode node); + void convertAndAssert(TNode node, bool lemma); /** * Constructs the stream to use the given sat solver. diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C index a735cd46c..8533e191b 100644 --- a/src/prop/minisat/core/Solver.C +++ b/src/prop/minisat/core/Solver.C @@ -98,7 +98,7 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) } -bool Solver::addClause(vec& ps) +bool Solver::addClause(vec& ps, ClauseType type) { assert(decisionLevel() == 0); @@ -119,16 +119,19 @@ bool Solver::addClause(vec& ps) if (ps.size() == 0) return ok = false; else if (ps.size() == 1){ + assert(type != CLAUSE_LEMMA); assert(value(ps[0]) == l_Undef); uncheckedEnqueue(ps[0]); return ok = (propagate() == NULL); }else{ Clause* c = Clause_new(ps, false); clauses.push(c); + if (type == CLAUSE_LEMMA) lemmas.push(c); attachClause(*c); } return true; + } @@ -181,6 +184,12 @@ void Solver::cancelUntil(int level) { qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); + // We can erase the lemmas now + for (int c = lemmas.size() - 1; c >= lemmas_lim[level]; c--) { + // TODO: can_erase[lemma[c]] = true; + } + lemmas.shrink(lemmas.size() - lemmas_lim[level]); + lemmas_lim.shrink(lemmas_lim.size() - level); } } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index bf2018338..312fe44d5 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -66,7 +66,18 @@ public: // Problem specification: // Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode. - bool addClause (vec& ps); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! + + // Types of clauses + enum ClauseType { + // Clauses defined by the problem + CLAUSE_PROBLEM, + // Lemma clauses added by the theories + CLAUSE_LEMMA, + // Conflict clauses + CLAUSE_CONFLICT + }; + + bool addClause (vec& ps, ClauseType type); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! // Solving: // @@ -148,9 +159,12 @@ protected: vec decision_var; // 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 lemmas; // List of lemmas we added (context dependent) + vec lemmas_lim; // Separator indices for different decision levels in 'lemmas'. vec reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. vec level; // 'level[var]' contains the level at which the assignment was made. int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). + int lhead; // Head of the lemma stack (for backtracking) 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. @@ -256,7 +270,7 @@ inline void Solver::claBumpActivity (Clause& c) { inline bool Solver::enqueue (Lit p, Clause* from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); } inline bool Solver::locked (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; } -inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); context->push(); } +inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); lemmas_lim.push(lemmas.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); } diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C index 057dfdbe2..9aad6aea7 100644 --- a/src/prop/minisat/simp/SimpSolver.C +++ b/src/prop/minisat/simp/SimpSolver.C @@ -118,7 +118,7 @@ bool SimpSolver::solve(const vec& assumps, bool do_simp, bool turn_off_simp -bool SimpSolver::addClause(vec& ps) +bool SimpSolver::addClause(vec& ps, ClauseType type) { for (int i = 0; i < ps.size(); i++) if (isEliminated(var(ps[i]))) @@ -129,7 +129,7 @@ bool SimpSolver::addClause(vec& ps) if (redundancy_check && implied(ps)) return true; - if (!Solver::addClause(ps)) + if (!Solver::addClause(ps, type)) return false; if (use_simplification && clauses.size() == nclauses + 1){ @@ -485,7 +485,7 @@ bool SimpSolver::eliminateVar(Var v, bool fail) vec resolvent; for (int i = 0; i < pos.size(); i++) for (int j = 0; j < neg.size(); j++) - if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent)) + if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent, CLAUSE_CONFLICT)) return false; // DEBUG: For checking that a clause set is saturated with respect to variable elimination. @@ -527,7 +527,7 @@ void SimpSolver::remember(Var v) clause.push(c[j]); remembered_clauses++; - check(addClause(clause)); + check(addClause(clause, CLAUSE_PROBLEM)); free(&c); } diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 38d51206d..3da574f6c 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -45,7 +45,7 @@ class SimpSolver : public Solver { // Problem specification: // Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); - bool addClause (vec& ps); + bool addClause (vec& ps, ClauseType type); // Variable mode: // diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index ec0e2dfbc..b9fbd3ce6 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -33,6 +33,26 @@ using namespace CVC4::context; namespace CVC4 { namespace prop { +/** Keeps a boolean flag scoped */ +class ScopedBool { + +private: + + bool d_original; + bool& d_reference; + +public: + + ScopedBool(bool& reference) : + d_reference(reference) { + d_original = reference; + } + + ~ScopedBool() { + d_reference = d_original; + } +}; + PropEngine::PropEngine(const Options* opts, DecisionEngine* de, TheoryEngine* te, Context* context) : d_inCheckSat(false), @@ -61,6 +81,7 @@ void PropEngine::assertFormula(TNode node) { } void PropEngine::assertLemma(TNode node) { + Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as removable d_cnfStream->convertAndAssert(node); @@ -89,12 +110,13 @@ void PropEngine::printSatisfyingAssignment(){ Result PropEngine::checkSat() { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "PropEngine::checkSat()" << endl; + // Mark that we are in the checkSat + ScopedBool scopedBool(d_inCheckSat); d_inCheckSat = true; + // Check the problem bool result = d_satSolver->solve(); - // Not in checkSat any more - d_inCheckSat = false; if( result && debugTagIsOn("prop") ) { printSatisfyingAssignment(); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 4d25e9bc0..7d3656a32 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -23,9 +23,11 @@ #include "util/result.h" #include "util/options.h" #include "util/decision_engine.h" -#include "theory/theory_engine.h" namespace CVC4 { + +class TheoryEngine; + namespace prop { class CnfStream; @@ -96,7 +98,9 @@ public: /** * Converts the given formula to CNF and assert the CNF to the sat solver. - * The formula can be removed by the sat solver. + * The formula can be removed by the sat solver after backtracking lower + * than the (SAT and SMT) level at which it was asserted. + * * @param node the formula to assert */ void assertLemma(TNode node); diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 46d2182a9..df6eead4c 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -9,7 +9,9 @@ namespace prop { void SatSolver::theoryCheck(SatClause& conflict) { // Try theory propagation - if (!d_theoryEngine->check(theory::Theory::FULL_EFFORT)) { + bool ok = d_theoryEngine->check(theory::Theory::FULL_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; diff --git a/src/prop/sat.h b/src/prop/sat.h index 42f454820..f9d27d2ac 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -93,7 +93,7 @@ inline std::string stringOfLiteralValue(SatLiteralValue val) { class SatInputInterface { public: /** Assert a clause in the solver. */ - virtual void addClause(SatClause& clause) = 0; + virtual void addClause(SatClause& clause, bool lemma) = 0; /** Create a new boolean variable in the solver. */ virtual SatVariable newVar(bool theoryAtom = false) = 0; }; @@ -148,7 +148,7 @@ public: bool solve(); - void addClause(SatClause& clause); + void addClause(SatClause& clause, bool lemma); SatVariable newVar(bool theoryAtom = false); @@ -190,8 +190,8 @@ inline bool SatSolver::solve() { return d_minisat->solve(); } -inline void SatSolver::addClause(SatClause& clause) { - d_minisat->addClause(clause); +inline void SatSolver::addClause(SatClause& clause, bool lemma) { + d_minisat->addClause(clause, lemma ? minisat::Solver::CLAUSE_LEMMA : minisat::Solver::CLAUSE_PROBLEM); } inline SatVariable SatSolver::newVar(bool theoryAtom) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a55c146b8..3b003846c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -20,6 +20,8 @@ #include "util/exception.h" #include "util/options.h" #include "prop/prop_engine.h" +#include "theory/theory_engine.h" + using namespace CVC4::prop; using CVC4::context::Context; @@ -72,8 +74,11 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : NodeManagerScope nms(d_nodeManager); d_decisionEngine = new DecisionEngine; - d_theoryEngine = new TheoryEngine(this, d_ctxt); + // We have mutual dependancy here, so we add the prop engine to the theory + // engine later (it is non-essential there) + d_theoryEngine = new TheoryEngine(d_ctxt); d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine, d_ctxt); + d_theoryEngine->setPropEngine(d_propEngine); } void SmtEngine::shutdown() { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6ca447ea5..bdc32ab21 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -130,8 +130,8 @@ void TheoryArith::registerTerm(TNode tn){ Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left); slackEqLeft.setAttribute(TheoryArithPropagated(), true); - //TODO this has to be wrong no? - d_out->lemma(slackEqLeft); + //TODO this has to be wrong no? YES (dejan) + // d_out->lemma(slackEqLeft); d_tableau.addRow(slackEqLeft); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index c8b93e8b4..e85e66e99 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -22,6 +22,7 @@ #include "theory/theory.h" #include "theory/theoryof_table.h" +#include "prop/prop_engine.h" #include "theory/booleans/theory_bool.h" #include "theory/uf/theory_uf.h" #include "theory/arith/theory_arith.h" @@ -30,8 +31,6 @@ namespace CVC4 { -class SmtEngine; - // In terms of abstraction, this is below (and provides services to) // PropEngine. @@ -43,8 +42,8 @@ class SmtEngine; */ class TheoryEngine { - /** Associated SMT engine */ - SmtEngine* d_smt; + /** Associated PropEngine engine */ + prop::PropEngine* d_propEngine; /** A table of Kinds to pointers to Theory */ theory::TheoryOfTable d_theoryOfTable; @@ -80,7 +79,8 @@ class TheoryEngine { void propagate(TNode, bool) throw(theory::Interrupted) { } - void lemma(TNode, bool) throw(theory::Interrupted) { + void lemma(TNode node, bool) throw(theory::Interrupted) { + d_engine->newLemma(node); } void explanation(TNode, bool) throw(theory::Interrupted) { @@ -171,8 +171,8 @@ public: /** * Construct a theory engine. */ - TheoryEngine(SmtEngine* smt, context::Context* ctxt) : - d_smt(smt), + TheoryEngine(context::Context* ctxt) : + d_propEngine(NULL), d_theoryOut(this, ctxt), d_bool(ctxt, d_theoryOut), d_uf(ctxt, d_theoryOut), @@ -187,6 +187,12 @@ public: d_theoryOfTable.registerTheory(&d_bv); } + void setPropEngine(prop::PropEngine* propEngine) + { + Assert(d_propEngine == NULL); + d_propEngine = propEngine; + } + /** * This is called at shutdown time by the SmtEngine, just before * destruction. It is important because there are destruction @@ -263,8 +269,10 @@ public: * Check all (currently-active) theories for conflicts. * @param effort the effort level to use */ - inline bool check(theory::Theory::Effort effort) { + inline bool check(theory::Theory::Effort effort) + { d_theoryOut.d_conflictNode = Node::null(); + // Do the checking try { //d_bool.check(effort); d_uf.check(effort); @@ -274,9 +282,14 @@ public: } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::check() => conflict" << std::endl; } + // Return wheather we have a conflict return d_theoryOut.d_conflictNode.get().isNull(); } + inline void newLemma(TNode node) { + d_propEngine->assertLemma(node); + } + /** * Returns the last conflict (if any). */ -- 2.30.2