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/theory/theory_engine.h | 79 ++++++++++++++++++++++++++++++++++++---------- 1 file changed, 62 insertions(+), 17 deletions(-) (limited to 'src/theory/theory_engine.h') 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 */ -- cgit v1.2.3