From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 14 Aug 2020 18:07:17 +0000 (-0500)
Subject: Simplify equality engine notifications (#4896)
X-Git-Tag: cvc5-1.0.0~3001
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=42cd0a7bcbe993870d76d8cc9db7acc0a9ae70f9;p=cvc5.git

Simplify equality engine notifications (#4896)

Previously, there was methods for being informed just before and just after equivalence classes are merged (eqNotifyPreMerge and eqNotifyPostMerge). The purpose of this was to allow e.g. the theory to inspect the equivalence classes in question before the equality engine modified them. However this is no longer used, and moreover is discouraged since Theory should generally buffer their usage of EqualityEngine while it is making internal calls.

TheoryStrings was the only theory to use eqNotifyPreMerge (somewhat arbitrarily), all others used eqNotifyPostMerge. This makes post-merge the default, renames it to eqNotifyMerge and removes pre notifications.

This will simplify the work of the new theory combination methods as well as leading to fewer spurious calls to callbacks in equality engine.
---

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 858098b70..ab3b485a8 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -110,9 +110,9 @@ void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyConstantTermMerge(TN
 }
 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyNewClass(TNode t) {
 }
-void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyPreMerge(TNode t1, TNode t2) {
-}
-void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyPostMerge(TNode t1, TNode t2) {
+void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyMerge(TNode t1,
+                                                                  TNode t2)
+{
 }
 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 }
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 96f82b059..aeb72ec94 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -72,8 +72,7 @@ private:
 
     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 eqNotifyMerge(TNode t1, TNode t2) override;
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
   };
   ArithCongruenceNotify d_notify;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 54acf21a5..116b0f43b 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -341,8 +341,7 @@ class TheoryArrays : public Theory {
     }
 
     void eqNotifyNewClass(TNode t) override {}
-    void eqNotifyPreMerge(TNode t1, TNode t2) override {}
-    void eqNotifyPostMerge(TNode t1, TNode t2) override
+    void eqNotifyMerge(TNode t1, TNode t2) override
     {
       if (t1.getType().isArray()) {
         d_arrays.mergeArrays(t1, t2);
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 8f4f9089a..181d6ec79 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -62,8 +62,7 @@ class CoreSolver : public SubtheorySolver {
                                      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 eqNotifyMerge(TNode t1, TNode t2) override {}
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
   };
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 17a43bc04..832324d4b 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -841,15 +841,12 @@ void TheoryDatatypes::eqNotifyNewClass(TNode t){
   }
 }
 
-/** called when two equivalance classes will merge */
-void TheoryDatatypes::eqNotifyPreMerge(TNode t1, TNode t2){
-
-}
-
 /** called when two equivalance classes have merged */
-void TheoryDatatypes::eqNotifyPostMerge(TNode t1, TNode t2){
+void TheoryDatatypes::eqNotifyMerge(TNode t1, TNode t2)
+{
   if( t1.getType().isDatatype() ){
-    Trace("datatypes-debug") << "NotifyPostMerge : " << t1 << " " << t2 << std::endl;
+    Trace("datatypes-debug")
+        << "NotifyMerge : " << t1 << " " << t2 << std::endl;
     d_pending_merge.push_back( t1.eqNode( t2 ) );
   }
 }
@@ -978,11 +975,6 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
   }
 }
 
-/** called when two equivalence classes are made disequal */
-void TheoryDatatypes::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
-
-}
-
 TheoryDatatypes::EqcInfo::EqcInfo( context::Context* c )
     : d_inst( c, false )
     , d_constructor( c, Node::null() )
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index ba8321e50..422a01f07 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -99,20 +99,14 @@ class TheoryDatatypes : public Theory {
       Debug("dt") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl;
       d_dt.eqNotifyNewClass(t);
     }
