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 858098b7085c942c5005acf0bad1757d95cb1aa4..ab3b485a8692551d513ff178e178024ffb62a421 100644 (file)
--- 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 96f82b059032c7f0459732a9d3a09af652ea240d..aeb72ec94014a08c62c609c40fad5d3a44b6d215 100644 (file)
--- 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 54acf21a5949697e16c72270f7e191e7ebf0e9f6..116b0f43b5aad324ddc495ab86817d0d01da679f 100644 (file)
--- 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 8f4f9089a3956cf704ae18164e613f933398f4c9..181d6ec794240e5ff9106bccabd7a8394ddf9427 100644 (file)
--- 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 17a43bc04f18a849f73e4083a96f1c5b4acc54cb..832324d4b2b773e2427d85ce49c8387a7600ebc4 100644 (file)
--- 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 ba8321e5028019fd4b54dcfd1089f42acc6edd97..422a01f07ef2fed9a5f9de930451a19e4ea87d7c 100644 (file)
--- 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 67140515a9a1dcb664542d7038d173b83625ca5c..3de1898d73ba7fdf42739ce5dcf05a0481e5961b 100644 (file)
--- 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 a3e0dd94af15539b41d69a46781dbd9f49c62311..a1dd8a731b2b8f0add5412582a557d12a30daf1c 100644 (file)
--- 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 21a3bd44b359b805a9d815e1ef36a571945d7a08..8eeb7a8e05ee3051f41b93ff72023628b04a5d93 100644 (file)
--- 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 d7c314a9aba8fe44869c9d037407a9d1133d35ed..1e8099054a14ac1bd2ccdd10651935c3fda0d945 100644 (file)
--- 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 e9b186ae2b6f1f6bcde3c62fc5c36ff222037cb1..4dfdb9fa5bfa26ab7f6e6c32465a8ca0d3089d58 100644 (file)
--- 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 3685ea06362afc93c90568a6b5fec653f8fcda6a..7c6ce38c4b65c69b0cb3302f4b758ba97e679c67 100644 (file)
--- 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 021db5bd384abebfae763ec9db81a6033a71a70b..bf81099a76a4b5d639f97ae2276c2a0710b7eee8 100644 (file)
--- 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 505ba95471672f04b03e4ff42862305b9d359193..84291346bd709289effec7cc6ec9d8dc87d36db7 100644 (file)
--- 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 25ee3167e3a4703989888464df10613819792622..bb94235706cdcf9fc9b135a4475b02653eb8ca72 100644 (file)
--- 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 2779a42b7c905545f21285fcec74b5f998e0e181..27ea6a9b876ab6d694ccffd43883b37a91dd6c5a 100644 (file)
--- 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 0bfd8e094ce1c6afd1f7260ccf2bb8b3b391a9a1..55cd84e584234f8f5697005e6a60bf015c08644f 100644 (file)
--- 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 06a86935f03b5e39a006302204acb7f1e8661dd1..970b832a9e6f6efbc636b50a310d28d77bf69b3c 100644 (file)
--- 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 2eee90ca4b42a44543861abdc1c7d21744201458..8d3162b3800b0018eb3d4ccfab06460d67349020 100644 (file)
--- 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 29c3cd64c6786bf444ba382090df467753814c1e..1d32611150ac70d25084ffccf6d5d78d0dfd5f81 100644 (file)
--- 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 5b04e49a8a0fccc61025b0d174ae4294157c0948..081d53098929b9fa1941877ce4393ca89eb08a41 100644 (file)
--- 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 172b2407c172d5747aae7c0aee990f9acba11a6c..643029b05eada9847169a6b316dfe7f9be1469b5 100644 (file)
--- 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 2fd83911542a86a87fffb94db6e0d7bbb66eb6f4..f63a887ef06c5f420308812953ed32880fcfd38e 100644 (file)
--- 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 02c9cb467fb959dcbd4be7123b1167d3eb186302..862a906a060f4998f2eb192e315e68be9cb3552a 100644 (file)
--- 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 58f4f18a518ebe3dac01925fd18f10c1949238b0..3455473010bfd0eb6d33b26623ca865405f25c2f 100644 (file)
--- 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);