Prepare theory of sets for dynamic allocation of equality engine (#4868)

In forthcoming PRs, Theory objects will be assigned equality engine objects dynamically.

This PR prepares the theory of sets for this update, which involves refactoring of its internal members.

1 files changed, 33 insertions, 7 deletions

diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index e81412ba9..f1b59e419 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -33,6 +33,8 @@ class TheorySetsScrutinize;
 
 class TheorySets : public Theory
 {
+  friend class TheorySetsPrivate;
+  friend class TheorySetsRels;
  public:
   /** Constructs a new instance of TheorySets w.r.t. the provided contexts. */
   TheorySets(context::Context* c,
@@ -43,10 +45,13 @@ class TheorySets : public Theory
              ProofNodeManager* pnm);
   ~TheorySets() override;
 
+  //--------------------------------- initialization
+  /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
-
   /** finish initialization */
   void finishInit() override;
+  //--------------------------------- end initialization
+
   void addSharedTerm(TNode) override;
   void check(Effort) override;
   bool collectModelInfo(TheoryModel* m) override;
@@ -60,15 +65,36 @@ class TheorySets : public Theory
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
   void presolve() override;
   void propagate(Effort) override;
-  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
   bool isEntailed(Node n, bool pol);
-
+  /* equality engine */
+  virtual eq::EqualityEngine* getEqualityEngine() override;
  private:
-  friend class TheorySetsPrivate;
-  friend class TheorySetsScrutinize;
-  friend class TheorySetsRels;
-
+  /** Functions to handle callbacks from equality engine */
+  class NotifyClass : public eq::EqualityEngineNotify
+  {
+   public:
+    NotifyClass(TheorySetsPrivate& theory) : d_theory(theory) {}
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override;
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override;
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
+    void eqNotifyNewClass(TNode t) override;
+    void eqNotifyPreMerge(TNode t1, TNode t2) override;
+    void eqNotifyPostMerge(TNode t1, TNode t2) override;
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
+    
+   private:
+    TheorySetsPrivate& d_theory;
+  };
+  /** The internal theory */
   std::unique_ptr<TheorySetsPrivate> d_internal;
+  /** Instance of the above class */
+  NotifyClass d_notify;  
+  /** Equality engine */
+  eq::EqualityEngine d_equalityEngine;
 }; /* class TheorySets */
 
 }/* CVC4::theory::sets namespace */