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 8885abe6bddabb6d420f22d574fd46d4d38efb0f..338076e78c56e3bd70ec85874e0e9f29b4e95018 100644 (file)
--- 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 024774593fcef00058960ed2d6a178e140afaf81..c0e7b347865465127470b6d6b7de135d30a9da5c 100644 (file)
--- 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<bool> 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;