diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-11-09 21:57:06 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-11-09 21:57:06 +0000 |
commit | df5f7fe03fda041429548bcb39abb8916ca2e291 (patch) | |
tree | 46b08f3e35ee9c3d4c551d82f3e7e36582383f39 /src | |
parent | 1f07775e9205b3f9e172a1ad218a9015b7265b58 (diff) |
Lemmas on demand work, push-pop, some cleanup.
Diffstat (limited to 'src')
27 files changed, 731 insertions, 307 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index da41b1de4..0c692501f 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -37,6 +37,14 @@ CnfStream::CnfStream(SatInputInterface *satSolver) : d_satSolver(satSolver) { } +void CnfStream::recordTranslation(TNode node) { + if (d_assertingLemma) { + d_lemmas.push_back(stripNot(node)); + } else { + d_translationTrail.push_back(stripNot(node)); + } +} + TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver) : CnfStream(satSolver) { } @@ -67,42 +75,61 @@ void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral assertClause(node, clause); } -bool CnfStream::isCached(TNode n) const { - return d_translationCache.find(n) != d_translationCache.end(); +bool CnfStream::isTranslated(TNode n) const { + TranslationCache::const_iterator find = d_translationCache.find(n); + return find != d_translationCache.end() && find->second.level >= 0; } -SatLiteral CnfStream::lookupInCache(TNode node) const { - Assert(isCached(node), "Node is not in CNF translation cache"); - return d_translationCache.find(node)->second; -} - -void CnfStream::cacheTranslation(TNode node, SatLiteral lit) { - Debug("cnf") << "caching translation " << node << " to " << lit << endl; - // We always cash both the node and the negation at the same time - d_translationCache[node] = lit; - d_translationCache[node.notNode()] = ~lit; +bool CnfStream::hasLiteral(TNode n) const { + TranslationCache::const_iterator find = d_translationCache.find(n); + return find != d_translationCache.end(); } SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { - SatLiteral lit = Minisat::mkLit(d_satSolver->newVar(theoryLiteral)); - cacheTranslation(node, lit); + Debug("cnf") << "newLiteral(" << node << ")" << endl; + + // Get the literal for this node + SatLiteral lit; + if (!hasLiteral(node)) { + // If no literal, well make one + lit = Minisat::mkLit(d_satSolver->newVar(theoryLiteral)); + d_translationCache[node].literal = lit; + d_translationCache[node.notNode()].literal = ~lit; + } else { + // We already have a literal + lit = getLiteral(node); + d_satSolver->renewVar(lit); + } + + // We will translate clauses, so remember the level + int level = d_satSolver->getLevel(); + d_translationCache[node].level = level; + d_translationCache[node.notNode()].level = level; + + // If it's a theory literal, store it for back queries if (theoryLiteral) { d_nodeCache[lit] = node; d_nodeCache[~lit] = node.notNode(); } + + // Here, you can have it + Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl; return lit; } -Node CnfStream::getNode(const SatLiteral& literal) { +TNode CnfStream::getNode(const SatLiteral& literal) { + Debug("cnf") << "getNode(" << literal << ")" << endl; NodeCache::iterator find = d_nodeCache.find(literal); Assert(find != d_nodeCache.end()); + Assert(d_translationCache.find(find->second) != d_translationCache.end()); + Debug("cnf") << "getNode(" << literal << ") => " << find->second << endl; return find->second; } SatLiteral CnfStream::convertAtom(TNode node) { Debug("cnf") << "convertAtom(" << node << ")" << endl; - Assert(!isCached(node), "atom already mapped!"); + Assert(!isTranslated(node), "atom already mapped!"); bool theoryLiteral = node.getKind() != kind::VARIABLE; SatLiteral lit = newLiteral(node, theoryLiteral); @@ -121,13 +148,13 @@ SatLiteral CnfStream::convertAtom(TNode node) { SatLiteral CnfStream::getLiteral(TNode node) { TranslationCache::iterator find = d_translationCache.find(node); Assert(find != d_translationCache.end(), "Literal not in the CNF Cache"); - SatLiteral literal = find->second; + SatLiteral literal = find->second.literal; Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; return literal; } SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { - Assert(!isCached(xorNode), "Atom already mapped!"); + Assert(!isTranslated(xorNode), "Atom already mapped!"); Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!"); Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!"); @@ -145,7 +172,7 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { } SatLiteral TseitinCnfStream::handleOr(TNode orNode) { - Assert(!isCached(orNode), "Atom already mapped!"); + Assert(!isTranslated(orNode), "Atom already mapped!"); Assert(orNode.getKind() == OR, "Expecting an OR expression!"); Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!"); @@ -181,7 +208,7 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) { } SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { - Assert(!isCached(andNode), "Atom already mapped!"); + Assert(!isTranslated(andNode), "Atom already mapped!"); Assert(andNode.getKind() == AND, "Expecting an AND expression!"); Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!"); @@ -216,7 +243,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { } SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { - Assert(!isCached(impliesNode), "Atom already mapped!"); + Assert(!isTranslated(impliesNode), "Atom already mapped!"); Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!"); Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!"); @@ -241,7 +268,7 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { - Assert(!isCached(iffNode), "Atom already mapped!"); + Assert(!isTranslated(iffNode), "Atom already mapped!"); Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!"); Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!"); @@ -273,15 +300,12 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { SatLiteral TseitinCnfStream::handleNot(TNode notNode) { - Assert(!isCached(notNode), "Atom already mapped!"); + Assert(!isTranslated(notNode), "Atom already mapped!"); Assert(notNode.getKind() == NOT, "Expecting a NOT expression!"); Assert(notNode.getNumChildren() == 1, "Expecting exactly 1 child!"); SatLiteral notLit = ~toCNF(notNode[0]); - // Since we don't introduce new variables, we need to cache the translation - cacheTranslation(notNode, notLit); - return notLit; } @@ -328,8 +352,12 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { Node negatedNode = node.notNode(); // If the non-negated node has already been translated, get the translation - if(isCached(node)) { - nodeLit = lookupInCache(node); + 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()) { @@ -395,6 +423,7 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated) for(int i = 0; i < nChildren; ++ disjunct, ++ i) { Assert( disjunct != node.end() ); clause[i] = toCNF(*disjunct, true); + recordTranslation(*disjunct); } Assert(disjunct == node.end()); assertClause(node, clause); @@ -411,6 +440,7 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool negated) for(int i = 0; i < nChildren; ++ disjunct, ++ i) { Assert( disjunct != node.end() ); clause[i] = toCNF(*disjunct, false); + recordTranslation(*disjunct); } Assert(disjunct == node.end()); assertClause(node, clause); @@ -451,6 +481,8 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated) clause2[1] = ~q; assertClause(node, clause2); } + recordTranslation(node[0]); + recordTranslation(node[1]); } void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated) { @@ -481,6 +513,8 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated) clause2[1] = q; assertClause(node, clause2); } + recordTranslation(node[0]); + recordTranslation(node[1]); } void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool negated) { @@ -493,6 +527,8 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool nega clause[0] = ~p; clause[1] = q; assertClause(node, clause); + recordTranslation(node[0]); + recordTranslation(node[1]); } else {// Construct the // !(p => q) is the same as (p && ~q) convertAndAssert(node[0], lemma, false); @@ -523,6 +559,10 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated) clause4[0] = r; clause4[1] = p; assertClause(node, clause4); + + recordTranslation(node[0]); + recordTranslation(node[1]); + recordTranslation(node[2]); } // At the top level we must ensure that all clauses that are asserted are @@ -556,9 +596,79 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool lemma, bool negated) { default: // Atoms assertClause(node, toCNF(node, negated)); + recordTranslation(node); break; } } +void CnfStream::removeClausesAboveLevel(int level) { + while (d_translationTrail.size() > 0) { + TNode node = d_translationTrail.back(); + Debug("cnf") << "Removing node " << node << " from CNF translation" << endl; + d_translationTrail.pop_back(); + // Get the translation informations + TranslationInfo& infoPos = d_translationCache.find(node)->second; + // If already untranslated, we're done + if (infoPos.level == -1) continue; + // If the level of the node is less or equal to given we are done + if (infoPos.level <= level) break; + // Otherwise we have to undo the translation + undoTranslate(node, level); + } +} + +void CnfStream::undoTranslate(TNode node, int level) { + // Get the translation information + TranslationInfo& infoPos = d_translationCache.find(node)->second; + // If already untranslated, we are done + if (infoPos.level == -1) return; + // If under the given level we're also done + if (infoPos.level <= level) return; + // Untranslate + infoPos.level = -1; + // Untranslate the negation node + // If not a not node, unregister it from sat and untranslate the negation + if (node.getKind() != kind::NOT) { + // Unregister the literal from SAT + SatLiteral lit = getLiteral(node); + d_satSolver->unregisterVar(lit); + // Untranslate the negation + TranslationInfo& infoNeg = d_translationCache.find(node.notNode())->second; + infoNeg.level = -1; + } + // undoTranslate the children + TNode::iterator child = node.begin(); + TNode::iterator child_end = node.end(); + while (child != child_end) { + undoTranslate(*child, level); + ++ child; + } +} + +void CnfStream::moveToBaseLevel(TNode node) { + TNode posNode = stripNot(node); + TranslationInfo& infoPos = d_translationCache.find(posNode)->second; + + Assert(infoPos.level >= 0); + if (infoPos.level == 0) return; + + TNode negNode = node.notNode(); + TranslationInfo& infoNeg = d_translationCache.find(negNode)->second; + + infoPos.level = 0; + infoNeg.level = 0; + + d_satSolver->renewVar(infoPos.literal, 0); + + // undoTranslate the children + TNode::iterator child = posNode.begin(); + TNode::iterator child_end = posNode.end(); + while (child != child_end) { + moveToBaseLevel(*child); + ++ child; + } + +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 96d1925de..b35f3eafe 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -47,10 +47,18 @@ class CnfStream { public: /** Cache of what nodes have been registered to a literal. */ - typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFunction> NodeCache; + typedef __gnu_cxx::hash_map<SatLiteral, TNode, SatSolver::SatLiteralHashFunction> NodeCache; + + /** Per node translation information */ + struct TranslationInfo { + /** The level at which this node was translated (negative if not translated) */ + int level; + /** The literal of this node */ + SatLiteral literal; + }; /** Cache of what literals have been registered to a node. */ - typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFunction> TranslationCache; + typedef __gnu_cxx::hash_map<Node, TranslationInfo, NodeHashFunction> TranslationCache; private: @@ -62,6 +70,33 @@ private: protected: + /** Top level nodes that we translated */ + std::vector<TNode> d_translationTrail; + + /** Nodes belonging to asserted lemmas */ + std::vector<Node> d_lemmas; + + /** Remove nots from the node */ + TNode stripNot(TNode node) { + while (node.getKind() == kind::NOT) { + node = node[0]; + } + return node; + } + + /** Record this translation */ + void recordTranslation(TNode node); + + /** + * Moves the node and all of it's parents to level 0. + */ + void moveToBaseLevel(TNode node); + + /** + * Mark the node, and all parent at levels above level as untranslated. + */ + void undoTranslate(TNode node, int level); + /** * Are we asserting a lemma (true) or a permanent clause (false). * This is set at the begining of convertAndAssert so that it doesn't @@ -105,22 +140,16 @@ protected: * @param node the node * @return true if the node has been cached */ - bool isCached(TNode node) const; - - /** - * Returns the cached literal corresponding to the given node. - * @param node the node to lookup - * @return returns the corresponding literal - */ - SatLiteral lookupInCache(TNode node) const; + bool isTranslated(TNode node) const; /** + * Returns true if the node has an assigned literal (it might not be translated). * Caches the pair of the node and the literal corresponding to the * translation. * @param node the node * @param lit the literal */ - void cacheTranslation(TNode node, SatLiteral lit); + bool hasLiteral(TNode node) const; /** * Acquires a new variable from the SAT solver to represent the node @@ -172,7 +201,7 @@ public: * @param literal the literal from the sat solver * @return the actual node */ - Node getNode(const SatLiteral& literal); + TNode getNode(const SatLiteral& literal); /** * Returns the literal that represents the given node in the SAT CNF @@ -190,6 +219,11 @@ public: return d_nodeCache; } + /** + * Removes all the translation information of clauses that have the given associated assert level. + */ + void removeClausesAboveLevel(int level); + };/* class CnfStream */ diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index e8efe3d03..3e1fbba17 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -50,9 +50,13 @@ static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction o //================================================================================================= // Constructor/Destructor: -Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context) : +Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enable_incremental) : proxy(proxy) , context(context) + , assertionLevel(0) + , enable_incremental(enable_incremental) + , problem_extended(false) + , in_propagate(false) // Parameters (user settable): // , verbosity (0) @@ -92,7 +96,7 @@ Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context) : , simpDB_props (0) , order_heap (VarOrderLt(activity)) , progress_estimate (0) - , remove_satisfied (true) + , remove_satisfied (!enable_incremental) // Resource constraints: // @@ -120,7 +124,7 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) watches .init(mkLit(v, false)); watches .init(mkLit(v, true )); assigns .push(l_Undef); - vardata .push(mkVarData(CRef_Undef, 0)); + vardata .push(mkVarData(CRef_Undef, 0, assertionLevel)); //activity .push(0); activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0); seen .push(0); @@ -128,7 +132,14 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) decision .push(); trail .capacity(v+1); setDecisionVar(v, dvar); - theory .push(theoryAtom); + theory .push(theoryAtom); + + // We have extended the problem + if (in_propagate) { + problem_extended = true; + insertVarOrder(v); + } + return v; } @@ -148,9 +159,19 @@ CRef Solver::reason(Var x) const { // We're actually changing the state, so we hack it into non-const Solver* nonconst_this = const_cast<Solver*>(this); - // Construct the reason - CRef real_reason = nonconst_this->ca.alloc(explanation, true); - nonconst_this->vardata[x] = mkVarData(real_reason, level(x)); + // Compute the assertion level for this clause + int explLevel = 0; + for (int i = 0; i < explanation.size(); ++ i) { + int varLevel = intro_level(var(explanation[i])); + if (varLevel > explLevel) { + explLevel = varLevel; + } + } + + // 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); return real_reason; @@ -158,18 +179,61 @@ CRef Solver::reason(Var x) const { bool Solver::addClause_(vec<Lit>& ps, ClauseType type) { - assert(decisionLevel() == 0); if (!ok) return false; + // If a lemma propagates the literal, we mark this + bool propagate_first_literal = false; + // Check if clause is satisfied and remove false/duplicate literals: sort(ps); Lit p; int i, j; - for (i = j = 0, p = lit_Undef; i < ps.size(); i++) - if (value(ps[i]) == l_True || ps[i] == ~p) + 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<Lit> assigned_lits; + 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 return true; - else if (value(ps[i]) != l_False && ps[i] != p) - ps[j++] = p = ps[i]; - ps.shrink(i - j); + } + 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]; + assigned_lits.push(p); + Debug("minisat::lemmas") << proxy->getNode(p) << " has value " << value(p) << endl; + } + } + Assert(j >= 1, "You are asserting a falsified lemma, produce a conflict instead!"); + // If only one literal we could have unit propagation + if (j == 1) 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 (value(p) == l_True) propagate_first_literal = false; + else if (level(var(p)) > max_level) { + max_level = level(var(p)); + max_level_j = j - 1; + } + } + if (value(ps[1]) != l_Undef) { + swap(ps[1], ps[max_level_j]); + } + ps.shrink(i - j); + } if (ps.size() == 0) return ok = false; @@ -179,10 +243,19 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type) uncheckedEnqueue(ps[0]); return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef); }else{ - CRef cr = ca.alloc(ps, false); + CRef cr = ca.alloc(type == CLAUSE_LEMMA ? 0 : assertionLevel, ps, false); clauses.push(cr); - if (type == CLAUSE_LEMMA) lemmas.push(cr); - attachClause(cr); + attachClause(cr); + if (propagate_first_literal) { + Debug("minisat::lemmas") << "Lemma propagating: " << (theory[var(ps[0])] ? proxy->getNode(ps[0]).toString() : "bool") << endl; + lemma_propagated_literals.push(ps[0]); + lemma_propagated_reasons.push(cr); + propagating_lemmas.push(cr); + } + } + + if (in_propagate && type == CLAUSE_LEMMA) { + problem_extended = true; } return true; @@ -191,6 +264,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type) void Solver::attachClause(CRef cr) { const Clause& c = ca[cr]; + CVC4::Debug("minisat") << "Solver::attachClause(" << c << ")" << std::endl; Assert(c.size() > 1); watches[~c[0]].push(Watcher(cr, c[1])); watches[~c[1]].push(Watcher(cr, c[0])); @@ -250,15 +324,47 @@ 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; + + // 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) { + // Propagate + uncheckedEnqueue(lemma[0], propagating_lemmas[i]); + // Remember the lemma + propagating_lemmas[j++] = propagating_lemmas[i]; + } } - lemmas.shrink(lemmas.size() - lemmas_lim[level]); - lemmas_lim.shrink(lemmas_lim.size() - level); + propagating_lemmas.shrink(i - j); + propagating_lemmas_lim.shrink(propagating_lemmas_lim.size() - level); } } +void Solver::popTrail() { + // If we're not incremental, just pop until level 0 + if (!enable_incremental) { + cancelUntil(0); + } else { + // Otherwise pop until the last recorded level 0 trail index + int target_size = trail_user_lim.last(); + for (int c = trail.size()-1; c >= target_size; c--){ + Var x = var(trail[c]); + assigns [x] = l_Undef; + if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) + polarity[x] = sign(trail[c]); + insertVarOrder(x); } + qhead = target_size; + trail.shrink(trail.size() - target_size); + } +} //================================================================================================= // Major methods: @@ -301,9 +407,10 @@ Lit Solver::pickBranchLit() | * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. | * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the | rest of literals. There may be others from the same level though. +| * returns the maximal level of the resolved clauses | |________________________________________________________________________________________________@*/ -void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) +int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) { int pathC = 0; Lit p = lit_Undef; @@ -313,10 +420,16 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) out_learnt.push(); // (leave room for the asserting literal) int index = trail.size() - 1; + int max_level = 0; // Maximal level of the resolved clauses + do{ assert(confl != CRef_Undef); // (otherwise should be UIP) Clause& c = ca[confl]; + if (c.level() > max_level) { + max_level = c.level(); + } + if (c.learnt()) claBumpActivity(c); @@ -344,7 +457,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) out_learnt[0] = ~p; // Simplify conflict clause: - // int i, j; out_learnt.copyTo(analyze_toclear); if (ccmin_mode == 2){ @@ -352,9 +464,23 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) for (i = 1; i < out_learnt.size(); i++) abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) - for (i = j = 1; i < out_learnt.size(); i++) - if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level)) + for (i = j = 1; i < out_learnt.size(); i++) { + if (reason(var(out_learnt[i])) == CRef_Undef) { out_learnt[j++] = out_learnt[i]; + } else { + // Check if the literal is redundant + int red_level = litRedundant(out_learnt[i], abstract_level); + if (red_level < 0) { + // Literal is not redundant + out_learnt[j++] = out_learnt[i]; + } else { + // Literal is redundant, mark the level of the redundancy derivation + if (max_level < red_level) { + max_level = red_level; + } + } + } + } }else if (ccmin_mode == 1){ for (i = j = 1; i < out_learnt.size(); i++){ @@ -395,18 +521,25 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) } for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) + + // Return the maximal resolution level + return max_level; } // Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is // visiting literals at levels that cannot be removed later. -bool Solver::litRedundant(Lit p, uint32_t abstract_levels) +int Solver::litRedundant(Lit p, uint32_t abstract_levels) { analyze_stack.clear(); analyze_stack.push(p); int top = analyze_toclear.size(); + int max_level = 0; while (analyze_stack.size() > 0){ assert(reason(var(analyze_stack.last())) != CRef_Undef); Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop(); + if (c.level() > max_level) { + max_level = c.level(); + } for (int i = 1; i < c.size(); i++){ Lit p = c[i]; @@ -419,13 +552,13 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) for (int j = top; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; analyze_toclear.shrink(analyze_toclear.size() - top); - return false; + return -1; } } } } - return true; + return max_level; } @@ -472,7 +605,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()); + vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p))); trail.push_(p); if (theory[var(p)] && from != CRef_Lazy) { // Enqueue to the theory @@ -483,17 +616,22 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) CRef Solver::propagate(TheoryCheckType type) { + in_propagate = true; + CRef confl = CRef_Undef; // If this is the final check, no need for Boolean propagation and // theory propagation if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) { - return theoryCheck(CVC4::theory::Theory::FULL_EFFORT); + confl = theoryCheck(CVC4::theory::Theory::FULL_EFFORT); + in_propagate = false; + return confl; } // The effort we will be using to theory check CVC4::theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ? - CVC4::theory::Theory::QUICK_CHECK : CVC4::theory::Theory::STANDARD; + CVC4::theory::Theory::QUICK_CHECK : + CVC4::theory::Theory::STANDARD; // Keep running until we have checked everything, we // have no conflict and no new literals have been asserted @@ -513,6 +651,8 @@ CRef Solver::propagate(TheoryCheckType type) } } while (new_assertions); + in_propagate = false; + return confl; } @@ -548,11 +688,15 @@ CRef Solver::theoryCheck(CVC4::theory::Theory::Effort effort) 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) { - int current_level = level(var(clause[i])); - Debug("minisat") << "Literal: " << clause[i] << " with reason " << reason(var(clause[i])) << " at level " << current_level << std::endl; + 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; } // 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; @@ -561,8 +705,8 @@ CRef Solver::theoryCheck(CVC4::theory::Theory::Effort effort) 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 - c = ca.alloc(clause, true); + // Create the new clause and attach all the information (level 0) + c = ca.alloc(max_intro_level, clause, true); learnts.push(c); attachClause(c); } @@ -690,6 +834,18 @@ void Solver::removeSatisfied(vec<CRef>& cs) cs.shrink(i - j); } +void Solver::removeClausesAboveLevel(vec<CRef>& cs, int level) +{ + int i, j; + for (i = j = 0; i < cs.size(); i++){ + Clause& c = ca[cs[i]]; + if (c.level() > level) + removeClause(cs[i]); + else + cs[j++] = cs[i]; + } + cs.shrink(i - j); +} void Solver::rebuildOrderHeap() { @@ -756,20 +912,25 @@ lbool Solver::search(int nof_conflicts) TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD; for (;;){ + problem_extended = false; CRef confl = propagate(check_type); if (confl != CRef_Undef){ // CONFLICT conflicts++; conflictC++; if (decisionLevel() == 0) return l_False; + // Clear the propagated literals + lemma_propagated_literals.clear(); + lemma_propagated_reasons.clear(); + learnt_clause.clear(); - analyze(confl, learnt_clause, backtrack_level); + int max_level = analyze(confl, learnt_clause, backtrack_level); cancelUntil(backtrack_level); if (learnt_clause.size() == 1){ uncheckedEnqueue(learnt_clause[0]); }else{ - CRef cr = ca.alloc(learnt_clause, true); + CRef cr = ca.alloc(max_level, learnt_clause, true); learnts.push(cr); attachClause(cr); claBumpActivity(ca[cr]); @@ -791,11 +952,27 @@ 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 we have more assertions from lemmas, we continue + if (problem_extended) { + + for (int i = 0, i_end = lemma_propagated_literals.size(); i < i_end; ++ i) { + Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << endl; + uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]); + } + + lemma_propagated_literals.clear(); + lemma_propagated_reasons.clear(); + + check_type = CHECK_WITH_PROPAGATION_STANDARD; + + continue; + } + // If this was a final check, we are satisfiable if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) return l_True; @@ -895,6 +1072,8 @@ static double luby(double y, int x){ // NOTE: assumptions passed in member-variable 'assumptions'. lbool Solver::solve_() { + Debug("minisat") << "nvars = " << nVars() << endl; + model.clear(); conflict.clear(); if (!ok) return l_False; @@ -929,11 +1108,16 @@ lbool Solver::solve_() if (status == l_True){ // Extend & copy model: model.growTo(nVars()); - for (int i = 0; i < nVars(); i++) model[i] = value(i); + for (int i = 0; i < nVars(); i++) { + model[i] = value(i); + Debug("minisat") << i << " = " << model[i] << endl; + } }else if (status == l_False && conflict.size() == 0) ok = false; - cancelUntil(0); + // Cancel the trail downto previous push + popTrail(); + return status; } @@ -1066,3 +1250,42 @@ void Solver::garbageCollect() ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); to.moveTo(ca); } + +void Solver::push() +{ + if (enable_incremental) { + ++ assertionLevel; + trail_user_lim.push(trail.size()); + } +} + +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); + + // Pop the user trail size + popTrail(); + trail_user_lim.pop(); + + // Notify the cnf + proxy->removeClausesAboveLevel(assertionLevel); + } +} + +void Solver::unregisterVar(Lit lit) { + Var v = var(lit); + vardata[v].intro_level = -1; + setDecisionVar(v, false); +} + +void Solver::renewVar(Lit lit, int level) { + Var v = var(lit); + vardata[v].intro_level = level == -1 ? getAssertionLevel() : level; + setDecisionVar(v, true); +} + + diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index bb8a81f16..7050f2d10 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -56,18 +56,44 @@ protected: /** The context from the SMT solver */ CVC4::context::Context* context; + /** The current assertion level (user) */ + int assertionLevel; + + /** Returns the current user assertion level */ + int getAssertionLevel() const { return assertionLevel; } + + /** 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<Lit> lemma_propagated_literals; + /** Reasons of literals propagated by lemmas */ + vec<CRef> lemma_propagated_reasons; + /** Lemmas that propagated something, we need to recheck them after backtracking */ + vec<CRef> propagating_lemmas; + vec<int> propagating_lemmas_lim; + + /** Shrink 'cs' to contain only clauses below given level */ + void removeClausesAboveLevel(vec<CRef>& cs, int level); + + /** True if we are inside the propagate method */ + bool in_propagate; + public: // Constructor/Destructor: // - Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context); + Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enableIncremental = false); CVC4_PUBLIC ~Solver(); // Problem specification: // Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode. - // Types of clauses + // Types of clauses enum ClauseType { // Clauses defined by the problem CLAUSE_PROBLEM, @@ -77,6 +103,13 @@ public: CLAUSE_CONFLICT }; + // CVC4 context push/pop + void push (); + void pop (); + + void unregisterVar(Lit lit); // Unregister the literal (set assertion level to -1) + void renewVar(Lit lit, int level = -1); // Register the literal (set assertion level to the given level, or current level if -1) + bool addClause (const vec<Lit>& ps, 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. @@ -174,8 +207,8 @@ protected: // Helper structures: // - struct VarData { CRef reason; int level; }; - static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; } + 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 Watcher { CRef cref; @@ -213,6 +246,7 @@ protected: vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic. vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made. vec<int> trail_lim; // Separator indices for different decision levels in 'trail'. + vec<int> trail_user_lim; // Separator indices for different user push levels in 'trail'. vec<VarData> vardata; // Stores reason and level for each variable. int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'. @@ -224,10 +258,8 @@ protected: ClauseAllocator ca; - // CVC4 Stuff + // CVC4 Stuff vec<bool> theory; // Is the variable representing a theory atom - vec<CRef> lemmas; // List of lemmas we added (context dependent) - vec<int> lemmas_lim; // Separator indices for different decision levels in 'lemmas'. enum TheoryCheckType { // Quick check, but don't perform theory propagation @@ -268,9 +300,10 @@ protected: 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); // Backtrack until a certain level. - void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack) + void popTrail (); // Backtrack the trail to the previous push position + int analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack) void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? - bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') + int litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') - returns the maximal level of the clauses proving redundancy of p lbool search (int nof_conflicts); // Search for a given number of conflicts. lbool solve_ (); // Main solve method (assumptions given in 'assumptions'). void reduceDB (); // Reduce the set of learnt clauses. @@ -302,6 +335,7 @@ protected: CRef reason (Var x) const; bool hasReason (Var x) const; // Does the variable have a reason int level (Var x) const; + int intro_level (Var x) const; // Level at which this variable was introduced double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... bool withinBudget () const; @@ -321,6 +355,7 @@ protected: }; + //================================================================================================= // Implementation of inline methods: @@ -328,6 +363,8 @@ inline bool Solver::hasReason(Var x) const { return vardata[x].reason != CRef_Un 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 void Solver::insertVarOrder(Var x) { if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); } @@ -365,7 +402,7 @@ inline bool Solver::addClause (Lit p, ClauseType 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()); lemmas_lim.push(lemmas.size()); context->push(); } +inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); propagating_lemmas_lim.push(propagating_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/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 12a0fdb6b..41e9be744 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -127,19 +127,21 @@ class Clause { unsigned learnt : 1; unsigned has_extra : 1; unsigned reloced : 1; - unsigned size : 27; } header; + unsigned size : 27; + unsigned level : 32; } header; union { Lit lit; float act; uint32_t abs; CRef rel; } data[0]; friend class ClauseAllocator; // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). template<class V> - Clause(const V& ps, bool use_extra, bool learnt) { + Clause(const V& ps, bool use_extra, bool learnt, int level) { header.mark = 0; header.learnt = learnt; header.has_extra = use_extra; header.reloced = 0; header.size = ps.size(); + header.level = level; for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i]; @@ -160,6 +162,7 @@ public: data[header.size].abs = abstraction; } + int level () const { return header.level; } 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); } @@ -208,14 +211,14 @@ class ClauseAllocator : public RegionAllocator<uint32_t> RegionAllocator<uint32_t>::moveTo(to); } template<class Lits> - CRef alloc(const Lits& ps, bool learnt = false) + CRef alloc(int level, const Lits& ps, bool learnt = false) { assert(sizeof(Lit) == sizeof(uint32_t)); assert(sizeof(float) == sizeof(uint32_t)); bool use_extra = learnt | extra_clause_field; CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra)); - new (lea(cid)) Clause(ps, use_extra, learnt); + new (lea(cid)) Clause(ps, use_extra, learnt, level); return cid; } @@ -239,7 +242,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t> if (c.reloced()) { cr = c.relocation(); return; } - cr = to.alloc(c, c.learnt()); + cr = to.alloc(c.level(), c, c.learnt()); c.relocate(cr); // Copy extra data-fields: @@ -368,6 +371,11 @@ class CMap |________________________________________________________________________________________________@*/ inline Lit Clause::subsumes(const Clause& other) const { + // We restrict subsumtion to clauses at higher levels (if !enable_incremantal this should always be false) + if (level() > other.level()) { + return lit_Error; + } + //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); diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 32ac223d6..8bcd9fe76 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -44,15 +44,15 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of // Constructor/Destructor: -SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context) : - Solver(proxy, context) +SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enableIncremental) : + Solver(proxy, context, enableIncremental) , grow (opt_grow) , clause_lim (opt_clause_lim) , subsumption_lim (opt_subsumption_lim) , simp_garbage_frac (opt_simp_garbage_frac) , use_asymm (opt_use_asymm) , use_rcheck (opt_use_rcheck) - , use_elim (opt_use_elim) + , use_elim (!enableIncremental) , merges (0) , asymm_lits (0) , eliminated_vars (0) @@ -65,7 +65,7 @@ SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* con { vec<Lit> dummy(1,lit_Undef); ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below. - bwdsub_tmpunit = ca.alloc(dummy); + bwdsub_tmpunit = ca.alloc(0, dummy); remove_satisfied = false; } diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 977da46e5..a7359e28e 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -41,7 +41,7 @@ class SimpSolver : public Solver { public: // Constructor/Destructor: // - SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context); + SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enableIncremental = false); CVC4_PUBLIC ~SimpSolver(); // Problem specification: @@ -52,7 +52,7 @@ class SimpSolver : public 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<Lit>& ps, ClauseType type); + bool addClause_(vec<Lit>& ps, ClauseType type); bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). // Variable mode: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 5851f3990..45d941553 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -22,7 +22,6 @@ #include "theory/theory_engine.h" #include "util/Assert.h" -#include "util/decision_engine.h" #include "util/options.h" #include "util/output.h" #include "util/result.h" @@ -57,11 +56,9 @@ public: } }; -PropEngine::PropEngine(DecisionEngine* de, TheoryEngine* te, +PropEngine::PropEngine(TheoryEngine* te, Context* context, const Options& opts) : d_inCheckSat(false), - // d_options(opts), - d_decisionEngine(de), d_theoryEngine(te), d_context(context) { Debug("prop") << "Constructing the PropEngine" << endl; @@ -85,9 +82,9 @@ void PropEngine::assertFormula(TNode node) { void PropEngine::assertLemma(TNode node) { Assert(d_inCheckSat, "Sat solver should be in solve()!"); - Debug("prop") << "assertFormula(" << node << ")" << endl; + Debug("prop::lemma") << "assertLemma(" << node << ")" << endl; // Assert as removable - d_cnfStream->convertAndAssert(node, false, false); + d_cnfStream->convertAndAssert(node, true, false); } @@ -101,8 +98,8 @@ void PropEngine::printSatisfyingAssignment(){ end = transCache.end(); i != end; ++i) { - pair<Node, SatLiteral> curr = *i; - SatLiteral l = curr.second; + pair<Node, CnfStream::TranslationInfo> curr = *i; + SatLiteral l = curr.second.literal; if(!sign(l)) { Node n = curr.first; SatLiteralValue value = d_satSolver->value(l); @@ -150,11 +147,13 @@ Node PropEngine::getValue(TNode node) { void PropEngine::push() { Assert(!d_inCheckSat, "Sat solver in solve()!"); + d_satSolver->push(); Debug("prop") << "push()" << endl; } void PropEngine::pop() { Assert(!d_inCheckSat, "Sat solver in solve()!"); + d_satSolver->pop(); Debug("prop") << "pop()" << endl; } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index ecef29ac2..b43c2d859 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -24,7 +24,6 @@ #define __CVC4__PROP_ENGINE_H #include "expr/node.h" -#include "util/decision_engine.h" #include "util/options.h" #include "util/result.h" @@ -52,9 +51,6 @@ class PropEngine { /** The global options */ //const Options d_options; - /** The decision engine we will be using */ - DecisionEngine *d_decisionEngine; - /** The theory engine we will be using */ TheoryEngine *d_theoryEngine; @@ -76,7 +72,7 @@ public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(DecisionEngine*, TheoryEngine*, context::Context*, const Options&); + PropEngine(TheoryEngine*, context::Context*, const Options&); /** * Destructor. diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 2197cb23e..97c5d1419 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -94,5 +94,13 @@ void SatSolver::setCnfStream(CnfStream* cnfStream) { d_cnfStream = cnfStream; } +void SatSolver::removeClausesAboveLevel(int level) { + d_cnfStream->removeClausesAboveLevel(level); +} + +TNode SatSolver::getNode(SatLiteral lit) { + return d_cnfStream->getNode(lit); +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/sat.h b/src/prop/sat.h index 550de5527..6e244d9d7 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -103,6 +103,12 @@ public: virtual void addClause(SatClause& clause, bool lemma) = 0; /** Create a new boolean variable in the solver. */ virtual SatVariable newVar(bool theoryAtom = false) = 0; + /** Get the current decision level of the solver */ + virtual int getLevel() const = 0; + /** Unregister the variable (of the literal) from solving */ + virtual void unregisterVar(SatLiteral lit) = 0; + /** Register the variable (of the literal) for solving */ + virtual void renewVar(SatLiteral lit, int level = -1) = 0; }; /** @@ -226,6 +232,21 @@ public: void setCnfStream(CnfStream* cnfStream); SatLiteralValue value(SatLiteral l); + + int getLevel() const; + + void push(); + + void pop(); + + void removeClausesAboveLevel(int level); + + void unregisterVar(SatLiteral lit); + + void renewVar(SatLiteral lit, int level = -1); + + TNode getNode(SatLiteral lit); + };/* class SatSolver */ /* Functions that delegate to the concrete SAT solver. */ @@ -241,7 +262,7 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, d_statistics() { // Create the solver - d_minisat = new Minisat::SimpSolver(this, d_context); + d_minisat = new Minisat::SimpSolver(this, d_context, options.incrementalSolving); // Setup the verbosity d_minisat->verbosity = (options.verbosity > 0) ? 1 : -1; @@ -273,6 +294,26 @@ inline SatLiteralValue SatSolver::value(SatLiteral l) { return d_minisat->modelValue(l); } +inline void SatSolver::push() { + d_minisat->push(); +} + +inline void SatSolver::pop() { + d_minisat->pop(); +} + +inline int SatSolver::getLevel() const { + return d_minisat->getAssertionLevel(); +} + +inline void SatSolver::unregisterVar(SatLiteral lit) { + d_minisat->unregisterVar(lit); +} + +inline void SatSolver::renewVar(SatLiteral lit, int level) { + d_minisat->renewVar(lit, level); +} + #endif /* __CVC4_USE_MINISAT */ inline size_t diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 151f7237b..bf74ab844 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -124,24 +124,24 @@ SmtEngine::SmtEngine(ExprManager* em, const Options& opts) throw() : void SmtEngine::init(const Options& opts) throw() { d_context = d_exprManager->getContext(); + d_userContext = new Context(); + d_nodeManager = d_exprManager->getNodeManager(); NodeManagerScope nms(d_nodeManager); - d_decisionEngine = new DecisionEngine; // 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_context, opts); - d_propEngine = new PropEngine(d_decisionEngine, d_theoryEngine, - d_context, opts); + d_propEngine = new PropEngine(d_theoryEngine, d_context, opts); d_theoryEngine->setPropEngine(d_propEngine); - d_definedFunctions = new(true) DefinedFunctionMap(d_context); + d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); d_assertionList = NULL; d_interactive = opts.interactive; if(d_interactive) { - d_assertionList = new(true) AssertionList(d_context); + d_assertionList = new(true) AssertionList(d_userContext); } d_assignments = NULL; @@ -156,7 +156,6 @@ void SmtEngine::init(const Options& opts) throw() { void SmtEngine::shutdown() { d_propEngine->shutdown(); d_theoryEngine->shutdown(); - d_decisionEngine->shutdown(); } SmtEngine::~SmtEngine() { @@ -174,9 +173,10 @@ SmtEngine::~SmtEngine() { d_definedFunctions->deleteSelf(); + delete d_userContext; + delete d_theoryEngine; delete d_propEngine; - delete d_decisionEngine; } void SmtEngine::setLogic(const std::string& s) throw(ModalException) { @@ -457,8 +457,10 @@ Result SmtEngine::checkSat(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT checkSat(" << e << ")" << endl; ensureBoolean(e);// ensure expr is type-checked at this point + internalPush(); SmtEnginePrivate::addFormula(*this, e.getNode()); Result r = check().asSatisfiabilityResult(); + internalPop(); d_status = r; d_haveAdditions = false; Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl; @@ -470,8 +472,10 @@ Result SmtEngine::query(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT query(" << e << ")" << endl; ensureBoolean(e);// ensure expr is type-checked at this point + internalPush(); SmtEnginePrivate::addFormula(*this, e.getNode().notNode()); Result r = check().asValidityResult(); + internalPop(); d_status = r; d_haveAdditions = false; Debug("smt") << "SMT query(" << e << ") ==> " << r << endl; @@ -629,21 +633,37 @@ vector<Expr> SmtEngine::getAssertions() void SmtEngine::push() { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT push()" << endl; - d_context->push(); - d_propEngine->push(); + d_userLevels.push_back(d_userContext->getLevel()); + internalPush(); Debug("userpushpop") << "SmtEngine: pushed to level " - << d_context->getLevel() << endl; + << d_userContext->getLevel() << endl; } void SmtEngine::pop() { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT pop()" << endl; - d_propEngine->pop(); - d_context->pop(); + Assert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel()); + while (d_userLevels.back() < d_userContext->getLevel()) { + internalPop(); + } + d_userLevels.pop_back(); + Debug("userpushpop") << "SmtEngine: popped to level " - << d_context->getLevel() << endl; + << d_userContext->getLevel() << endl; // FIXME: should we reset d_status here? // SMT-LIBv2 spec seems to imply no, but it would make sense to.. } +void SmtEngine::internalPop() { + Debug("smt") << "internalPop()" << endl; + d_propEngine->pop(); + d_userContext->pop(); +} + +void SmtEngine::internalPush() { + Debug("smt") << "internalPush()" << endl; + d_userContext->push(); + d_propEngine->push(); +} + }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 854399bd7..d8d9f4b54 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -48,7 +48,6 @@ typedef NodeTemplate<false> TNode; class NodeHashFunction; class TheoryEngine; -class DecisionEngine; namespace context { class Context; @@ -91,16 +90,18 @@ class CVC4_PUBLIC SmtEngine { /** The type of our internal assignment set */ typedef context::CDSet<Node, NodeHashFunction> AssignmentSet; - /** Our Context */ + /** Expr manager context */ context::Context* d_context; + + /** The context levels of user pushes */ + std::vector<int> d_userLevels; + /** User level context */ + context::Context* d_userContext; + /** Our expression manager */ ExprManager* d_exprManager; /** Out internal expression/node manager */ NodeManager* d_nodeManager; - /** User-level options */ - //const Options d_options; - /** The decision engine */ - DecisionEngine* d_decisionEngine; /** The decision engine */ TheoryEngine* d_theoryEngine; /** The propositional engine */ @@ -190,6 +191,10 @@ class CVC4_PUBLIC SmtEngine { */ void ensureBoolean(const BoolExpr& e); + void internalPush(); + + void internalPop(); + friend class ::CVC4::smt::SmtEnginePrivate; public: diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index d50c48552..25aff4e75 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -237,10 +237,12 @@ inline int deltaCoeff(Kind k){ case kind::EQUAL: return kind::DISTINCT; default: + Unreachable(); return kind::UNDEFINED_KIND; } } default: + Unreachable(); return kind::UNDEFINED_KIND; } } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 181632812..7b768d9af 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -103,21 +103,8 @@ ArithVar TheoryArith::findBasicRow(ArithVar variable){ void TheoryArith::preRegisterTerm(TNode n) { Debug("arith_preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl; Kind k = n.getKind(); - if(k == EQUAL){ - TNode left = n[0]; - TNode right = n[1]; - - Node lt = NodeManager::currentNM()->mkNode(LT, left,right); - Node gt = NodeManager::currentNM()->mkNode(GT, left,right); - Node eagerSplit = NodeManager::currentNM()->mkNode(OR, n, lt, gt); - - d_splits.push_back(eagerSplit); - - d_out->augmentingLemma(eagerSplit); - } - - bool isStrictlyVarList = n.getKind() == kind::MULT && VarList::isMember(n); + bool isStrictlyVarList = k == kind::MULT && VarList::isMember(n); if(isStrictlyVarList){ d_out->setIncomplete(); @@ -307,15 +294,49 @@ bool TheoryArith::assertionCases(TNode assertion){ <<x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl; switch(simpKind){ case LEQ: + if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) { + Node diseq = assertion[0].eqNode(assertion[1]).notNode(); + if (d_diseq.find(diseq) != d_diseq.end()) { + NodeBuilder<3> conflict(kind::AND); + conflict << diseq << assertion << d_partialModel.getLowerConstraint(x_i); + d_out->conflict((TNode)conflict); + return true; + } + } case LT: return d_simplex.AssertUpper(x_i, c_i, assertion); - case GT: case GEQ: + if (d_partialModel.hasUpperBound(x_i) && d_partialModel.getUpperBound(x_i) == c_i) { + Node diseq = assertion[0].eqNode(assertion[1]).notNode(); + if (d_diseq.find(diseq) != d_diseq.end()) { + NodeBuilder<3> conflict(kind::AND); + conflict << diseq << assertion << d_partialModel.getUpperConstraint(x_i); + d_out->conflict((TNode)conflict); + return true; + } + } + case GT: return d_simplex.AssertLower(x_i, c_i, assertion); case EQUAL: return d_simplex.AssertEquality(x_i, c_i, assertion); case DISTINCT: - d_diseq.push_back(assertion); + { + d_diseq.insert(assertion); + // Check if it conflicts with the the bounds + TNode eq = assertion[0]; + Assert(eq.getKind() == kind::EQUAL); + TNode lhs = eq[0]; + TNode rhs = eq[1]; + Assert(rhs.getKind() == CONST_RATIONAL); + ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL); + DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL); + if (d_partialModel.hasLowerBound(lhsVar) && d_partialModel.hasUpperBound(lhsVar) && + d_partialModel.getLowerBound(lhsVar) == rhsValue && d_partialModel.getUpperBound(lhsVar) == rhsValue) { + NodeBuilder<3> conflict(kind::AND); + conflict << assertion << d_partialModel.getLowerConstraint(lhsVar) << d_partialModel.getUpperConstraint(lhsVar); + d_out->conflict((TNode)conflict); + } + } return false; default: Unreachable(); @@ -323,7 +344,7 @@ bool TheoryArith::assertionCases(TNode assertion){ } } -void TheoryArith::check(Effort level){ +void TheoryArith::check(Effort effortLevel){ Debug("arith") << "TheoryArith::check begun" << std::endl; while(!done()){ @@ -339,8 +360,25 @@ void TheoryArith::check(Effort level){ } } - //TODO This must be done everytime for the time being - if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); } + if(Debug.isOn("arith::print_assertions") && fullEffort(effortLevel)) { + Debug("arith::print_assertions") << "Assertions:" << endl; + for (ArithVar i = 0; i < d_variables.size(); ++ i) { + if (d_partialModel.hasLowerBound(i)) { + Node lConstr = d_partialModel.getLowerConstraint(i); + Debug("arith::print_assertions") << lConstr.toString() << endl; + } + + if (d_partialModel.hasUpperBound(i)) { + Node uConstr = d_partialModel.getUpperConstraint(i); + Debug("arith::print_assertions") << uConstr.toString() << endl; + } + } + context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin(); + context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end(); + for(; it != it_end; ++ it) { + Debug("arith::print_assertions") << *it << endl; + } + } Node possibleConflict = d_simplex.updateInconsistentVars(); if(possibleConflict != Node::null()){ @@ -355,10 +393,36 @@ void TheoryArith::check(Effort level){ Debug("arith_conflict") <<"Found a conflict "<< possibleConflict << endl; }else{ d_partialModel.commitAssignmentChanges(); + + if (fullEffort(effortLevel)) { + context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin(); + context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end(); + for(; it != it_end; ++ it) { + TNode eq = (*it)[0]; + Assert(eq.getKind() == kind::EQUAL); + TNode lhs = eq[0]; + TNode rhs = eq[1]; + Assert(rhs.getKind() == CONST_RATIONAL); + ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL); + if(d_tableau.isEjected(lhsVar)){ + d_simplex.reinjectVariable(lhsVar); + } + DeltaRational lhsValue = d_partialModel.getAssignment(lhsVar); + DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL); + if (lhsValue == rhsValue) { + Debug("arith_lemma") << "Splitting on " << eq << endl; + Debug("arith_lemma") << "LHS value = " << lhsValue << endl; + Debug("arith_lemma") << "RHS value = " << rhsValue << endl; + Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs; + Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs; + Node lemma = NodeBuilder<3>(OR) << eq << ltNode << gtNode; + d_out->lemma(lemma); + } + } + } } if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); } - Debug("arith") << "TheoryArith::check end" << std::endl; if(Debug.isOn("arith::print_model")) { @@ -372,17 +436,6 @@ void TheoryArith::check(Effort level){ Debug("arith::print_model") << endl; } } - if(Debug.isOn("arith::print_assertions")) { - Debug("arith::print_assertions") << "Assertions:" << endl; - for (ArithVar i = 0; i < d_variables.size(); ++ i) { - Node lConstr = d_partialModel.getLowerConstraint(i); - Debug("arith::print_assertions") << lConstr.toString() << endl; - - Node uConstr = d_partialModel.getUpperConstraint(i); - Debug("arith::print_assertions") << uConstr.toString() << endl; - - } - } } void TheoryArith::explain(TNode n, Effort e) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index af52da444..5c65b993d 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -24,6 +24,7 @@ #include "theory/theory.h" #include "context/context.h" #include "context/cdlist.h" +#include "context/cdset.h" #include "expr/node.h" #include "theory/arith/arith_utilities.h" @@ -86,7 +87,7 @@ private: /** * List of all of the inequalities asserted in the current context. */ - context::CDList<Node> d_diseq; + context::CDSet<Node, NodeHashFunction> d_diseq; /** * The tableau for all of the constraints seen thus far in the system. diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 1c48c0160..269f28732 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -100,17 +100,6 @@ public: throw(Interrupted, AssertionException) = 0; /** - * Tell the core to add the following valid lemma as if it were a - * user assertion. This should NOT be called during solving, only - * preprocessing. - * - * @param n - a theory lemma valid to be asserted - * @param safe - whether it is safe to be interrupted - */ - virtual void augmentingLemma(TNode n, bool safe = false) - throw(Interrupted, AssertionException) = 0; - - /** * Provide an explanation in response to an explanation request. * * @param n - an explanation diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index b2f047824..7958d977e 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -106,11 +106,7 @@ class TheoryEngine { ++(d_engine->d_statistics.d_statLemma); d_engine->newLemma(node); } - void augmentingLemma(TNode node, bool) - throw(theory::Interrupted, AssertionException) { - ++(d_engine->d_statistics.d_statAugLemma); - d_engine->newAugmentingLemma(node); - } + void explanation(TNode explanationNode, bool) throw(theory::Interrupted, AssertionException) { d_explanationNode = explanationNode; @@ -322,12 +318,7 @@ public: } inline void newLemma(TNode node) { - d_propEngine->assertLemma(node); - } - - inline void newAugmentingLemma(TNode node) { - Node preprocessed = preprocess(node); - d_propEngine->assertFormula(preprocessed); + d_propEngine->assertLemma(preprocess(node)); } /** diff --git a/src/util/Makefile.am b/src/util/Makefile.am index af3457550..837837cd6 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -12,8 +12,6 @@ libutil_la_SOURCES = \ Makefile.in \ congruence_closure.h \ debug.h \ - decision_engine.cpp \ - decision_engine.h \ exception.h \ hash.h \ bool.h \ @@ -29,7 +27,6 @@ libutil_la_SOURCES = \ rational.h \ integer.h \ bitvector.h \ - bitvector.cpp \ gmp_util.h \ sexpr.h \ stats.h \ @@ -44,12 +41,10 @@ BUILT_SOURCES = \ if CVC4_CLN_IMP libutil_la_SOURCES += \ - integer_cln_imp.cpp \ rational_cln_imp.cpp endif if CVC4_GMP_IMP libutil_la_SOURCES += \ - integer_gmp_imp.cpp \ rational_gmp_imp.cpp endif @@ -57,11 +52,9 @@ EXTRA_DIST = \ rational_cln_imp.h \ integer_cln_imp.h \ rational_cln_imp.cpp \ - integer_cln_imp.cpp \ rational_gmp_imp.h \ integer_gmp_imp.h \ rational_gmp_imp.cpp \ - integer_gmp_imp.cpp \ rational.h.in \ integer.h.in \ tls.h.in diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp deleted file mode 100644 index 8ea95e1c9..000000000 --- a/src/util/bitvector.cpp +++ /dev/null @@ -1,32 +0,0 @@ -/********************* */ -/*! \file bitvector.cpp - ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): taking - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "bitvector.h" - -namespace CVC4 { - -std::ostream& operator <<(std::ostream& os, const BitVector& bv) { - return os << bv.toString(); -} - -std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) { - return os << "[" << bv.high << ":" << bv.low << "]"; -} - -}/* CVC4 namespace */ diff --git a/src/util/bitvector.h b/src/util/bitvector.h index edf4e987d..51239cbbb 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -245,8 +245,13 @@ struct UnsignedHashStrategy { } }; -std::ostream& operator <<(std::ostream& os, const BitVector& bv); -std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv); +inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) { + return os << bv.toString(); +} + +inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) { + return os << "[" << bv.high << ":" << bv.low << "]"; +} }/* CVC4 namespace */ diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp deleted file mode 100644 index 692520257..000000000 --- a/src/util/integer_cln_imp.cpp +++ /dev/null @@ -1,37 +0,0 @@ -/********************* */ -/*! \file integer_cln_imp.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief A multiprecision rational constant. - ** - ** A multiprecision rational constant. - ** This stores the rational as a pair of multiprecision integers, - ** one for the numerator and one for the denominator. - ** The number is always stored so that the gcd of the numerator and denominator - ** is 1. (This is referred to as referred to as canonical form in GMP's - ** literature.) A consquence is that that the numerator and denominator may be - ** different than the values used to construct the Rational. - **/ - -#include "cvc4autoconfig.h" -#include "util/integer.h" - -#ifndef CVC4_CLN_IMP -# error "This source should only ever be built if CVC4_CLN_IMP is on !" -#endif /* CVC4_CLN_IMP */ - -using namespace CVC4; - -std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) { - return os << n.toString(); -} - diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index ee256867a..21f6c7581 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -228,7 +228,9 @@ struct IntegerHashStrategy { } };/* struct IntegerHashStrategy */ -std::ostream& operator<<(std::ostream& os, const Integer& n); +inline std::ostream& operator<<(std::ostream& os, const Integer& n) { + return os << n.toString(); +} }/* CVC4 namespace */ diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp deleted file mode 100644 index 1c2bd7ccd..000000000 --- a/src/util/integer_gmp_imp.cpp +++ /dev/null @@ -1,37 +0,0 @@ -/********************* */ -/*! \file integer_gmp_imp.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief A multiprecision rational constant. - ** - ** A multiprecision rational constant. - ** This stores the rational as a pair of multiprecision integers, - ** one for the numerator and one for the denominator. - ** The number is always stored so that the gcd of the numerator and denominator - ** is 1. (This is referred to as referred to as canonical form in GMP's - ** literature.) A consquence is that that the numerator and denominator may be - ** different than the values used to construct the Rational. - **/ - -#include "cvc4autoconfig.h" -#include "util/integer.h" - -#ifndef CVC4_GMP_IMP -# error "This source should only ever be built if CVC4_GMP_IMP is on !" -#endif /* CVC4_GMP_IMP */ - -using namespace CVC4; - -std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) { - return os << n.toString(); -} - diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 44f460559..72a653545 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -164,7 +164,9 @@ struct IntegerHashStrategy { } };/* struct IntegerHashStrategy */ -std::ostream& operator<<(std::ostream& os, const Integer& n); +inline std::ostream& operator<<(std::ostream& os, const Integer& n) { + return os << n.toString(); +} }/* CVC4 namespace */ diff --git a/src/util/options.cpp b/src/util/options.cpp index dbfed887d..8f26d9376 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -66,7 +66,8 @@ static const string optionsDescription = "\ --no-interactive do not run interactively\n\ --produce-models support the get-value command\n\ --produce-assignments support the get-assignment command\n\ - --lazy-definition-expansion expand define-fun lazily\n"; + --lazy-definition-expansion expand define-fun lazily\n\ + --incremental enable incremental solving\n"; static const string languageDescription = "\ Languages currently supported as arguments to the -L / --lang option:\n\ @@ -119,6 +120,7 @@ enum OptionValue { NO_TYPE_CHECKING, LAZY_TYPE_CHECKING, EAGER_TYPE_CHECKING, + INCREMENTAL };/* enum OptionValue */ /** @@ -174,6 +176,7 @@ static struct option cmdlineOptions[] = { { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING}, { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING}, { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING}, + { "incremental", no_argument, NULL, INCREMENTAL}, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -367,6 +370,10 @@ throw(OptionException) { earlyTypeChecking = true; break; + case INCREMENTAL: + incrementalSolving = true; + break; + case SHOW_CONFIG: fputs(Configuration::about().c_str(), stdout); printf("\n"); diff --git a/src/util/options.h b/src/util/options.h index 60c8f2a1a..1eca0d499 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -126,6 +126,9 @@ struct CVC4_PUBLIC Options { /** Whether we do typechecking at Expr creation time. */ bool earlyTypeChecking; + /** Whether incemental solving (push/pop) */ + bool incrementalSolving; + Options() : binary_name(), statistics(false), @@ -147,7 +150,8 @@ struct CVC4_PUBLIC Options { produceModels(false), produceAssignments(false), typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT), - earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) { + earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT), + incrementalSolving(false) { } /** |