diff options
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 |