diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-29 20:53:47 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-29 20:53:47 +0000 |
commit | e792bb8628ea7010fa9c452bf1aa7ba1b60291a3 (patch) | |
tree | ddc12f92092627b7aee2a63dca8dd66279b2970e /src/prop | |
parent | e7e9c10006b5b243a73832ed97c5dec79df6c90a (diff) |
Merging the unate-propagator branch into the trunk. This is a big update so expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 41 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 36 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.C | 111 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 23 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.C | 6 | ||||
-rw-r--r-- | src/prop/sat.cpp | 45 | ||||
-rw-r--r-- | src/prop/sat.h | 14 |
7 files changed, 214 insertions, 62 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 45f7ab398..9136a73c3 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -102,26 +102,10 @@ Node CnfStream::getNode(const SatLiteral& literal) { return 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; - Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; - return literal; -} - -const CnfStream::NodeCache& CnfStream::getNodeCache() const { - return d_nodeCache; -} - -const CnfStream::TranslationCache& CnfStream::getTranslationCache() const { - return d_translationCache; -} - -SatLiteral TseitinCnfStream::handleAtom(TNode node) { +SatLiteral CnfStream::convertAtom(TNode node) { Assert(!isCached(node), "atom already mapped!"); - Debug("cnf") << "handleAtom(" << node << ")" << endl; + Debug("cnf") << "convertAtom(" << node << ")" << endl; bool theoryLiteral = node.getKind() != kind::VARIABLE; SatLiteral lit = newLiteral(node, theoryLiteral); @@ -137,6 +121,23 @@ SatLiteral TseitinCnfStream::handleAtom(TNode node) { return lit; } +SatLiteral CnfStream::getLiteral(TNode node, bool create /* = false */) { + TranslationCache::iterator find = d_translationCache.find(node); + SatLiteral literal; + if(create) { + if(find == d_translationCache.end()) { + literal = convertAtom(node); + } else { + literal = find->second; + } + } else { + Assert(find != d_translationCache.end(), "Literal not in the CNF Cache"); + literal = find->second; + } + Debug("cnf") << "CnfStream::getLiteral(" << node << ", create = " << create << ") => " << literal << std::endl; + return literal; +} + SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { Assert(!isCached(xorNode), "Atom already mapped!"); Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!"); @@ -366,10 +367,10 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { default: { //TODO make sure this does not contain any boolean substructure - nodeLit = handleAtom(node); + nodeLit = convertAtom(node); //Unreachable(); //Node atomic = handleNonAtomicNode(node); - //return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic); + //return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic); } } } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index abb69f590..ba87cf269 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -127,6 +127,16 @@ protected: */ SatLiteral newLiteral(TNode node, bool theoryLiteral = false); + /** + * Constructs a new literal for an atom and returns it. Calls + * newLiteral(). + * + * @param node the node to convert; there should be no boolean + * structure in this expression. Assumed to not be in the + * translation cache. + */ + SatLiteral convertAtom(TNode node); + public: /** @@ -161,14 +171,25 @@ public: /** * Returns the literal that represents the given node in the SAT CNF - * representation. [Presumably there are some constraints on the kind - * of node? E.g., it needs to be a boolean? -Chris] - * + * representation. + * @param node [Presumably there are some constraints on the kind of + * node? E.g., it needs to be a boolean? -Chris] + * @param create Controls whether or not to create a new SAT literal + * mapping for Node if it does not exist. This exists to break + * circular dependencies, where an atom is converted and asserted to + * the SAT solver, which propagates it immediately since it's a + * unit, which can theory-propagate additional literals that don't + * yet have a SAT literal mapping. */ - SatLiteral getLiteral(TNode node); + SatLiteral getLiteral(TNode node, bool create = false); + + const TranslationCache& getTranslationCache() const { + return d_translationCache; + } - const TranslationCache& getTranslationCache() const; - const NodeCache& getNodeCache() const; + const NodeCache& getNodeCache() const { + return d_nodeCache; + } }; /* class CnfStream */ /** @@ -178,7 +199,7 @@ public: * will be equivalent to each subexpression in the constructed equi-satisfiable * formula, then substitute the new literal for the formula, and so on, * recursively. - * + * * This implementation does this in a single recursive pass. [??? -Chris] */ class TseitinCnfStream : public CnfStream { @@ -211,7 +232,6 @@ private: // - returning l // // handleX( n ) can assume that n is not in d_translationCache - SatLiteral handleAtom(TNode node); SatLiteral handleNot(TNode node); SatLiteral handleXor(TNode node); SatLiteral handleImplies(TNode node); diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C index 8533e191b..1667af20d 100644 --- a/src/prop/minisat/core/Solver.C +++ b/src/prop/minisat/core/Solver.C @@ -29,6 +29,28 @@ namespace CVC4 { namespace prop { namespace minisat { +Clause* Solver::lazy_reason = reinterpret_cast<Clause*>(1); + +Clause* Solver::getReason(Lit l) +{ + if (reason[var(l)] != lazy_reason) return reason[var(l)]; + // Get the explanation from the theory + SatClause explanation; + if (value(l) == l_True) { + proxy->explainPropagation(l, explanation); + assert(explanation[0] == l); + } else { + proxy->explainPropagation(~l, explanation); + assert(explanation[0] == ~l); + } + Clause* real_reason = Clause_new(explanation, true); + reason[var(l)] = real_reason; + // Add it to the database + learnts.push(real_reason); + attachClause(*real_reason); + return real_reason; +} + Solver::Solver(SatSolver* proxy, context::Context* context) : // SMT stuff @@ -122,7 +144,7 @@ bool Solver::addClause(vec<Lit>& ps, ClauseType type) assert(type != CLAUSE_LEMMA); assert(value(ps[0]) == l_Undef); uncheckedEnqueue(ps[0]); - return ok = (propagate() == NULL); + return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == NULL); }else{ Clause* c = Clause_new(ps, false); clauses.push(c); @@ -282,7 +304,7 @@ void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel) // Select next clause to look at: while (!seen[var(trail[index--])]); p = trail[index+1]; - confl = reason[var(p)]; + confl = getReason(p); seen[var(p)] = 0; pathC--; @@ -299,12 +321,12 @@ void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel) out_learnt.copyTo(analyze_toclear); for (i = j = 1; i < out_learnt.size(); i++) - if (reason[var(out_learnt[i])] == NULL || !litRedundant(out_learnt[i], abstract_level)) + if (getReason(out_learnt[i]) == NULL || !litRedundant(out_learnt[i], abstract_level)) out_learnt[j++] = out_learnt[i]; }else{ out_learnt.copyTo(analyze_toclear); for (i = j = 1; i < out_learnt.size(); i++){ - Clause& c = *reason[var(out_learnt[i])]; + Clause& c = *getReason(out_learnt[i]); for (int k = 1; k < c.size(); k++) if (!seen[var(c[k])] && level[var(c[k])] > 0){ out_learnt[j++] = out_learnt[i]; @@ -342,13 +364,13 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) analyze_stack.clear(); analyze_stack.push(p); int top = analyze_toclear.size(); while (analyze_stack.size() > 0){ - assert(reason[var(analyze_stack.last())] != NULL); + assert(getReason(analyze_stack.last()) != NULL); Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop(); for (int i = 1; i < c.size(); i++){ Lit p = c[i]; if (!seen[var(p)] && level[var(p)] > 0){ - if (reason[var(p)] != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){ + if (getReason(p) != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){ seen[var(p)] = 1; analyze_stack.push(p); analyze_toclear.push(p); @@ -415,42 +437,74 @@ void Solver::uncheckedEnqueue(Lit p, Clause* from) polarity [var(p)] = sign(p); trail.push(p); - if (theory[var(p)]) { + if (theory[var(p)] && from != lazy_reason) { // Enqueue to the theory proxy->enqueueTheoryLiteral(p); } } -Clause* Solver::propagate() +Clause* Solver::propagate(TheoryCheckType type) { Clause* confl = NULL; - while(qhead < trail.size()) { - confl = propagateBool(); - if (confl != NULL) break; - confl = propagateTheory(); - if (confl != NULL) break; + // If this is the final check, no need for Boolean propagation and + // theory propagation + if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) { + return theoryCheck(theory::Theory::FULL_EFFORT); } + // The effort we will be using to theory check + theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ? + theory::Theory::QUICK_CHECK : theory::Theory::STANDARD; + + // Keep running until we have checked everything, we + // have no conflict and no new literals have been asserted + bool new_assertions; + do { + new_assertions = false; + while(qhead < trail.size()) { + confl = propagateBool(); + if (confl != NULL) break; + confl = theoryCheck(effort); + if (confl != NULL) break; + } + + if (confl == NULL && type == CHECK_WITH_PROPAGATION_STANDARD) { + new_assertions = propagateTheory(); + if (!new_assertions) break; + } + } while (new_assertions); + return confl; } +bool Solver::propagateTheory() { + std::vector<Lit> propagatedLiterals; + proxy->theoryPropagate(propagatedLiterals); + const unsigned i_end = propagatedLiterals.size(); + for (unsigned i = 0; i < i_end; ++ i) { + uncheckedEnqueue(propagatedLiterals[i], lazy_reason); + } + proxy->clearPropagatedLiterals(); + return propagatedLiterals.size() > 0; +} + /*_________________________________________________________________________________________________ | -| propagateTheory : [void] -> [Clause*] +| theoryCheck: [void] -> [Clause*] | | Description: -| Propagates all enqueued theory facts. If a conflict arises, the conflicting clause is returned, -| otherwise NULL. +| Checks all enqueued theory facts for satisfiability. If a conflict arises, the conflicting +| clause is returned, otherwise NULL. | | Note: the propagation queue might be NOT empty |________________________________________________________________________________________________@*/ -Clause* Solver::propagateTheory() +Clause* Solver::theoryCheck(theory::Theory::Effort effort) { Clause* c = NULL; SatClause clause; - proxy->theoryCheck(clause); + proxy->theoryCheck(effort, clause); int clause_size = clause.size(); Assert(clause_size != 1, "Can't handle unit clause explanations"); if(clause_size > 0) { @@ -598,7 +652,7 @@ bool Solver::simplify() { assert(decisionLevel() == 0); - if (!ok || propagate() != NULL) + if (!ok || propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL) return ok = false; if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) @@ -643,9 +697,9 @@ lbool Solver::search(int nof_conflicts, int nof_learnts) starts++; bool first = true; - + TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD; for (;;){ - Clause* confl = propagate(); + Clause* confl = propagate(check_type); if (confl != NULL){ // CONFLICT conflicts++; conflictC++; @@ -671,9 +725,16 @@ lbool Solver::search(int nof_conflicts, int nof_learnts) varDecayActivity(); claDecayActivity(); + // We have a conflict so, we are going back to standard checks + check_type = CHECK_WITH_PROPAGATION_STANDARD; + }else{ // NO CONFLICT + // If this was a final check, we are satisfiable + if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) + return l_True; + if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ // Reached bound on number of conflicts: progress_estimate = progressEstimate(); @@ -709,9 +770,11 @@ lbool Solver::search(int nof_conflicts, int nof_learnts) decisions++; next = pickBranchLit(polarity_mode, random_var_freq); - if (next == lit_Undef) - // Model found: - return l_True; + if (next == lit_Undef) { + // We need to do a full theory check to confirm + check_type = CHECK_WITHOUTH_PROPAGATION_FINAL; + continue; + } } // Increase decision level and enqueue 'next' diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 312fe44d5..2e44803e9 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define __CVC4__PROP__MINISAT__SOLVER_H #include "context/context.h" +#include "theory/theory.h" #include <cstdio> #include <cassert> @@ -161,7 +162,11 @@ protected: vec<int> trail_lim; // Separator indices for different decision levels in 'trail'. vec<Clause*> lemmas; // List of lemmas we added (context dependent) vec<int> lemmas_lim; // Separator indices for different decision levels in 'lemmas'. - vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. + static Clause* lazy_reason; // The mark when we need to ask the theory engine for a reason + vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, lazy_reason if theory propagated, or 'NULL' if none. + + Clause* getReason(Lit l); // Returns the reason, or asks the theory for an explanation + vec<int> 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) @@ -181,6 +186,15 @@ protected: vec<Lit> analyze_toclear; vec<Lit> add_tmp; + enum TheoryCheckType { + // Quick check, but don't perform theory propagation + CHECK_WITHOUTH_PROPAGATION_QUICK, + // Check and perform theory propagation + CHECK_WITH_PROPAGATION_STANDARD, + // The SAT problem is satisfiable, perform a full theory check + CHECK_WITHOUTH_PROPAGATION_FINAL + }; + // Main internal methods: // void insertVarOrder (Var x); // Insert a variable in the decision order priority queue. @@ -188,9 +202,10 @@ protected: void newDecisionLevel (); // Begins a new decision level. void uncheckedEnqueue (Lit p, Clause* from = NULL); // Enqueue a literal. Assumes value of literal is undefined. bool enqueue (Lit p, Clause* from = NULL); // Test if fact 'p' contradicts current state, enqueue otherwise. - Clause* propagate (); // Perform Boolean and Theory. Returns possibly conflicting clause. + Clause* propagate (TheoryCheckType type); // Perform Boolean and Theory. Returns possibly conflicting clause. Clause* propagateBool (); // Perform Boolean propagation. Returns possibly conflicting clause. - Clause* propagateTheory (); // Perform Theory propagation. Returns possibly conflicting clause. + bool propagateTheory (); // Perform Theory propagation. Return true if any literals were asserted. + Clause* theoryCheck (theory::Theory::Effort effort); // Perform a theory satisfiability check. Returns possibly conflicting clause. void cancelUntil (int level); // Backtrack until a certain level. void analyze (Clause* 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? @@ -216,7 +231,7 @@ protected: // Misc: // - int decisionLevel () const; // Gives the current decisionlevel. + int decisionLevel () const; // Gives the current decision level. uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels. double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C index 9aad6aea7..00f93402f 100644 --- a/src/prop/minisat/simp/SimpSolver.C +++ b/src/prop/minisat/simp/SimpSolver.C @@ -212,7 +212,7 @@ bool SimpSolver::strengthenClause(Clause& c, Lit l) updateElimHeap(var(l)); } - return c.size() == 1 ? enqueue(c[0]) && propagate() == NULL : true; + return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == NULL : true; } @@ -312,7 +312,7 @@ bool SimpSolver::implied(const vec<Lit>& c) uncheckedEnqueue(~c[i]); } - bool result = propagate() != NULL; + bool result = propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL; cancelUntil(0); return result; } @@ -394,7 +394,7 @@ bool SimpSolver::asymm(Var v, Clause& c) else l = c[i]; - if (propagate() != NULL){ + if (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL){ cancelUntil(0); asymm_lits++; if (!strengthenClause(c, l)) diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 207bda4db..a7b536a57 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -26,9 +26,9 @@ namespace CVC4 { namespace prop { -void SatSolver::theoryCheck(SatClause& conflict) { +void SatSolver::theoryCheck(theory::Theory::Effort effort, SatClause& conflict) { // Try theory propagation - bool ok = d_theoryEngine->check(theory::Theory::FULL_EFFORT); + bool ok = d_theoryEngine->check(effort); // If in conflict construct the conflict clause if (!ok) { // We have a conflict, get it @@ -47,6 +47,47 @@ void SatSolver::theoryCheck(SatClause& conflict) { } } +void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) { + // Propagate + d_theoryEngine->propagate(); + // Get the propagated literals + const std::vector<TNode>& outputNodes = d_theoryEngine->getPropagatedLiterals(); + // If any literals, make a clause + const unsigned i_end = outputNodes.size(); + for (unsigned i = 0; i < i_end; ++ i) { + Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << endl; + // The second argument ("true") instructs the CNF stream to create + // a new literal mapping if it doesn't exist. This can happen due + // to a circular dependence, if a SAT literal "a" is asserted as a + // unit to the SAT solver, a round of theory propagation can occur + // before all Nodes have SAT variable mappings. + SatLiteral l = d_cnfStream->getLiteral(outputNodes[i], true); + output.push_back(l); + } +} + +void SatSolver::explainPropagation(SatLiteral l, SatClause& explanation) { + TNode lNode = d_cnfStream->getNode(l); + Debug("prop-explain") << "explainPropagation(" << lNode.toString() << ")" << endl; + Node theoryExplanation = d_theoryEngine->getExplanation(lNode); + Debug("prop-explain") << "explainPropagation() => " << theoryExplanation.toString() << endl; + if (lNode.getKind() == kind::AND) { + Node::const_iterator it = theoryExplanation.begin(); + Node::const_iterator it_end = theoryExplanation.end(); + explanation.push(l); + for (; it != it_end; ++ it) { + explanation.push(~d_cnfStream->getLiteral(*it)); + } + } else { + explanation.push(l); + explanation.push(~d_cnfStream->getLiteral(theoryExplanation)); + } +} + +void SatSolver::clearPropagatedLiterals() { + d_theoryEngine->clearPropagatedLiterals(); +} + void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) { Node literalNode = d_cnfStream->getNode(l); Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl; diff --git a/src/prop/sat.h b/src/prop/sat.h index f64697d7b..992d8ecd2 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -27,6 +27,7 @@ #include "util/options.h" #include "util/stats.h" +#include "theory/theory.h" #ifdef __CVC4_USE_MINISAT @@ -199,7 +200,13 @@ public: SatVariable newVar(bool theoryAtom = false); - void theoryCheck(SatClause& conflict); + void theoryCheck(theory::Theory::Effort effort, SatClause& conflict); + + void explainPropagation(SatLiteral l, SatClause& explanation); + + void theoryPropagate(std::vector<SatLiteral>& output); + + void clearPropagatedLiterals(); void enqueueTheoryLiteral(const SatLiteral& l); @@ -229,6 +236,11 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, // Make minisat reuse the literal values d_minisat->polarity_mode = minisat::SimpSolver::polarity_user; + // No random choices + if(debugTagIsOn("no_rnd_decisions")){ + d_minisat->random_var_freq = 0; + } + d_statistics.init(d_minisat); } |