From 7719c492e69e22f9bdf0ce84ecc41ba0a4423aee Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 22 Feb 2012 20:08:57 +0000 Subject: Added OutputChannel::propagateAsDecision() functionality, allowing a theory to request a decision on a literal. All these theory requests are kept in a context-dependent queue and serviced in order when the SAT solver goes to make a decision. Requests that don't have a SAT literal give an assert-fail. Requests for literals that already have an assignment are silently ignored. Since the queue is CD, requests can actually be serviced more than once (e.g., if a request is made at DL 5, but not serviced until DL 10, and later, a conflict backtracks to level 7, the request may be serviced again). Performance impact: none to negligible for theories that don't use it See http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3620&reference_id=3614&mode=&category=&p=0 --- src/prop/minisat/core/Solver.cc | 18 +++++++- src/prop/sat.cpp | 5 +++ src/prop/sat.h | 2 + src/theory/output_channel.h | 18 ++++++++ src/theory/theory_engine.cpp | 15 ++++++- src/theory/theory_engine.h | 79 ++++++++++++++++++++++++++-------- src/theory/theory_test_utils.h | 7 +++ test/unit/theory/theory_black.h | 5 +++ test/unit/theory/theory_engine_white.h | 3 ++ 9 files changed, 132 insertions(+), 20 deletions(-) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index e1a8ded8e..cdab47163 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -355,13 +355,27 @@ void Solver::popTrail() { Lit Solver::pickBranchLit() { + Lit nextLit; + #ifdef CVC4_REPLAY - Lit nextLit = proxy->getNextReplayDecision(); + nextLit = proxy->getNextReplayDecision(); if (nextLit != lit_Undef) { return nextLit; } #endif /* CVC4_REPLAY */ + // Theory requests + nextLit = proxy->getNextDecisionRequest(); + while (nextLit != lit_Undef) { + if(value(var(nextLit)) == l_Undef) { + Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl; + return nextLit; + } else { + Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl; + } + nextLit = proxy->getNextDecisionRequest(); + } + Var next = var_Undef; // Random decision: @@ -699,6 +713,7 @@ void Solver::propagateTheory() { std::vector propagatedLiterals; proxy->theoryPropagate(propagatedLiterals); int oldTrailSize = trail.size(); + Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl; for (unsigned i = 0, i_end = propagatedLiterals.size(); i < i_end; ++ i) { Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl; // multiple theories can propagate the same literal @@ -707,6 +722,7 @@ void Solver::propagateTheory() { uncheckedEnqueue(p, CRef_Lazy); } else { // but we check that this is the case and that they agree + Debug("minisat") << "trail_index(var(p)) == " << trail_index(var(p)) << std::endl; Assert(trail_index(var(p)) >= oldTrailSize); Assert(value(p) == lbool(!sign(p))); } diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 7df7535dd..559467922 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -71,6 +71,11 @@ void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) { d_theoryEngine->assertFact(literalNode); } +SatLiteral SatSolver::getNextDecisionRequest() { + TNode n = d_theoryEngine->getNextDecisionRequest(); + return n.isNull() ? Minisat::lit_Undef : d_cnfStream->getLiteral(n); +} + bool SatSolver::theoryNeedCheck() const { return d_theoryEngine->needCheck(); } diff --git a/src/prop/sat.h b/src/prop/sat.h index e86443827..3f3166c14 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -236,6 +236,8 @@ public: void enqueueTheoryLiteral(const SatLiteral& l); + SatLiteral getNextDecisionRequest(); + bool theoryNeedCheck() const; void setCnfStream(CnfStream* cnfStream); diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 0e47cd7f2..71bbefb6a 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -106,6 +106,24 @@ public: */ virtual void propagate(TNode n) throw(AssertionException) = 0; + /** + * Request that the core make a decision on this atom. The decision + * will be "as soon as possible," but due to other propagation and + * conflict-detection work going on internally, the request is queued + * up and may be behind other such requests. The request will be + * silently dropped if the atom has a definite value at the point the + * request would be serviced. This request is also context-dependent + * on the search context, meaning that it will be dropped completely + * if a conflict is found before it is serviced. Each request will only + * be serviced a single time, even though the atom may become undefined + * due to backtracking. + * + * @param atom the atom to decide upon (or the negation of an + * atom---the decision will be in the phase provided); must be + * associated to a SAT literal. + */ + virtual void propagateAsDecision(TNode n) throw(AssertionException) = 0; + /** * Tell the core that a valid theory lemma at decision level 0 has * been detected. (This requests a split.) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 75c64654d..c4a8dc591 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -55,6 +55,8 @@ TheoryEngine::TheoryEngine(context::Context* context, d_logic(""), d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), + d_decisionRequests(context), + d_decisionRequestsIndex(context, 0), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms) { @@ -665,13 +667,22 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { } } +void TheoryEngine::propagateAsDecision(TNode literal, theory::TheoryId theory) { + Debug("theory") << "EngineOutputChannel::propagateAsDecision(" << literal << ", " << theory << ")" << std::endl; + + d_propEngine->checkTime(); + + Assert(d_propEngine->isSatLiteral(literal.getKind() == kind::NOT ? literal[0] : literal), "OutputChannel::propagateAsDecision() requires a SAT literal (or negation of one)"); + + d_decisionRequests.push_back(literal); +} + theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { Assert(a.getType() == b.getType()); return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b); } -Node TheoryEngine::getExplanation(TNode node) -{ +Node TheoryEngine::getExplanation(TNode node) { Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl; TNode atom = node.getKind() == kind::NOT ? node[0] : node; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 6385d1467..be1c3abaf 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -57,14 +57,14 @@ struct NodeTheoryPair { bool operator == (const NodeTheoryPair& pair) const { return node == pair.node && theory == pair.theory; } -}; +};/* struct NodeTheoryPair */ struct NodeTheoryPairHashFunction { NodeHashFunction hashFunction; size_t operator()(const NodeTheoryPair& pair) const { return hashFunction(pair.node)*0x9e3779b9 + pair.theory; } -}; +};/* struct NodeTheoryPairHashFunction */ /** * This is essentially an abstraction for a collection of theories. A @@ -128,7 +128,9 @@ class TheoryEngine { */ class Statistics { - static std::string mkName(std::string prefix, theory::TheoryId theory, std::string suffix) { + static std::string mkName(std::string prefix, + theory::TheoryId theory, + std::string suffix) { std::stringstream ss; ss << prefix << theory << suffix; return ss.str(); @@ -136,22 +138,25 @@ class TheoryEngine { public: - IntStat conflicts, propagations, lemmas; + IntStat conflicts, propagations, lemmas, propagationsAsDecisions; Statistics(theory::TheoryId theory): conflicts(mkName("theory<", theory, ">::conflicts"), 0), propagations(mkName("theory<", theory, ">::propagations"), 0), - lemmas(mkName("theory<", theory, ">::lemmas"), 0) + lemmas(mkName("theory<", theory, ">::lemmas"), 0), + propagationsAsDecisions(mkName("theory<", theory, ">::propagationsAsDecisions"), 0) { StatisticsRegistry::registerStat(&conflicts); StatisticsRegistry::registerStat(&propagations); StatisticsRegistry::registerStat(&lemmas); + StatisticsRegistry::registerStat(&propagationsAsDecisions); } ~Statistics() { StatisticsRegistry::unregisterStat(&conflicts); StatisticsRegistry::unregisterStat(&propagations); StatisticsRegistry::unregisterStat(&lemmas); + StatisticsRegistry::unregisterStat(&propagationsAsDecisions); } };/* class TheoryEngine::Statistics */ @@ -202,6 +207,13 @@ class TheoryEngine { d_engine->propagate(literal, d_theory); } + void propagateAsDecision(TNode literal) throw(AssertionException) { + Trace("theory") << "EngineOutputChannel<" << d_theory << ">::propagateAsDecision(" << literal << ")" << std::endl; + ++ d_statistics.propagationsAsDecisions; + d_engine->d_outputChannelUsed = true; + d_engine->propagateAsDecision(literal, d_theory); + } + theory::LemmaStatus lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { Trace("theory") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; @@ -217,7 +229,7 @@ class TheoryEngine { d_engine->spendResource(); } - };/* class EngineOutputChannel */ + };/* class TheoryEngine::EngineOutputChannel */ /** * Output channels for individual theories. @@ -235,8 +247,9 @@ class TheoryEngine { context::CDO d_sharedTermsExist; /** - * Explain the equality literals and push all the explaining literals into the builder. All - * the non-equality literals are pushed to the builder. + * Explain the equality literals and push all the explaining literals + * into the builder. All the non-equality literals are pushed to the + * builder. */ void explainEqualities(theory::TheoryId theoryId, TNode literals, NodeBuilder<>& builder); @@ -288,18 +301,18 @@ class TheoryEngine { NodeTheoryPair toAssert; /** This is the node/theory pair that we will use to explain it */ NodeTheoryPair toExplain; - + SharedEquality(TNode assertion, TNode original, theory::TheoryId sendingTheory, theory::TheoryId receivingTheory) : toAssert(assertion, receivingTheory), toExplain(original, sendingTheory) { } - }; - + };/* struct SharedEquality */ + /** - * Map from equalities asserted to a theory, to the theory that can explain them. + * Map from equalities asserted to a theory, to the theory that can explain them. */ typedef context::CDMap SharedAssertionsMap; - + /** * A map from asserted facts to where they came from (for explanations). */ @@ -316,7 +329,7 @@ class TheoryEngine { /** * Literals that are propagated by the theory. Note that these are TNodes. * The theory can only propagate nodes that have an assigned literal in the - * sat solver and are hence referenced in the SAT solver. + * SAT solver and are hence referenced in the SAT solver. */ context::CDList d_propagatedLiterals; @@ -330,6 +343,19 @@ class TheoryEngine { */ std::vector d_propagatedEqualities; + /** + * Decisions that are requested via propagateAsDecision(). The theory + * can only request decisions on nodes that have an assigned litearl in + * the SAT solver and are hence referenced in the SAT solver (making the + * use of TNode safe). + */ + context::CDList d_decisionRequests; + + /** + * The index of the next decision requested by a theory. + */ + context::CDO d_decisionRequestsIndex; + /** * Called by the output channel to propagate literals and facts */ @@ -341,6 +367,12 @@ class TheoryEngine { */ void propagate(theory::Theory::Effort effort); + /** + * Called by the output channel to request decisions "as soon as + * possible." + */ + void propagateAsDecision(TNode literal, theory::TheoryId theory); + /** * A variable to mark if we added any lemmas. */ @@ -541,6 +573,19 @@ public: } } + TNode getNextDecisionRequest() { + if(d_decisionRequestsIndex < d_decisionRequests.size()) { + TNode req = d_decisionRequests[d_decisionRequestsIndex]; + Debug("propagateAsDecision") << "TheoryEngine requesting decision[" + << d_decisionRequestsIndex << "]: " + << req << std::endl; + d_decisionRequestsIndex = d_decisionRequestsIndex + 1; + return req; + } else { + return TNode::null(); + } + } + bool properConflict(TNode conflict) const; bool properPropagation(TNode lit) const; bool properExplanation(TNode node, TNode expl) const; @@ -572,8 +617,8 @@ public: } /** - * Returns the equality status of the two terms, from the theory that owns the domain type. - * The types of a and b must be the same. + * Returns the equality status of the two terms, from the theory + * that owns the domain type. The types of a and b must be the same. */ theory::EqualityStatus getEqualityStatus(TNode a, TNode b); @@ -583,7 +628,7 @@ private: PreRegisterVisitor d_preRegistrationVisitor; /** Visitor for collecting shared terms */ - SharedTermsVisitor d_sharedTermsVisitor; + SharedTermsVisitor d_sharedTermsVisitor; };/* class TheoryEngine */ diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 96bd02b5a..aaf47425b 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -41,6 +41,7 @@ namespace theory { enum OutputChannelCallType { CONFLICT, PROPAGATE, + PROPAGATE_AS_DECISION, AUG_LEMMA, LEMMA, EXPLANATION @@ -52,6 +53,7 @@ inline std::ostream& operator<<(std::ostream& out, theory::OutputChannelCallType switch(type) { case theory::CONFLICT: return out << "CONFLICT"; case theory::PROPAGATE: return out << "PROPAGATE"; + case theory::PROPAGATE_AS_DECISION: return out << "PROPAGATE_AS_DECISION"; case theory::AUG_LEMMA: return out << "AUG_LEMMA"; case theory::LEMMA: return out << "LEMMA"; case theory::EXPLANATION: return out << "EXPLANATION"; @@ -81,6 +83,11 @@ public: push(PROPAGATE, n); } + void propagateAsDecision(TNode n) + throw(AssertionException) { + push(PROPAGATE_AS_DECISION, n); + } + LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0); diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 60e090d16..76385219d 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -62,6 +62,11 @@ public: push(PROPAGATE, n); } + void propagateAsDecision(TNode n) + throw(AssertionException) { + // ignore + } + LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) { push(LEMMA, n); diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 2363e4906..8d7bc9c72 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -54,6 +54,9 @@ class FakeOutputChannel : public OutputChannel { void propagate(TNode n) throw(AssertionException) { Unimplemented(); } + void propagateAsDecision(TNode n) throw(AssertionException) { + Unimplemented(); + } LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) { Unimplemented(); } -- cgit v1.2.3