-    void eqNotifyPreMerge(TNode t1, TNode t2) override
+    void eqNotifyMerge(TNode t1, TNode t2) override
     {
-      Debug("dt") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl;
-      d_dt.eqNotifyPreMerge(t1, t2);
-    }
-    void eqNotifyPostMerge(TNode t1, TNode t2) override
-    {
-      Debug("dt") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl;
-      d_dt.eqNotifyPostMerge(t1, t2);
+      Debug("dt") << "NotifyClass::eqNotifyMerge(" << t1 << ", " << t2 << ")"
+                  << std::endl;
+      d_dt.eqNotifyMerge(t1, t2);
     }
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
     {
-      Debug("dt") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
-      d_dt.eqNotifyDisequal(t1, t2, reason);
     }
   };/* class TheoryDatatypes::NotifyClass */
 private:
@@ -295,12 +289,8 @@ private:
   void conflict(TNode a, TNode b);
   /** called when a new equivalance class is created */
   void eqNotifyNewClass(TNode t);
-  /** called when two equivalance classes will merge */
-  void eqNotifyPreMerge(TNode t1, TNode t2);
   /** called when two equivalance classes have merged */
-  void eqNotifyPostMerge(TNode t1, TNode t2);
-  /** called when two equivalence classes are made disequal */
-  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+  void eqNotifyMerge(TNode t1, TNode t2);
 
   void check(Effort e) override;
   bool needsCheckLastEffort() override;
diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h
index 67140515a..3de1898d7 100644
--- a/src/theory/ee_manager_distributed.h
+++ b/src/theory/ee_manager_distributed.h
@@ -120,8 +120,7 @@ class EqEngineManagerDistributed : public EqEngineManager
       return true;
     }
     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
-    void eqNotifyPreMerge(TNode t1, TNode t2) override {}
-    void eqNotifyPostMerge(TNode t1, TNode t2) override {}
+    void eqNotifyMerge(TNode t1, TNode t2) override {}
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
 
    private:
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index a3e0dd94a..a1dd8a731 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -80,8 +80,7 @@ class TheoryFp : public Theory {
                                      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 eqNotifyMerge(TNode t1, TNode t2) override {}
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
   };
   friend NotifyClass;
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 21a3bd44b..8eeb7a8e0 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -122,7 +122,8 @@ void ConjectureGenerator::eqNotifyNewClass( TNode t ){
   d_upendingAdds.push_back( t );
 }
 
-void ConjectureGenerator::eqNotifyPreMerge(TNode t1, TNode t2) {
+void ConjectureGenerator::eqNotifyMerge(TNode t1, TNode t2)
+{
   //get maintained representatives
   TNode rt1 = t1;
   TNode rt2 = t2;
@@ -151,15 +152,6 @@ void ConjectureGenerator::eqNotifyPreMerge(TNode t1, TNode t2) {
   }
 }
 
-void ConjectureGenerator::eqNotifyPostMerge(TNode t1, TNode t2) {
-
-}
-
-void ConjectureGenerator::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
-  Trace("thm-ee-debug") << "UEE : disequality holds : " << t1 << " != " << t2 << std::endl;
-
-}
-
 
 ConjectureGenerator::EqcInfo::EqcInfo( context::Context* c ) : d_rep( c, Node::null() ){
 
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index d7c314a9a..1e8099054 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -263,17 +263,12 @@ private:
     }
     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
     void eqNotifyNewClass(TNode t) override { d_sg.eqNotifyNewClass(t); }
-    void eqNotifyPreMerge(TNode t1, TNode t2) override
+    void eqNotifyMerge(TNode t1, TNode t2) override
     {
-      d_sg.eqNotifyPreMerge(t1, t2);
-    }
-    void eqNotifyPostMerge(TNode t1, TNode t2) override
-    {
-      d_sg.eqNotifyPostMerge(t1, t2);
+      d_sg.eqNotifyMerge(t1, t2);
     }
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
     {
-      d_sg.eqNotifyDisequal(t1, t2, reason);
     }
   };/* class ConjectureGenerator::NotifyClass */
   /** The notify class */
@@ -299,12 +294,8 @@ private:
   std::map< Node, EqcInfo* > d_eqc_info;
   /** called when a new equivalance class is created */
   void eqNotifyNewClass(TNode t);
-  /** called when two equivalance classes will merge */
-  void eqNotifyPreMerge(TNode t1, TNode t2);
   /** called when two equivalance classes have merged */
-  void eqNotifyPostMerge(TNode t1, TNode t2);
-  /** called when two equivalence classes are made disequal */
-  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+  void eqNotifyMerge(TNode t1, TNode t2);
   /** are universal equal */
   bool areUniversalEqual( TNode n1, TNode n2 );
   /** are universal disequal */
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index e9b186ae2..4dfdb9fa5 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1584,12 +1584,8 @@ bool TheorySep::areDisequal( Node a, Node b ){
   return false;
 }
 
-
-void TheorySep::eqNotifyPreMerge(TNode t1, TNode t2) {
-
-}
-
-void TheorySep::eqNotifyPostMerge(TNode t1, TNode t2) {
+void TheorySep::eqNotifyMerge(TNode t1, TNode t2)
+{
   HeapAssertInfo * e2 = getOrMakeEqcInfo( t2, false );
   if( e2 && ( !e2->d_pto.get().isNull() || e2->d_has_neg_pto.get() ) ){
     HeapAssertInfo * e1 = getOrMakeEqcInfo( t1, true );
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 3685ea063..7c6ce38c4 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -192,13 +192,9 @@ class TheorySep : public Theory {
     }
 
     void eqNotifyNewClass(TNode t) override {}
-    void eqNotifyPreMerge(TNode t1, TNode t2) override
+    void eqNotifyMerge(TNode t1, TNode t2) override
     {
-      d_sep.eqNotifyPreMerge(t1, t2);
-    }
-    void eqNotifyPostMerge(TNode t1, TNode t2) override
-    {
-      d_sep.eqNotifyPostMerge(t1, t2);
+      d_sep.eqNotifyMerge(t1, t2);
     }
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
   };
@@ -324,8 +320,7 @@ class TheorySep : public Theory {
   bool hasTerm( Node a );
   bool areEqual( Node a, Node b );
   bool areDisequal( Node a, Node b );
-  void eqNotifyPreMerge(TNode t1, TNode t2);
-  void eqNotifyPostMerge(TNode t1, TNode t2);
+  void eqNotifyMerge(TNode t1, TNode t2);
 
   void sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer = false );
   void doPendingFacts();
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 021db5bd3..bf81099a7 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -267,18 +267,11 @@ void TheorySets::NotifyClass::eqNotifyNewClass(TNode t)
   d_theory.eqNotifyNewClass(t);
 }
 
-void TheorySets::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
+void TheorySets::NotifyClass::eqNotifyMerge(TNode t1, TNode t2)
 {
-  Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:"
+  Debug("sets-eq") << "[sets-eq] eqNotifyMerge:"
                    << " t1 = " << t1 << " t2 = " << t2 << std::endl;
-  d_theory.eqNotifyPreMerge(t1, t2);
-}
-
-void TheorySets::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
-{
-  Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:"
-                   << " t1 = " << t1 << " t2 = " << t2 << std::endl;
-  d_theory.eqNotifyPostMerge(t1, t2);
+  d_theory.eqNotifyMerge(t1, t2);
 }
 
 void TheorySets::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 505ba9547..84291346b 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -83,8 +83,7 @@ class TheorySets : public Theory
                                      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 eqNotifyMerge(TNode t1, TNode t2) override;
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
     
    private:
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 25ee3167e..bb9423570 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -79,9 +79,7 @@ void TheorySetsPrivate::eqNotifyNewClass(TNode t)
   }
 }
 
