From 983f41ea94f68e90d24e353ae3fd1aca04ac56ff Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 24 Aug 2020 09:43:06 -0500 Subject: Extend the standard Theory template based on equality engine (#4929) Apart from { quantifiers, bool, builtin }, each Theory now has an official equality engine. This PR elaborates on the standard recommended template that Theory should follow, which applies to all theories, regardless of whether they have an equality engine. This includes: A standard check method. The Theory is now expected to implement 4 callbacks (preCheck, postCheck, preNotifyFact, notifyFact). A standard collectModelInfo method. The Theory is now expected to implement 2 callbacks (computeRelevantTerms, collectModelValues). Additionally, 2 more methods have an obvious default: (1) getEqualityStatus, which returns information based on an equality engine if it exists, (2) addSharedTerm, which adds the term as a trigger term to the equality engine of the theory if it exists. Notice that for the sake of more consistent naming, theories now implement notifySharedTerm (previously TheoryEngine called theory-independent addSharedTermInternal which called addSharedTerm, this is updated now to addSharedTerm/notifySharedTerm). Other methods will not be standardized yet e.g. preRegisterTerm, since they vary per theory. FYI @barrettcw Each theory on the branch https://github.com/ajreynol/CVC4/tree/centralEe conforms to this template (e.g. they do not override check or collectModelInfo). The next step will be to pull the new implementation of each Theory from that branch. --- src/theory/sep/theory_sep.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/theory/sep/theory_sep.cpp') 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); } -- cgit v1.2.3