diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 75 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 3 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 49 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 6 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 48 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 20 | ||||
-rw-r--r-- | src/prop/sat.h | 24 | ||||
-rw-r--r-- | src/prop/sat_module.cpp | 3 | ||||
-rw-r--r-- | src/prop/sat_module.h | 6 |
9 files changed, 217 insertions, 17 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 9f49d81a2..396454fac 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -50,9 +50,19 @@ CnfStream::CnfStream(SatSolverInterface *satSolver, Registrar* registrar, bool f d_registrar(registrar) { } -void CnfStream::recordTranslation(TNode node) { +void CnfStream::recordTranslation(TNode node, bool alwaysRecord) { + Debug("cnf") << "recordTranslation(" << alwaysRecord << "," << d_removable << "): " << node << std::endl; if (!d_removable) { - d_translationTrail.push_back(stripNot(node)); + node = stripNot(node); + if(d_translationCache.find(node)->second.recorded) { + Debug("cnf") << "--> Already recorded, not recording again." << std::endl; + } else { + Debug("cnf") << "--> Recorded at position " << d_translationTrail.size() << ". (level " << d_translationCache.find(node)->second.level << ")" << std::endl; + Assert(d_translationTrail.empty() || d_translationCache.find(node)->second.level >= d_translationCache.find(d_translationTrail.back())->second.level, "levels on the translation trail should be monotonically increasing ?!"); + d_translationTrail.push_back(node); + d_translationCache.find(node)->second.recorded = true; + d_translationCache.find(node.notNode())->second.recorded = true; + } } } @@ -112,7 +122,8 @@ bool CnfStream::hasLiteral(TNode n) const { void TseitinCnfStream::ensureLiteral(TNode n) { if(hasLiteral(n)) { // Already a literal! - SatLiteral lit = getLiteral(n); + // newLiteral() may be necessary to renew a previously-extant literal + SatLiteral lit = isTranslated(n) ? getLiteral(n) : newLiteral(n, true); NodeCache::iterator i = d_nodeCache.find(lit); if(i == d_nodeCache.end()) { // Store backward-mappings @@ -158,11 +169,12 @@ void TseitinCnfStream::ensureLiteral(TNode n) { SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl; + Assert(node.getKind() != kind::NOT); // Get the literal for this node SatLiteral lit; if (!hasLiteral(node)) { - // If no literal, well make one + // If no literal, we'll make one lit = SatLiteral(d_satSolver->newVar(theoryLiteral)); d_translationCache[node].literal = lit; d_translationCache[node.notNode()].literal = ~lit; @@ -174,13 +186,15 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { // We will translate clauses, so remember the level int level = d_satSolver->getAssertionLevel(); + d_translationCache[node].recorded = false; + d_translationCache[node.notNode()].recorded = false; d_translationCache[node].level = level; d_translationCache[node.notNode()].level = level; // If it's a theory literal, need to store it for back queries if ( theoryLiteral || d_fullLitToNodeMap || ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) || - Dump.isOn("clauses") ) { + (Dump.isOn("clauses")) ) { d_nodeCache[lit] = node; d_nodeCache[~lit] = node.notNode(); } @@ -223,6 +237,11 @@ SatLiteral CnfStream::convertAtom(TNode node) { } } + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(node, true); + return lit; } @@ -250,6 +269,11 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { assertClause(xorNode, a, ~b, xorLit); assertClause(xorNode, ~a, b, xorLit); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(xorNode, true); + return xorLit; } @@ -285,6 +309,11 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) { // This needs to go last, as the clause might get modified by the SAT solver assertClause(orNode, clause); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(orNode, true); + // Return the literal return orLit; } @@ -321,6 +350,12 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { clause[n_children] = andLit; // This needs to go last, as the clause might get modified by the SAT solver assertClause(andNode, clause); + + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(andNode, true); + return andLit; } @@ -345,6 +380,11 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { assertClause(impliesNode, a, impliesLit); assertClause(impliesNode, ~b, impliesLit); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(impliesNode, true); + return impliesLit; } @@ -377,6 +417,11 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { assertClause(iffNode, ~a, ~b, iffLit); assertClause(iffNode, a, b, iffLit); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(iffNode, true); + return iffLit; } @@ -423,6 +468,11 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { assertClause(iteNode, iteLit, ~condLit, ~thenLit); assertClause(iteNode, iteLit, condLit, ~elseLit); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(iteNode, true); + return iteLit; } @@ -435,6 +485,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { // If the non-negated node has already been translated, get the translation if(isTranslated(node)) { + Debug("cnf") << "toCNF(): already translated" << endl; nodeLit = getLiteral(node); } else { // Handle each Boolean operator case @@ -690,15 +741,19 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { void CnfStream::removeClausesAboveLevel(int level) { while (d_translationTrail.size() > 0) { + Debug("cnf") << "Considering translation trail position " << d_translationTrail.size() << std::endl; TNode node = d_translationTrail.back(); + // Get the translation information + TranslationInfo& infoPos = d_translationCache.find(node)->second; + // If the level of the node is less or equal to given we are done + if (infoPos.level >= 0 && infoPos.level <= level) { + Debug("cnf") << "Node is " << node << " level " << infoPos.level << ", we're done." << std::endl; + break; + } 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); } @@ -734,6 +789,7 @@ void CnfStream::undoTranslate(TNode node, int level) { // Untranslate infoPos.level = -1; + infoPos.recorded = false; // Untranslate the negation node // If not a not node, unregister it from sat and untranslate the negation @@ -747,6 +803,7 @@ void CnfStream::undoTranslate(TNode node, int level) { Assert(it != d_translationCache.end()); TranslationInfo& infoNeg = (*it).second; infoNeg.level = -1; + infoNeg.recorded = false; } // undoTranslate the children diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index c9306952b..4812c6a21 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -52,6 +52,7 @@ public: /** Per node translation information */ struct TranslationInfo { + bool recorded; /** The level at which this node was translated (negative if not translated) */ int level; /** The literal of this node */ @@ -109,7 +110,7 @@ protected: } /** Record this translation */ - void recordTranslation(TNode node); + void recordTranslation(TNode node, bool alwaysRecord = false); /** * Moves the node and all of it's parents to level 0. diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 3fe9db10c..678fe28dc 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -714,10 +714,11 @@ CRef Solver::propagate(TheoryCheckType type) } void Solver::propagateTheory() { - - SatClause propagatedLiteralsClause; + SatClause propagatedLiteralsClause; + // Doesn't actually call propagate(); that's done in theoryCheck() now that combination + // is online. This just incorporates those propagations previously discovered. proxy->theoryPropagate(propagatedLiteralsClause); - + vec<Lit> propagatedLiterals; DPLLMinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); @@ -885,10 +886,22 @@ void Solver::removeClausesAboveLevel(vec<CRef>& cs, int level) for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; if (c.level() > level) { - Debug("minisat") << "removeClausesAboveLevel(" << level << "): removing level-" << c.level() << " clause: " << c << std::endl; + if(Debug.isOn("minisat")) { + Debug("minisat") << "removeClausesAboveLevel(" << level << "): removing level-" << c.level() << " clause: " << c << ":"; + for(int i = 0; i < c.size(); ++i) { + Debug("minisat") << " " << c[i]; + } + Debug("minisat") << std::endl; + } removeClause(cs[i]); } else { - Debug("minisat") << "removeClausesAboveLevel(" << level << "): leaving level-" << c.level() << " clause: " << c << std::endl; + if(Debug.isOn("minisat")) { + Debug("minisat") << "removeClausesAboveLevel(" << level << "): leaving level-" << c.level() << " clause: " << c << ":"; + for(int i = 0; i < c.size(); ++i) { + Debug("minisat") << " " << c[i]; + } + Debug("minisat") << std::endl; + } cs[j++] = cs[i]; } } @@ -1328,16 +1341,25 @@ void Solver::push() Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl; trail_user.push(lit_Undef); trail_ok.push(ok); + trail_user_lim.push(trail.size()); + assert(trail_user_lim.size() == assertionLevel); + Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl; } void Solver::pop() { assert(enable_incremental); + Debug("minisat") << "MINISAT POP at level " << decisionLevel() << " (context " << context->getLevel() << "), popping trail..." << std::endl; popTrail(); + Debug("minisat") << "MINISAT POP now at " << decisionLevel() << " (context " << context->getLevel() << ")" << std::endl; + + assert(decisionLevel() == 0); + assert(trail_user_lim.size() == assertionLevel); --assertionLevel; + Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", need to get down to " << trail_user_lim.last() << std::endl; Debug("minisat") << "in user pop, reducing assertion level to " << assertionLevel << " and removing clauses above this from db" << std::endl; // Remove all the clauses asserted (and implied) above the new base level @@ -1346,6 +1368,23 @@ void Solver::pop() Debug("minisat") << "in user pop, at " << trail_lim.size() << " : " << assertionLevel << std::endl; + int downto = trail_user_lim.last(); + while(downto < trail.size()) { + Debug("minisat") << "== unassigning " << trail.last() << std::endl; + Var x = var(trail.last()); + if(intro_level(x) != -1) {// might be unregistered + assigns [x] = l_Undef; + vardata[x].trail_index = -1; + polarity[x] = sign(trail.last()); + insertVarOrder(x); + } + trail.pop(); + } + qhead = trail.size(); + Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", should be at " << trail_user_lim.last() << std::endl; + assert(trail_user_lim.last() == qhead); + trail_user_lim.pop(); + // Unset any units learned or added at this level Debug("minisat") << "in user pop, unsetting level units for level " << assertionLevel << std::endl; while(trail_user.last() != lit_Undef) { diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 426268b4b..c0dd00166 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -191,6 +191,10 @@ public: int nVars () const; // The current number of variables. int nFreeVars () const; + // Debugging SMT explanations + // + bool properExplanation(Lit l, Lit expl) const; // returns true if expl can be used to explain l---i.e., both assigned and trail_index(expl) < trail_index(l) + // Resource contraints: // void setConfBudget(int64_t x); @@ -282,6 +286,7 @@ protected: vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made. vec<int> trail_lim; // Separator indices for different decision levels in 'trail'. vec<Lit> trail_user; // Stack of assignments to UNdo on user pop. + vec<int> trail_user_lim; // Separator indices for different user levels in 'trail'. vec<bool> trail_ok; // Stack of "whether we're in conflict" flags. vec<VarData> vardata; // Stores reason and level for each variable. int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). @@ -462,6 +467,7 @@ inline int Solver::nClauses () const { return clauses_persisten inline int Solver::nLearnts () const { return clauses_removable.size(); } inline int Solver::nVars () const { return vardata.size(); } inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); } +inline bool Solver::properExplanation(Lit l, Lit expl) const { return value(l) == l_True && value(expl) == l_True && trail_index(var(expl)) < trail_index(var(l)); } inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; } inline void Solver::setDecisionVar(Var v, bool b) { diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 7d0353122..2538e6d0c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -232,6 +232,10 @@ void PropEngine::pop() { Debug("prop") << "pop()" << endl; } +bool PropEngine::isRunning() const { + return d_inCheckSat; +} + void PropEngine::interrupt() throw(ModalException) { if(! d_inCheckSat) { throw ModalException("SAT solver is not currently solving anything; " @@ -247,5 +251,49 @@ void PropEngine::spendResource() throw() { // TODO implement me } +bool PropEngine::properExplanation(TNode node, TNode expl) const { + if(! d_cnfStream->hasLiteral(node)) { + Trace("properExplanation") << "properExplanation(): Failing because node " + << "being explained doesn't have a SAT literal ?!" << std::endl + << "properExplanation(): The node is: " << node << std::endl; + return false; + } + + SatLiteral nodeLit = d_cnfStream->getLiteral(node); + + for(TNode::kinded_iterator i = expl.begin(kind::AND), + i_end = expl.end(kind::AND); + i != i_end; + ++i) { + if(! d_cnfStream->hasLiteral(*i)) { + Trace("properExplanation") << "properExplanation(): Failing because one of explanation " + << "nodes doesn't have a SAT literal" << std::endl + << "properExplanation(): The explanation node is: " << *i << std::endl; + return false; + } + + SatLiteral iLit = d_cnfStream->getLiteral(*i); + + if(iLit == nodeLit) { + Trace("properExplanation") << "properExplanation(): Failing because the node" << std::endl + << "properExplanation(): " << node << std::endl + << "properExplanation(): cannot be made to explain itself!" << std::endl; + return false; + } + + if(! d_satSolver->properExplanation(nodeLit, iLit)) { + Trace("properExplanation") << "properExplanation(): SAT solver told us that node" << std::endl + << "properExplanation(): " << *i << std::endl + << "properExplanation(): is not part of a proper explanation node for" << std::endl + << "properExplanation(): " << node << std::endl + << "properExplanation(): Perhaps it one of the two isn't assigned or the explanation" << std::endl + << "properExplanation(): node wasn't propagated before the node being explained" << std::endl; + return false; + } + } + + return true; +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 4f83888fc..91b9a61e6 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -242,6 +242,12 @@ public: void pop(); /** + * Return true if we are currently searching (either in this or + * another thread). + */ + bool isRunning() const; + + /** * Check the current time budget. */ void checkTime(); @@ -258,11 +264,23 @@ public: */ void spendResource() throw(); + /** + * For debugging. Return true if "expl" is a well-formed + * explanation for "node," meaning: + * + * 1. expl is either a SAT literal or an AND of SAT literals + * currently assigned true; + * 2. node is assigned true; + * 3. node does not appear in expl; and + * 4. node was assigned after all of the literals in expl + */ + bool properExplanation(TNode node, TNode expl) const; + };/* class PropEngine */ inline void SatTimer::check() { - if(expired()) { + if(d_propEngine.isRunning() && expired()) { Trace("limit") << "SatTimer::check(): interrupt!" << std::endl; d_propEngine.interrupt(); } diff --git a/src/prop/sat.h b/src/prop/sat.h index a6bdcb309..14b42e445 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -49,6 +49,30 @@ class PropEngine; class CnfStream; /* Definitions of abstract types and conversion functions for SAT interface */ +/* +inline SatLiteral variableToLiteral(SatVariable var) { + return Minisat::mkLit(var); +} + +inline bool literalSign(SatLiteral lit) { + return Minisat::sign(lit); +} + +static inline size_t +hashSatLiteral(const SatLiteral& literal) { + return (size_t) Minisat::toInt(literal); +} + +inline std::string stringOfLiteralValue(SatLiteralValue val) { + if( val == l_False ) { + return "0"; + } else if (val == l_True ) { + return "1"; + } else { // unknown + return "_"; + } +} +*/ /** * The proxy class that allows the SatSolver to communicate with the theories diff --git a/src/prop/sat_module.cpp b/src/prop/sat_module.cpp index 9391acbe5..db911f488 100644 --- a/src/prop/sat_module.cpp +++ b/src/prop/sat_module.cpp @@ -383,6 +383,9 @@ SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){ return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); } +bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const { + return true; +} /** Incremental interface */ diff --git a/src/prop/sat_module.h b/src/prop/sat_module.h index 320dfe09b..9c49c7d67 100644 --- a/src/prop/sat_module.h +++ b/src/prop/sat_module.h @@ -152,6 +152,8 @@ public: virtual void pop() = 0; + virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0; + }; // toodo add ifdef @@ -179,11 +181,11 @@ public: SatLiteralValue value(SatLiteral l); SatLiteralValue modelValue(SatLiteral l); - void unregisterVar(SatLiteral lit); void renewVar(SatLiteral lit, int level = -1); int getAssertionLevel() const; + // helper methods for converting from the internal Minisat representation static SatVariable toSatVariable(BVMinisat::Var var); @@ -254,6 +256,8 @@ public: SatLiteralValue modelValue(SatLiteral l); + bool properExplanation(SatLiteral lit, SatLiteral expl) const; + /** Incremental interface */ int getAssertionLevel() const; |