-void TheorySetsPrivate::eqNotifyPreMerge(TNode t1, TNode t2) {}
-
-void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2)
+void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
 {
   if (!d_state.isInConflict())
   {
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 2779a42b7..27ea6a9b8 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -44,8 +44,7 @@ class TheorySetsPrivate {
 
  public:
   void eqNotifyNewClass(TNode t);
-  void eqNotifyPreMerge(TNode t1, TNode t2);
-  void eqNotifyPostMerge(TNode t1, TNode t2);
+  void eqNotifyMerge(TNode t1, TNode t2);
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
   /** Assert fact holds in the current context with explanation exp.
    *
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 0bfd8e094..55cd84e58 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -104,8 +104,7 @@ private:
     }
 
     void eqNotifyNewClass(TNode t) override {}
-    void eqNotifyPreMerge(TNode t1, TNode t2) override {}
-    void eqNotifyPostMerge(TNode t1, TNode t2) override {}
+    void eqNotifyMerge(TNode t1, TNode t2) override {}
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
   };
 
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 06a86935f..970b832a9 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -129,7 +129,7 @@ void SolverState::eqNotifyNewClass(TNode t)
   }
 }
 
-void SolverState::eqNotifyPreMerge(TNode t1, TNode t2)
+void SolverState::eqNotifyMerge(TNode t1, TNode t2)
 {
   EqcInfo* e2 = getOrMakeEqcInfo(t2, false);
   if (e2)
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index 2eee90ca4..8d3162b38 100644
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -82,8 +82,8 @@ class SolverState
   //-------------------------------------- notifications for equalities
   /** called when a new equivalence class is created */
   void eqNotifyNewClass(TNode t);
-  /** called when two equivalence classes will merge */
-  void eqNotifyPreMerge(TNode t1, TNode t2);
+  /** called when two equivalence classes merge */
+  void eqNotifyMerge(TNode t1, TNode t2);
   /** called when two equivalence classes are made disequal */
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
   //-------------------------------------- end notifications for equalities
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 29c3cd64c..1d3261115 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -166,14 +166,11 @@ class TheoryStrings : public Theory {
       Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
       d_str.eqNotifyNewClass(t);
     }
-    void eqNotifyPreMerge(TNode t1, TNode t2) override
+    void eqNotifyMerge(TNode t1, TNode t2) override
     {
-      Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
-      d_state.eqNotifyPreMerge(t1, t2);
-    }
-    void eqNotifyPostMerge(TNode t1, TNode t2) override
-    {
-      Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
+      Debug("strings") << "NotifyClass::eqNotifyMerge(" << t1 << ", " << t2
+                       << std::endl;
+      d_state.eqNotifyMerge(t1, t2);
     }
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
     {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 5b04e49a8..081d53098 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -174,12 +174,7 @@ class TheoryEngine {
     }
     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
     void eqNotifyNewClass(TNode t) override { d_te.eqNotifyNewClass(t); }
-    void eqNotifyPreMerge(TNode t1, TNode t2) override
-    {
-    }
-    void eqNotifyPostMerge(TNode t1, TNode t2) override
-    {
-    }
+    void eqNotifyMerge(TNode t1, TNode t2) override {}
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
     {
     }
@@ -190,9 +185,6 @@ class TheoryEngine {
    * notification methods
    */
   void eqNotifyNewClass(TNode t);
-  void eqNotifyPreMerge(TNode t1, TNode t2);
-  void eqNotifyPostMerge(TNode t1, TNode t2);
-  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 
   /**
    * The quantifiers engine
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 172b2407c..643029b05 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -593,15 +593,13 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
   EqualityNode cc1 = getEqualityNode(n1);
   EqualityNode cc2 = getEqualityNode(n2);
   bool doNotify = false;
-  // notify the theory
-  // the second part of this check is needed due to the internal implementation of this class.
-  // It ensures that we are merging terms and not operators.
-  if (d_performNotify && class1Id==cc1.getFind() && class2Id==cc2.getFind()) {
+  // Determine if we should notify the owner of this class of this merge.
+  // The second part of this check is needed due to the internal implementation
+  // of this class. It ensures that we are merging terms and not operators.
+  if (d_performNotify && class1Id == cc1.getFind() && class2Id == cc2.getFind())
+  {
     doNotify = true;
   }
-  if (doNotify) {
-    d_notify.eqNotifyPreMerge(n1, n2);
-  }
 
   // Check for constant merges
   bool class1isConstant = d_isConstant[class1Id];
@@ -729,7 +727,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
 
   // notify the theory
   if (doNotify) {
-    d_notify.eqNotifyPostMerge(n1, n2);
+    d_notify.eqNotifyMerge(n1, n2);
   }
 
   // Go through the trigger term disequalities and propagate
diff --git a/src/theory/uf/equality_engine_notify.h b/src/theory/uf/equality_engine_notify.h
index 2fd839115..f63a887ef 100644
--- a/src/theory/uf/equality_engine_notify.h
+++ b/src/theory/uf/equality_engine_notify.h
@@ -77,21 +77,13 @@ class EqualityEngineNotify
    */
   virtual void eqNotifyNewClass(TNode t) = 0;
 
-  /**
-   * Notifies about the merge of two classes (just before the merge).
-   *
-   * @param t1 a term
-   * @param t2 a term
-   */
-  virtual void eqNotifyPreMerge(TNode t1, TNode t2) = 0;
-
   /**
    * Notifies about the merge of two classes (just after the merge).
    *
    * @param t1 a term
    * @param t2 a term
    */
-  virtual void eqNotifyPostMerge(TNode t1, TNode t2) = 0;
+  virtual void eqNotifyMerge(TNode t1, TNode t2) = 0;
 
   /**
    * Notifies about the disequality of two terms.
@@ -128,8 +120,7 @@ class EqualityEngineNotifyNone : public EqualityEngineNotify
   }
   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 eqNotifyMerge(TNode t1, TNode t2) override {}
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
 }; /* class EqualityEngineNotifyNone */
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 02c9cb467..862a906a0 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -657,13 +657,8 @@ void TheoryUF::eqNotifyNewClass(TNode t) {
   }
 }
 
-void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) {
-  //if (getLogicInfo().isQuantified()) {
-    //getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 );
-  //}
-}
-
-void TheoryUF::eqNotifyPostMerge(TNode t1, TNode t2) {
+void TheoryUF::eqNotifyMerge(TNode t1, TNode t2)
+{
   if (d_thss != NULL) {
     d_thss->merge(t1, t2);
   }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 58f4f18a5..345547301 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -91,16 +91,11 @@ public:
       d_uf.eqNotifyNewClass(t);
     }
 
-    void eqNotifyPreMerge(TNode t1, TNode t2) override
+    void eqNotifyMerge(TNode t1, TNode t2) override
     {
-      Debug("uf-notify") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl;
-      d_uf.eqNotifyPreMerge(t1, t2);
-    }
-
-    void eqNotifyPostMerge(TNode t1, TNode t2) override
-    {
-      Debug("uf-notify") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl;
-      d_uf.eqNotifyPostMerge(t1, t2);
+      Debug("uf-notify") << "NotifyClass::eqNotifyMerge(" << t1 << ", " << t2
+                         << ")" << std::endl;
+      d_uf.eqNotifyMerge(t1, t2);
     }
 
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
@@ -163,11 +158,8 @@ private:
   /** called when a new equivalance class is created */
   void eqNotifyNewClass(TNode t);
 
-  /** called when two equivalance classes will merge */
-  void eqNotifyPreMerge(TNode t1, TNode t2);
-
   /** called when two equivalance classes have merged */
-  void eqNotifyPostMerge(TNode t1, TNode t2);
+  void eqNotifyMerge(TNode t1, TNode t2);
 
   /** called when two equivalence classes are made disequal */
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);