From: Andrew Reynolds Date: Wed, 30 Jun 2021 18:09:45 +0000 (-0500) Subject: Do not notify during equality engine initialization (#6817) X-Git-Tag: cvc5-1.0.0~1543 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6e502dbc3def28d0530218a0a2374e9e4c1a946d;p=cvc5.git Do not notify during equality engine initialization (#6817) This is an alternative fix to https://github.com/cvc5/cvc5/pull/6808. This ensures that we do not notify the provided class of an equality engine during initialization. --- diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 338076e78..75294621a 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -107,7 +107,7 @@ EqualityEngine::EqualityEngine(context::Context* context, d_masterEqualityEngine(0), d_context(context), d_done(context, false), - d_notify(s_notifyNone), + d_notify(&s_notifyNone), d_applicationLookupsCount(context, 0), d_nodesCount(context, 0), d_assertedEqualitiesCount(context, 0), @@ -136,7 +136,7 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, d_masterEqualityEngine(0), d_context(context), d_done(context, false), - d_notify(notify), + d_notify(&s_notifyNone), d_applicationLookupsCount(context, 0), d_nodesCount(context, 0), d_assertedEqualitiesCount(context, 0), @@ -154,6 +154,10 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, d_name(name) { init(); + // since init makes notifications (e.g. new eq class for true/false), and + // since the notify class may not be fully constructed yet, we + // don't set up the provided notification class until after initialization. + d_notify = ¬ify; } void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) { @@ -375,7 +379,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { { // Notify e.g. the theory that owns this equality engine that there is a // new equivalence class. - d_notify.eqNotifyNewClass(t); + d_notify->eqNotifyNewClass(t); if (d_constantsAreTriggers && d_isConstant[result]) { // Non-Boolean constants are trigger terms for all tags @@ -497,7 +501,7 @@ bool EqualityEngine::assertEquality(TNode eq, } // notify the theory - d_notify.eqNotifyDisequal(eq[0], eq[1], reason); + d_notify->eqNotifyDisequal(eq[0], eq[1], reason); Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; @@ -555,7 +559,7 @@ bool EqualityEngine::assertEquality(TNode eq, storePropagatedDisequality(aTag, aSharedId, bSharedId); // Notify Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ": notifying " << aTag << " for " << d_nodes[aSharedId] << " != " << d_nodes[bSharedId] << std::endl; - if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) { + if (!d_notify->eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) { break; } } @@ -730,7 +734,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // notify the theory if (doNotify) { - d_notify.eqNotifyMerge(n1, n2); + d_notify->eqNotifyMerge(n1, n2); } // Go through the trigger term disequalities and propagate @@ -787,7 +791,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect class1triggers.d_triggers[i1++]; // since they are both tagged notify of merge EqualityNodeId tag2id = class2triggers.d_triggers[i2++]; - if (!d_notify.eqNotifyTriggerTermEquality( + if (!d_notify->eqNotifyTriggerTermEquality( tag1, d_nodes[tag1id], d_nodes[tag2id], true)) { return false; @@ -1709,11 +1713,11 @@ void EqualityEngine::addTriggerEquality(TNode eq) { // If they are equal or disequal already, no need for the trigger if (areEqual(eq[0], eq[1])) { - d_notify.eqNotifyTriggerPredicate(eq, true); + d_notify->eqNotifyTriggerPredicate(eq, true); skipTrigger = true; } if (areDisequal(eq[0], eq[1], true)) { - d_notify.eqNotifyTriggerPredicate(eq, false); + d_notify->eqNotifyTriggerPredicate(eq, false); skipTrigger = true; } @@ -1752,11 +1756,11 @@ void EqualityEngine::addTriggerPredicate(TNode predicate) { // If it's know already, no need for the trigger if (areEqual(predicate, d_true)) { - d_notify.eqNotifyTriggerPredicate(predicate, true); + d_notify->eqNotifyTriggerPredicate(predicate, true); skipTrigger = true; } if (areEqual(predicate, d_false)) { - d_notify.eqNotifyTriggerPredicate(predicate, false); + d_notify->eqNotifyTriggerPredicate(predicate, false); skipTrigger = true; } @@ -1923,7 +1927,7 @@ void EqualityEngine::propagate() { d_assertedEqualities.push_back(Equality(null_id, null_id)); d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; // Notify - d_notify.eqNotifyConstantTermMerge(d_nodes[t1classId], + d_notify->eqNotifyConstantTermMerge(d_nodes[t1classId], d_nodes[t2classId]); // Empty the queue and exit continue; @@ -2007,7 +2011,7 @@ void EqualityEngine::propagate() { d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId)); } storePropagatedDisequality(THEORY_LAST, lhsId, rhsId); - if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.d_trigger, + if (!d_notify->eqNotifyTriggerPredicate(triggerInfo.d_trigger, triggerInfo.d_polarity)) { d_done = true; @@ -2017,7 +2021,7 @@ void EqualityEngine::propagate() { else { // Equalities are simple - if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.d_trigger, + if (!d_notify->eqNotifyTriggerPredicate(triggerInfo.d_trigger, triggerInfo.d_polarity)) { d_done = true; @@ -2026,7 +2030,7 @@ void EqualityEngine::propagate() { } else { - if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.d_trigger, + if (!d_notify->eqNotifyTriggerPredicate(triggerInfo.d_trigger, triggerInfo.d_polarity)) { d_done = true; @@ -2212,7 +2216,7 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) << "): already have this trigger in class with " << d_nodes[triggerId] << std::endl; if (eqNodeId != triggerId - && !d_notify.eqNotifyTriggerTermEquality( + && !d_notify->eqNotifyTriggerTermEquality( tag, t, d_nodes[triggerId], true)) { d_done = true; @@ -2595,7 +2599,7 @@ bool EqualityEngine::propagateTriggerTermDisequalities( // Store the propagation storePropagatedDisequality(currentTag, myRep, tagRep); // Notify - if (!d_notify.eqNotifyTriggerTermEquality( + if (!d_notify->eqNotifyTriggerTermEquality( currentTag, d_nodes[myRep], d_nodes[tagRep], false)) { d_done = true; diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index c0e7b3478..aec2510f3 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -121,7 +121,7 @@ private: context::CDO d_done; /** The class to notify when a representative changes for a term */ - EqualityEngineNotify& d_notify; + EqualityEngineNotify* d_notify; /** The map of kinds to be treated as function applications */ KindMap d_congruenceKinds;