Standard equality engine notify class for Theory (#5042)

This makes a standard equality engine notify class that forwards the 3 mandatory callbacks to the provided inference manager (the other 3 callbacks may be specific to the theory). It updates TheoryUF to use this class, other theories will be updated to this style as more inference manager are added.

Notice that we could also forward the other 3 callbacks in this class to Theory, making eqNotifyNewClass, eqNotifyMerge, and eqNotifyDisequal virtual methods in Theory, which can be done on a future PR if needed.

1 files changed, 14 insertions, 46 deletions

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 86c1b62c8..25825e17d 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -24,6 +24,7 @@
 #include "expr/node.h"
 #include "expr/node_trie.h"
 #include "theory/theory.h"
+#include "theory/theory_eq_notify.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_checker.h"
 #include "theory/uf/proof_equality_engine.h"
@@ -38,44 +39,19 @@ class CardinalityExtension;
 class HoExtension;
 
 class TheoryUF : public Theory {
-
-public:
-
-  class NotifyClass : public eq::EqualityEngineNotify {
-    TheoryUF& d_uf;
-  public:
-    NotifyClass(TheoryUF& uf): d_uf(uf) {}
-
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
-    {
-      Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
-      if (value) {
-        return d_uf.propagateLit(predicate);
-      }
-      return d_uf.propagateLit(predicate.notNode());
-    }
-
-    bool eqNotifyTriggerTermEquality(TheoryId tag,
-                                     TNode t1,
-                                     TNode t2,
-                                     bool value) override
-    {
-      Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
-      if (value) {
-        return d_uf.propagateLit(t1.eqNode(t2));
-      }
-      return d_uf.propagateLit(t1.eqNode(t2).notNode());
-    }
-
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
+ public:
+  class NotifyClass : public TheoryEqNotifyClass
+  {
+   public:
+    NotifyClass(TheoryInferenceManager& im, TheoryUF& uf)
+        : TheoryEqNotifyClass(im), d_uf(uf)
     {
-      Debug("uf-notify") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
-      d_uf.conflict(t1, t2);
     }
 
     void eqNotifyNewClass(TNode t) override
     {
-      Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl;
+      Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")"
+                         << std::endl;
       d_uf.eqNotifyNewClass(t);
     }
 
@@ -92,13 +68,12 @@ public:
       d_uf.eqNotifyDisequal(t1, t2, reason);
     }
 
+   private:
+    /** Reference to the parent theory */
+    TheoryUF& d_uf;
   };/* class TheoryUF::NotifyClass */
 
 private:
-
-  /** The notify class */
-  NotifyClass d_notify;
-
   /** The associated cardinality extension (or nullptr if it does not exist) */
   std::unique_ptr<CardinalityExtension> d_thss;
   /** the higher-order solver extension (or nullptr if it does not exist) */
@@ -107,21 +82,12 @@ private:
   /** node for true */
   Node d_true;
 
-  /**
-   * Should be called to propagate the literal. We use a node here
-   * since some of the propagated literals are not kept anywhere.
-   */
-  bool propagateLit(TNode literal);
-
   /** All the function terms that the theory has seen */
   context::CDList<TNode> d_functionsTerms;
 
   /** Symmetry analyzer */
   SymmetryBreaker d_symb;
 
-  /** Conflict when merging two constants */
-  void conflict(TNode a, TNode b);
-
   /** called when a new equivalance class is created */
   void eqNotifyNewClass(TNode t);
 
@@ -206,6 +172,8 @@ private:
   TheoryState d_state;
   /** A (default) inference manager */
   TheoryInferenceManager d_im;
+  /** The notify class */
+  NotifyClass d_notify;
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */