From 42cd0a7bcbe993870d76d8cc9db7acc0a9ae70f9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 14 Aug 2020 13:07:17 -0500 Subject: 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. --- src/theory/uf/equality_engine.cpp | 14 ++++++-------- src/theory/uf/equality_engine_notify.h | 13 ++----------- src/theory/uf/theory_uf.cpp | 9 ++------- src/theory/uf/theory_uf.h | 18 +++++------------- 4 files changed, 15 insertions(+), 39 deletions(-) (limited to 'src/theory/uf') 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); -- cgit v1.2.3