diff options
25 files changed, 57 insertions, 153 deletions
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 @@ -78,20 +78,12 @@ 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); |