Standardize equality engine notifications in sets (#5098)

1 files changed, 6 insertions, 8 deletions

diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index fce57ca6c..4d0c74516 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -25,6 +25,7 @@
 #include "theory/sets/skolem_cache.h"
 #include "theory/sets/solver_state.h"
 #include "theory/theory.h"
+#include "theory/theory_eq_notify.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
@@ -82,16 +83,13 @@ class TheorySets : public Theory
 
  private:
   /** Functions to handle callbacks from equality engine */
-  class NotifyClass : public eq::EqualityEngineNotify
+  class NotifyClass : public TheoryEqNotifyClass
   {
    public:
-    NotifyClass(TheorySetsPrivate& theory) : d_theory(theory) {}
-    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;
+    NotifyClass(TheorySetsPrivate& theory, TheoryInferenceManager& im)
+        : TheoryEqNotifyClass(im), d_theory(theory)
+    {
+    }
     void eqNotifyNewClass(TNode t) override;
     void eqNotifyMerge(TNode t1, TNode t2) override;
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;