Merge branch 'master' into fixCMSBuildPRfixCMSBuildPR

1 files changed, 16 insertions, 4 deletions

diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index a7fb31dab..7787c0f9b 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -58,12 +58,23 @@ class TheorySets : public Theory
   void finishInit() override;
   //--------------------------------- end initialization
 
-  void notifySharedTerm(TNode) override;
-  void check(Effort) override;
-  bool collectModelInfo(TheoryModel* m) 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;
@@ -71,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