diff options
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 8 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 7 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 10 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.cpp | 6 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.h | 2 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 6 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.h | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.cpp | 4 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.h | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 9 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 2 | ||||
-rw-r--r-- | src/theory/theory.cpp | 142 | ||||
-rw-r--r-- | src/theory/theory.h | 189 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 3 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 2 |
21 files changed, 290 insertions, 118 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 4e0582f50..ea751ca74 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -87,9 +87,7 @@ TrustNode TheoryArith::expandDefinition(Node node) return d_internal->expandDefinition(node); } -void TheoryArith::addSharedTerm(TNode n){ - d_internal->addSharedTerm(n); -} +void TheoryArith::notifySharedTerm(TNode n) { d_internal->addSharedTerm(n); } TrustNode TheoryArith::ppRewrite(TNode atom) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index d0147fe9f..bfe30db61 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -104,7 +104,7 @@ class TheoryArith : public Theory { EqualityStatus getEqualityStatus(TNode a, TNode b) override; - void addSharedTerm(TNode n) override; + void notifySharedTerm(TNode n) override; Node getModelValue(TNode var) override; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 34c4fd156..b4a234748 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -883,9 +883,11 @@ Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) { // SHARING ///////////////////////////////////////////////////////////////////////////// - -void TheoryArrays::addSharedTerm(TNode t) { - Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl; +void TheoryArrays::notifySharedTerm(TNode t) +{ + Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) + << "TheoryArrays::notifySharedTerm(" << t << ")" + << std::endl; d_equalityEngine->addTriggerTerm(t, THEORY_ARRAYS); if (t.getType().isArray()) { d_sharedArrays.insert(t); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index a1fa19631..8cbf826c1 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -251,7 +251,7 @@ class TheoryArrays : public Theory { void checkPair(TNode r1, TNode r2); public: - void addSharedTerm(TNode t) override; + void notifySharedTerm(TNode t) override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; void computeCareGraph() override; bool isShared(TNode t) diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index d03d81a3d..1696d6185 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -880,9 +880,10 @@ TrustNode TheoryBV::explain(TNode node) return TrustNode::mkTrustPropExp(node, explanation, nullptr); } - -void TheoryBV::addSharedTerm(TNode t) { - Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; +void TheoryBV::notifySharedTerm(TNode t) +{ + Debug("bitvector::sharing") + << indent() << "TheoryBV::notifySharedTerm(" << t << ")" << std::endl; d_sharedTermsSet.insert(t); if (options::bitvectorEqualitySolver()) { for (unsigned i = 0; i < d_subtheories.size(); ++i) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 65100f98f..c6e9282f4 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -244,7 +244,7 @@ class TheoryBV : public Theory { */ void explain(TNode literal, std::vector<TNode>& assumptions); - void addSharedTerm(TNode t) override; + void notifySharedTerm(TNode t) override; bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 65264bb3f..f85b79c53 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -727,11 +727,13 @@ TrustNode TheoryDatatypes::ppRewrite(TNode in) return TrustNode::null(); } -void TheoryDatatypes::addSharedTerm(TNode t) { - Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): " - << t << " " << t.getType().isBoolean() << endl; +void TheoryDatatypes::notifySharedTerm(TNode t) +{ + Debug("datatypes") << "TheoryDatatypes::notifySharedTerm(): " << t << " " + << t.getType().isBoolean() << endl; d_equalityEngine->addTriggerTerm(t, THEORY_DATATYPES); - Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl; + Debug("datatypes") << "TheoryDatatypes::notifySharedTerm() finished" + << std::endl; } bool TheoryDatatypes::propagateLit(TNode literal) diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 137aae469..6dd990b30 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -290,7 +290,7 @@ private: void preRegisterTerm(TNode n) override; TrustNode expandDefinition(Node n) override; TrustNode ppRewrite(TNode n) override; - void addSharedTerm(TNode t) override; + void notifySharedTerm(TNode t) override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; bool collectModelInfo(TheoryModel* m) override; void shutdown() override {} diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 82086aafe..0c5a92572 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -908,9 +908,10 @@ void TheoryFp::preRegisterTerm(TNode node) return; } -void TheoryFp::addSharedTerm(TNode node) { +void TheoryFp::notifySharedTerm(TNode node) +{ Trace("fp-addSharedTerm") - << "TheoryFp::addSharedTerm(): " << node << std::endl; + << "TheoryFp::notifySharedTerm(): " << node << std::endl; // A system-wide invariant; terms must be registered before they are shared Assert(isRegistered(node)); return; @@ -998,7 +999,6 @@ void TheoryFp::check(Effort level) { } // Resolve the abstractions for the conversion lemmas - // if (level == EFFORT_COMBINATION) { if (level == EFFORT_LAST_CALL) { Trace("fp") << "TheoryFp::check(): checking abstractions" << std::endl; diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index ad052f92a..79ece7bce 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -58,7 +58,7 @@ class TheoryFp : public Theory { TrustNode expandDefinition(Node node) override; void preRegisterTerm(TNode node) override; - void addSharedTerm(TNode node) override; + void notifySharedTerm(TNode node) override; TrustNode ppRewrite(TNode node) override; diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index cf3cf2f9a..0059d9f3a 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -160,9 +160,9 @@ TrustNode TheorySep::explain(TNode literal) // SHARING ///////////////////////////////////////////////////////////////////////////// - -void TheorySep::addSharedTerm(TNode t) { - Debug("sep") << "TheorySep::addSharedTerm(" << t << ")" << std::endl; +void TheorySep::notifySharedTerm(TNode t) +{ + Debug("sep") << "TheorySep::notifySharedTerm(" << t << ")" << std::endl; d_equalityEngine->addTriggerTerm(t, THEORY_SEP); } diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index bbb37a3a2..af411c64a 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -114,7 +114,7 @@ class TheorySep : public Theory { TrustNode explain(TNode n) override; public: - void addSharedTerm(TNode t) override; + void notifySharedTerm(TNode t) override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; void computeCareGraph() override; diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 647a7bb47..63ebacc23 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -88,9 +88,7 @@ void TheorySets::finishInit() d_internal->finishInit(); } -void TheorySets::addSharedTerm(TNode n) { - d_internal->addSharedTerm(n); -} +void TheorySets::notifySharedTerm(TNode n) { d_internal->addSharedTerm(n); } void TheorySets::check(Effort e) { if (done() && e < Theory::EFFORT_FULL) { diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 9e04b89a7..a7fb31dab 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -58,7 +58,7 @@ class TheorySets : public Theory void finishInit() override; //--------------------------------- end initialization - void addSharedTerm(TNode) override; + void notifySharedTerm(TNode) override; void check(Effort) override; bool collectModelInfo(TheoryModel* m) override; void computeCareGraph() override; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e42796354..0de0cc33c 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -153,15 +153,16 @@ bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { return false; } -void TheoryStrings::addSharedTerm(TNode t) { - Debug("strings") << "TheoryStrings::addSharedTerm(): " - << t << " " << t.getType().isBoolean() << endl; +void TheoryStrings::notifySharedTerm(TNode t) +{ + Debug("strings") << "TheoryStrings::notifySharedTerm(): " << t << " " + << t.getType().isBoolean() << endl; d_equalityEngine->addTriggerTerm(t, THEORY_STRINGS); if (options::stringExp()) { d_esolver.addSharedTerm(t); } - Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl; + Debug("strings") << "TheoryStrings::notifySharedTerm() finished" << std::endl; } EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) { diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 8a1afe6b3..f4aa0675c 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -96,7 +96,7 @@ class TheoryStrings : public Theory { /** shutdown */ void shutdown() override {} /** add shared term */ - void addSharedTerm(TNode n) override; + void notifySharedTerm(TNode n) override; /** get equality status */ EqualityStatus getEqualityStatus(TNode a, TNode b) override; /** preregister term */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 7220e2e1c..f65a7c45c 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -44,8 +44,6 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ os << "EFFORT_STANDARD"; break; case Theory::EFFORT_FULL: os << "EFFORT_FULL"; break; - case Theory::EFFORT_COMBINATION: - os << "EFFORT_COMBINATION"; break; case Theory::EFFORT_LAST_CALL: os << "EFFORT_LAST_CALL"; break; default: @@ -109,9 +107,11 @@ void Theory::setEqualityEngine(eq::EqualityEngine* ee) d_theoryState->setEqualityEngine(ee); } } + void Theory::setQuantifiersEngine(QuantifiersEngine* qe) { Assert(d_quantEngine == nullptr); + // quantifiers engine may be null if not in quantified logic d_quantEngine = qe; } @@ -266,11 +266,15 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node) return tid; } -void Theory::addSharedTermInternal(TNode n) { - Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl; - Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl; - d_sharedTerms.push_back(n); - addSharedTerm(n); +void Theory::notifySharedTerm(TNode n) +{ + // TODO (project #39): this will move to addSharedTerm, as every theory with + // an equality does this in their notifySharedTerm method. + // if we have an equality engine, add the trigger term + if (d_equalityEngine != nullptr) + { + d_equalityEngine->addTriggerTerm(n, d_id); + } } void Theory::computeCareGraph() { @@ -394,17 +398,23 @@ void Theory::computeRelevantTermsInternal(std::set<Node>& termSet, // Collect all terms appearing in assertions irrKinds.insert(kind::EQUAL); irrKinds.insert(kind::NOT); - context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end(); - for (; assert_it != assert_it_end; ++assert_it) { + context::CDList<Assertion>::const_iterator assert_it = facts_begin(), + assert_it_end = facts_end(); + for (; assert_it != assert_it_end; ++assert_it) + { collectTerms(*assert_it, irrKinds, termSet); } - if (!includeShared) return; - + if (!includeShared) + { + return; + } // Add terms that are shared terms - set<Kind> kempty; - context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(); - for (; shared_it != shared_it_end; ++shared_it) { + std::set<Kind> kempty; + context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), + shared_it_end = shared_terms_end(); + for (; shared_it != shared_it_end; ++shared_it) + { collectTerms(*shared_it, kempty, termSet); } } @@ -474,6 +484,110 @@ void Theory::getCareGraph(CareGraph* careGraph) { d_careGraph = NULL; } +EqualityStatus Theory::getEqualityStatus(TNode a, TNode b) +{ + // if not using an equality engine, then by default we don't know the status + if (d_equalityEngine == nullptr) + { + return EQUALITY_UNKNOWN; + } + Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b)); + + // Check for equality (simplest) + if (d_equalityEngine->areEqual(a, b)) + { + // The terms are implied to be equal + return EQUALITY_TRUE; + } + + // Check for disequality + if (d_equalityEngine->areDisequal(a, b, false)) + { + // The terms are implied to be dis-equal + return EQUALITY_FALSE; + } + + // All other terms are unknown, which is conservative. A theory may override + // this method if it knows more information. + return EQUALITY_UNKNOWN; +} + +void Theory::check(Effort level) +{ + // see if we are already done (as an optimization) + if (done() && level < EFFORT_FULL) + { + return; + } + Assert(d_theoryState!=nullptr); + // standard calls for resource, stats + d_out->spendResource(ResourceManager::Resource::TheoryCheckStep); + TimerStat::CodeTimer checkTimer(d_checkTime); + // pre-check at level + if (preCheck(level)) + { + // check aborted for a theory-specific reason + return; + } + // process the pending fact queue + while (!done() && !d_theoryState->isInConflict()) + { + // Get the next assertion from the fact queue + Assertion assertion = get(); + TNode fact = assertion.d_assertion; + bool polarity = fact.getKind() != kind::NOT; + TNode atom = polarity ? fact : fact[0]; + // call the pre-notify method + if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered)) + { + // handled in theory-specific way that doesn't involve equality engine + continue; + } + // Theories that don't have an equality engine should always return true + // for preNotifyFact + Assert(d_equalityEngine != nullptr); + // assert to the equality engine + if (atom.getKind() == kind::EQUAL) + { + d_equalityEngine->assertEquality(atom, polarity, fact); + } + else + { + d_equalityEngine->assertPredicate(atom, polarity, fact); + } + // notify the theory of the new fact, which is not internal + notifyFact(atom, polarity, fact, false); + } + // post-check at level + postCheck(level); +} + +bool Theory::preCheck(Effort level) { return false; } + +void Theory::postCheck(Effort level) {} + +bool Theory::preNotifyFact(TNode atom, bool polarity, TNode fact, bool isPrereg) +{ + return false; +} + +void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal) +{ +} + +void Theory::preRegisterTerm(TNode node) {} + +void Theory::addSharedTerm(TNode n) +{ + Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" + << std::endl; + Debug("theory::assertions") + << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl; + d_sharedTerms.push_back(n); + // now call theory-specific method notifySharedTerm + notifySharedTerm(n); +} + eq::EqualityEngine* Theory::getEqualityEngine() { // get the assigned equality engine, which is a pointer stored in this class diff --git a/src/theory/theory.h b/src/theory/theory.h index 349f36a57..8ea64e724 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -138,9 +138,6 @@ class Theory { /** Index into the head of the facts list */ context::CDO<unsigned> d_factsHead; - /** Add shared term to the theory. */ - void addSharedTermInternal(TNode node); - /** Indices for splitting on the shared terms. */ context::CDO<unsigned> d_sharedTermsIndex; @@ -184,7 +181,7 @@ class Theory { */ context::CDList<TNode> d_sharedTerms; - //---------------------------------- collect model info + //---------------------------------- private collect model info /** * Scans the current set of assertions and shared terms top-down * until a theory-leaf is reached, and adds all terms found to @@ -207,21 +204,7 @@ class Theory { void collectTerms(TNode n, std::set<Kind>& irrKinds, std::set<Node>& termSet) const; - /** - * Same as above, but with empty irrKinds. This version can be overridden - * by the theory, e.g. by restricting or extending the set of terms returned - * by computeRelevantTermsInternal, which is called by default with no - * irrKinds. - */ - virtual void computeRelevantTerms(std::set<Node>& termSet, - bool includeShared = true); - /** - * Collect model values, after equality information is added to the model. - * The argument termSet is the set of relevant terms returned by - * computeRelevantTerms. - */ - virtual bool collectModelValues(TheoryModel* m, std::set<Node>& termSet); - //---------------------------------- end collect model info + //---------------------------------- end private collect model info /** * Construct a Theory. @@ -334,6 +317,16 @@ class Theory { virtual void finishInit() {} //--------------------------------- end private initialization + /** + * This method is called to notify a theory that the node n should + * be considered a "shared term" by this theory. This does anything + * theory-specific concerning the fact that n is now marked as a shared + * term, which is done in addition to explicitly storing n as a shared + * term and adding it as a trigger term in the equality engine of this + * class (see addSharedTerm). + */ + virtual void notifySharedTerm(TNode n); + public: //--------------------------------- initialization /** @@ -435,25 +428,23 @@ class Theory { * Normally we call QUICK_CHECK or STANDARD; at the leaves we call * with FULL_EFFORT. */ - enum Effort { + enum Effort + { /** * Standard effort where theory need not do anything */ EFFORT_STANDARD = 50, /** - * Full effort requires the theory make sure its assertions are satisfiable or not + * Full effort requires the theory make sure its assertions are satisfiable + * or not */ EFFORT_FULL = 100, /** - * Combination effort means that the individual theories are already satisfied, and - * it is time to put some effort into propagation of shared term equalities - */ - EFFORT_COMBINATION = 150, - /** - * Last call effort, reserved for quantifiers. + * Last call effort, called after theory combination has completed with + * no lemmas and a model is available. */ EFFORT_LAST_CALL = 200 - };/* enum Effort */ + }; /* enum Effort */ static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION { return e >= EFFORT_STANDARD; } @@ -461,8 +452,6 @@ class Theory { { return e >= EFFORT_STANDARD && e < EFFORT_FULL; } static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION { return e == EFFORT_FULL; } - static inline bool combination(Effort e) CVC4_CONST_FUNCTION - { return e == EFFORT_COMBINATION; } /** * Get the id for this Theory. @@ -506,6 +495,9 @@ class Theory { return d_valuation; } + /** Get the equality engine being used by this theory. */ + eq::EqualityEngine* getEqualityEngine(); + /** * Get the quantifiers engine associated to this theory. */ @@ -513,13 +505,6 @@ class Theory { return d_quantEngine; } - /** - * Get the quantifiers engine associated to this theory (const version). - */ - const QuantifiersEngine* getQuantifiersEngine() const { - return d_quantEngine; - } - /** Get the decision manager associated to this theory. */ DecisionManager* getDecisionManager() { return d_decManager; } @@ -559,7 +544,7 @@ class Theory { /** * Pre-register a term. Done one time for a Node per SAT context level. */ - virtual void preRegisterTerm(TNode) { } + virtual void preRegisterTerm(TNode); /** * Assert a fact in the current context. @@ -571,16 +556,8 @@ class Theory { d_facts.push_back(Assertion(assertion, isPreregistered)); } - /** - * This method is called to notify a theory that the node n should - * be considered a "shared term" by this theory - */ - virtual void addSharedTerm(TNode n) { } - - /** - * Get the official equality engine of this theory. - */ - eq::EqualityEngine* getEqualityEngine(); + /** Add shared term to the theory. */ + void addSharedTerm(TNode node); /** * Return the current theory care graph. Theories should overload @@ -593,31 +570,17 @@ class Theory { * Return the status of two terms in the current context. Should be * implemented in sub-theories to enable more efficient theory-combination. */ - virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { - return EQUALITY_UNKNOWN; - } + virtual EqualityStatus getEqualityStatus(TNode a, TNode b); /** * Return the model value of the give shared term (or null if not available). - */ - virtual Node getModelValue(TNode var) { return Node::null(); } - - /** - * Check the current assignment's consistency. * - * An implementation of check() is required to either: - * - return a conflict on the output channel, - * - be interrupted, - * - throw an exception - * - or call get() until done() is true. + * TODO (project #39): this method is likely to become deprecated. */ - virtual void check(Effort level = EFFORT_FULL) { } - - /** Needs last effort check? */ - virtual bool needsCheckLastEffort() { return false; } + virtual Node getModelValue(TNode var) { return Node::null(); } /** T-propagate new literal assignments in the current context. */ - virtual void propagate(Effort level = EFFORT_FULL) { } + virtual void propagate(Effort level = EFFORT_FULL) {} /** * Return an explanation for the literal represented by parameter n @@ -630,6 +593,74 @@ class Theory { "Theory::explain() interface!"; } + //--------------------------------- check + /** + * Does this theory wish to be called to check at last call effort? This is + * the case for any theory that wishes to run when a model is available. + */ + virtual bool needsCheckLastEffort() { return false; } + /** + * Check the current assignment's consistency. + * + * An implementation of check() is required to either: + * - return a conflict on the output channel, + * - be interrupted, + * - throw an exception + * - or call get() until done() is true. + * + * The standard method for check consists of a loop that processes the entire + * fact queue when preCheck returns false. It makes four theory-specific + * callbacks, (preCheck, postCheck, preNotifyFact, notifyFact) as described + * below. It asserts each fact to the official equality engine when + * preNotifyFact returns false. + * + * Theories that use this check method must use an official theory + * state object (d_theoryState). + * + * TODO (project #39): this method should be non-virtual, once all theories + * conform to the new standard + */ + virtual void check(Effort level = EFFORT_FULL); + /** + * Pre-check, called before the fact queue of the theory is processed. + * If this method returns false, then the theory will process its fact + * queue. If this method returns true, then the theory has indicated + * its check method should finish immediately. + */ + virtual bool preCheck(Effort level = EFFORT_FULL); + /** + * Post-check, called after the fact queue of the theory is processed. + */ + virtual void postCheck(Effort level = EFFORT_FULL); + /** + * Pre-notify fact, return true if the theory processed it. If this + * method returns false, then the atom will be added to the equality engine + * of the theory and notifyFact will be called with isInternal=false. + * + * Theories that implement check but do not use official equality + * engines should always return true for this method. + * + * @param atom The atom + * @param polarity Its polarity + * @param fact The original literal that was asserted + * @param isPrereg Whether the assertion is preregistered + * @return true if the theory completely processed this fact, i.e. it does + * not need to assert the fact to its equality engine. + */ + virtual bool preNotifyFact(TNode atom, bool pol, TNode fact, bool isPrereg); + /** + * Notify fact, called immediately after the fact was pushed into the + * equality engine. + * + * @param atom The atom + * @param polarity Its polarity + * @param fact The original literal that was asserted + * @param isInternal Whether the origin of the fact was internal + */ + virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal); + //--------------------------------- end check + + //--------------------------------- collect model info /** * Get all relevant information in this theory regarding the current * model. This should be called after a call to check( FULL_EFFORT ) @@ -637,10 +668,34 @@ class Theory { * * This method returns true if and only if the equality engine of m is * consistent as a result of this call. + * + * The standard method for collectModelInfo computes the relevant terms, + * asserts the theory's equality engine to the model (if necessary) and + * then calls computeModelValues. + * + * TODO (project #39): this method should be non-virtual, once all theories + * conform to the new standard */ virtual bool collectModelInfo(TheoryModel* m); + /** + * Same as above, but with empty irrKinds. This version can be overridden + * by the theory, e.g. by restricting or extending the set of terms returned + * by computeRelevantTermsInternal, which is called by default with no + * irrKinds. + */ + virtual void computeRelevantTerms(std::set<Node>& termSet, + bool includeShared = true); + /** + * Collect model values, after equality information is added to the model. + * The argument termSet is the set of relevant terms returned by + * computeRelevantTerms. + */ + virtual bool collectModelValues(TheoryModel* m, std::set<Node>& termSet); /** if theories want to do something with model after building, do it here */ virtual void postProcessModel( TheoryModel* m ){ } + //--------------------------------- end collect model info + + //--------------------------------- preprocessing /** * Statically learn from assertion "in," which has been asserted * true at the top level. The theory should only add (via @@ -681,6 +736,7 @@ class Theory { * preprocessing before they are asserted to theory engine. */ virtual void ppNotifyAssertions(const std::vector<Node>& assertions) {} + //--------------------------------- end preprocessing /** * A Theory is called with presolve exactly one time per user @@ -941,7 +997,6 @@ class Theory { /** Turn on proof-production mode. */ void produceProofs() { d_proofsEnabled = true; } - };/* class Theory */ std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b88b6158e..cf29039ff 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1219,7 +1219,7 @@ void TheoryEngine::assertFact(TNode literal) Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term); for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) { if (Theory::setContains(id, theories)) { - theoryOf(id)->addSharedTermInternal(term); + theoryOf(id)->addSharedTerm(term); } } d_sharedTerms.markNotified(term, theories); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 29014d33f..7d554c613 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -503,7 +503,8 @@ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) { return EQUALITY_FALSE_IN_MODEL; } -void TheoryUF::addSharedTerm(TNode t) { +void TheoryUF::notifySharedTerm(TNode t) +{ Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl; d_equalityEngine->addTriggerTerm(t, THEORY_UF); } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 8efaf79e3..916c6ef6b 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -184,7 +184,7 @@ private: void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; void presolve() override; - void addSharedTerm(TNode n) override; + void notifySharedTerm(TNode n) override; void computeCareGraph() override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; |