diff options
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 79 |
1 files changed, 62 insertions, 17 deletions
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<bool> 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<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> 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<TNode> d_propagatedLiterals; @@ -331,6 +344,19 @@ class TheoryEngine { std::vector<SharedEquality> 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<TNode> d_decisionRequests; + + /** + * The index of the next decision requested by a theory. + */ + context::CDO<unsigned> d_decisionRequestsIndex; + + /** * Called by the output channel to propagate literals and facts */ void propagate(TNode literal, theory::TheoryId theory); @@ -342,6 +368,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. */ bool d_lemmasAdded; @@ -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 */ |