2 files changed, 16 insertions, 77 deletions

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 18ab70d46..4a9f52918 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -46,15 +46,13 @@ TheoryUF::TheoryUF(context::Context* c,
                    ProofNodeManager* pnm,
                    std::string instanceName)
     : Theory(THEORY_UF, c, u, out, valuation, logicInfo, pnm, instanceName),
-      d_notify(*this),
-      /* The strong theory solver can be notified by EqualityEngine::init(),
-       * so make sure it's initialized first. */
       d_thss(nullptr),
       d_ho(nullptr),
       d_functionsTerms(c),
       d_symb(u, instanceName),
       d_state(c, u, valuation),
-      d_im(*this, d_state, pnm)
+      d_im(*this, d_state, pnm),
+      d_notify(d_im, *this)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
 
@@ -268,25 +266,6 @@ void TheoryUF::preRegisterTerm(TNode node)
   }
 }
 
-bool TheoryUF::propagateLit(TNode literal)
-{
-  Debug("uf::propagate") << "TheoryUF::propagateLit(" << literal << ")"
-                         << std::endl;
-  // If already in conflict, no more propagation
-  if (d_state.isInConflict())
-  {
-    Debug("uf::propagate") << "TheoryUF::propagateLit(" << literal
-                           << "): already in conflict" << std::endl;
-    return false;
-  }
-  // Propagate out
-  bool ok = d_out->propagate(literal);
-  if (!ok) {
-    d_state.notifyInConflict();
-  }
-  return ok;
-}/* TheoryUF::propagate(TNode) */
-
 void TheoryUF::explain(TNode literal, Node& exp)
 {
   Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
@@ -648,14 +627,6 @@ void TheoryUF::computeCareGraph() {
                        << std::endl;
 }/* TheoryUF::computeCareGraph() */
 
-void TheoryUF::conflict(TNode a, TNode b)
-{
-  // call the inference manager, which will construct the conflict (possibly
-  // with proofs from the underlying proof equality engine), and notify the
-  // state object.
-  d_im.conflictEqConstantMerge(a, b);
-}
-
 void TheoryUF::eqNotifyNewClass(TNode t) {
   if (d_thss != NULL) {
     d_thss->newEqClass(t);
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 */