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.

2 files changed, 22 insertions, 18 deletions

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 = &notify;
 }
 
 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<bool> 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;