diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-24 09:43:06 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-24 09:43:06 -0500 |
commit | 983f41ea94f68e90d24e353ae3fd1aca04ac56ff (patch) | |
tree | 511720f4a1431b7e5b77712cfbbc512d7311ad5b /src/theory/sets | |
parent | 413da163bd36c8a9651308d7249e9aaf811872af (diff) |
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.
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/theory_sets.cpp | 4 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.h | 2 |
2 files changed, 2 insertions, 4 deletions
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; |