From: Andrew Reynolds Date: Tue, 22 Jun 2021 17:32:22 +0000 (-0500) Subject: Minor simplification to equality engine notifications (#6726) X-Git-Tag: cvc5-1.0.0~1571 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=525fe1f4f33aca05f5e92b0cc0f3e0c7e6effa8b;p=cvc5.git Minor simplification to equality engine notifications (#6726) This removes the d_performNotify flag from equality engine which was supposedly used to guard a very old dependency concerning notifications during initialization. We are now robust to this and hence the flag can be removed. --- diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 8885abe6b..338076e78 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -88,10 +88,6 @@ void EqualityEngine::init() { d_triggerDatabaseAllocatedSize = 100000; d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize); - //We can't notify during the initialization because it notifies - // QuantifiersEngine.AddTermToDatabase that try to access to the uf - // instantiator that currently doesn't exist. - ScopedBool sb(d_performNotify, false); addTermInternal(d_true); addTermInternal(d_false); @@ -111,7 +107,6 @@ EqualityEngine::EqualityEngine(context::Context* context, d_masterEqualityEngine(0), d_context(context), d_done(context, false), - d_performNotify(true), d_notify(s_notifyNone), d_applicationLookupsCount(context, 0), d_nodesCount(context, 0), @@ -141,7 +136,6 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, d_masterEqualityEngine(0), d_context(context), d_done(context, false), - d_performNotify(true), d_notify(notify), d_applicationLookupsCount(context, 0), d_nodesCount(context, 0), @@ -381,10 +375,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. - if (d_performNotify) - { - d_notify.eqNotifyNewClass(t); - } + d_notify.eqNotifyNewClass(t); if (d_constantsAreTriggers && d_isConstant[result]) { // Non-Boolean constants are trigger terms for all tags @@ -506,9 +497,7 @@ bool EqualityEngine::assertEquality(TNode eq, } // notify the theory - if (d_performNotify) { - 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; @@ -608,7 +597,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // 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()) + if (class1Id == cc1.getFind() && class2Id == cc2.getFind()) { doNotify = true; } @@ -797,11 +786,11 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] = class1triggers.d_triggers[i1++]; // since they are both tagged notify of merge - if (d_performNotify) { - EqualityNodeId tag2id = class2triggers.d_triggers[i2++]; - if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) { - return false; - } + EqualityNodeId tag2id = class2triggers.d_triggers[i2++]; + if (!d_notify.eqNotifyTriggerTermEquality( + tag1, d_nodes[tag1id], d_nodes[tag2id], true)) + { + return false; } // Next tags tag1 = TheoryIdSetUtil::setPop(tags1); @@ -1934,9 +1923,8 @@ void EqualityEngine::propagate() { d_assertedEqualities.push_back(Equality(null_id, null_id)); d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; // Notify - if (d_performNotify) { - d_notify.eqNotifyConstantTermMerge(d_nodes[t1classId], d_nodes[t2classId]); - } + d_notify.eqNotifyConstantTermMerge(d_nodes[t1classId], + d_nodes[t2classId]); // Empty the queue and exit continue; } @@ -1995,7 +1983,8 @@ void EqualityEngine::propagate() { } // Notify the triggers - if (d_performNotify && !d_done) { + if (!d_done) + { for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) { const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggers[trigger_i]]; if (triggerInfo.d_trigger.getKind() == kind::EQUAL) @@ -2217,12 +2206,16 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) TriggerTermSetRef triggerSetRef = d_nodeIndividualTrigger[classId]; if (triggerSetRef != +null_set_id && getTriggerTermSet(triggerSetRef).hasTrigger(tag)) { // If the term already is in the equivalence class that a tagged representative, just notify - if (d_performNotify) { - EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag); - Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << "): already have this trigger in class with " << d_nodes[triggerId] << std::endl; - if (eqNodeId != triggerId && !d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) { - d_done = true; - } + EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag); + Debug("equality::trigger") + << d_name << "::eq::addTriggerTerm(" << t << ", " << tag + << "): already have this trigger in class with " << d_nodes[triggerId] + << std::endl; + if (eqNodeId != triggerId + && !d_notify.eqNotifyTriggerTermEquality( + tag, t, d_nodes[triggerId], true)) + { + d_done = true; } } else { @@ -2602,10 +2595,10 @@ bool EqualityEngine::propagateTriggerTermDisequalities( // Store the propagation storePropagatedDisequality(currentTag, myRep, tagRep); // Notify - if (d_performNotify) { - if (!d_notify.eqNotifyTriggerTermEquality(currentTag, d_nodes[myRep], d_nodes[tagRep], false)) { - d_done = true; - } + 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 024774593..c0e7b3478 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -120,9 +120,6 @@ private: /** If we are done, we don't except any new assertions */ context::CDO d_done; - /** Whether to notify or not (temporarily disabled on equality checks) */ - bool d_performNotify; - /** The class to notify when a representative changes for a term */ EqualityEngineNotify& d_notify;