diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-02 08:17:39 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-02 08:17:39 -0500 |
commit | 78917e16f6521b0e8a074f3649fc6adf37614617 (patch) | |
tree | 702258e43bb5e46b230a67637a2ea356b55c6cd6 /src/theory/sets/theory_sets.h | |
parent | 3830d80ce312e8633b9de6311b809bd9418ddd4a (diff) |
(new theory) Update TheorySets to the new interface (#4951)
This updates the theory of sets to the new interface (see #4929).
Diffstat (limited to 'src/theory/sets/theory_sets.h')
-rw-r--r-- | src/theory/sets/theory_sets.h | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index a826a43af..7787c0f9b 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -58,13 +58,23 @@ class TheorySets : public Theory void finishInit() override; //--------------------------------- end initialization - void notifySharedTerm(TNode) override; - void check(Effort) override; + //--------------------------------- standard check + /** Post-check, called after the fact queue of the theory is processed. */ + void postCheck(Effort level) override; + /** Pre-notify fact, return true if processed. */ + bool preNotifyFact(TNode atom, + bool pol, + TNode fact, + bool isPrereg, + bool isInternal) override; + /** Notify fact */ + void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override; + //--------------------------------- end standard check + /** Collect model values in m based on the relevant terms given by termSet */ bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet) override; void computeCareGraph() override; TrustNode explain(TNode) override; - EqualityStatus getEqualityStatus(TNode a, TNode b) override; Node getModelValue(TNode) override; std::string identify() const override { return "THEORY_SETS"; } void preRegisterTerm(TNode node) override; @@ -72,6 +82,7 @@ class TheorySets : public Theory PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; void presolve() override; bool isEntailed(Node n, bool pol); + private: /** Functions to handle callbacks from equality engine */ class NotifyClass : public eq::EqualityEngineNotify |