Fix double notify in equality engine (#4036)

Fixes #3955.

Previously we were getting two calls to notifyNewEqClass from the equality engine for new application nodes, since the notification was being done in an internal call to newNode(...). The proper place to call this is in addTermInternal(...) which is called only once per Node per SAT context.

This bug potentially impacted some performance (due to redundant calls), and also broke the contract that notifyNewEqClass should only be called once per node per SAT context. In most cases, this was being handled in a benign way by theory solvers, although an assertion was failing in EqualityQuery, which is fixed by this PR.

A block of code changed indentation in this commit.

1 files changed, 42 insertions, 26 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 479e3400d..693b7bd66 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -248,11 +248,6 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
 
   Debug("equality") << d_name << "::eq::newNode(" << node << ") => " << newId << std::endl;
 
-  // notify e.g. the theory that owns this equality engine.
-  if (d_performNotify) {
-    d_notify.eqNotifyNewClass(node);
-  }
-
   return newId;
 }
 
@@ -298,7 +293,9 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
 
   EqualityNodeId result;
 
-  if (t.getKind() == kind::EQUAL) {
+  Kind tk = t.getKind();
+  if (tk == kind::EQUAL)
+  {
     addTermInternal(t[0]);
     addTermInternal(t[1]);
     EqualityNodeId t0id = getNodeId(t[0]);
@@ -306,13 +303,15 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
     result = newApplicationNode(t, t0id, t1id, APP_EQUALITY);
     d_isInternal[result] = false;
     d_isConstant[result] = false;
-  } else if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()]) {
+  }
+  else if (t.getNumChildren() > 0 && d_congruenceKinds[tk])
+  {
     TNode tOp = t.getOperator();
     // Add the operator
-    addTermInternal(tOp, !isExternalOperatorKind(t.getKind()));
+    addTermInternal(tOp, !isExternalOperatorKind(tk));
     result = getNodeId(tOp);
     // Add all the children and Curryfy
-    bool isInterpreted = isInterpretedFunctionKind(t.getKind());
+    bool isInterpreted = isInterpretedFunctionKind(tk);
     for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
       // Add the child
       addTermInternal(t[i]);
@@ -333,7 +332,9 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
         }
       }
     }
-  } else {
+  }
+  else
+  {
     // Otherwise we just create the new id
     result = newNode(t);
     // Is this an operator
@@ -341,26 +342,41 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
     d_isConstant[result] = !isOperator && t.isConst();
   }
 
-  if (t.getKind() == kind::EQUAL) {
+  if (tk == kind::EQUAL)
+  {
     // We set this here as this only applies to actual terms, not the
     // intermediate application terms
     d_isEquality[result] = true;
-  } else if (d_constantsAreTriggers && d_isConstant[result]) {
-    // Non-Boolean constants are trigger terms for all tags
-    EqualityNodeId tId = getNodeId(t);
-    // Setup the new set
-    Theory::Set newSetTags = 0;
-    EqualityNodeId newSetTriggers[THEORY_LAST];
-    unsigned newSetTriggersSize = THEORY_LAST;
-    for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) {
-      newSetTags = Theory::setInsert(currentTheory, newSetTags);
-      newSetTriggers[currentTheory] = tId;
+  }
+  else
+  {
+    // Notify e.g. the theory that owns this equality engine that there is a
+    // new equivalence class.
+    if (d_performNotify)
+    {
+      d_notify.eqNotifyNewClass(t);
+    }
+    if (d_constantsAreTriggers && d_isConstant[result])
+    {
+      // Non-Boolean constants are trigger terms for all tags
+      EqualityNodeId tId = getNodeId(t);
+      // Setup the new set
+      Theory::Set newSetTags = 0;
+      EqualityNodeId newSetTriggers[THEORY_LAST];
+      unsigned newSetTriggersSize = THEORY_LAST;
+      for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST;
+           ++currentTheory)
+      {
+        newSetTags = Theory::setInsert(currentTheory, newSetTags);
+        newSetTriggers[currentTheory] = tId;
+      }
+      // Add it to the list for backtracking
+      d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id));
+      d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
+      // Mark the the new set as a trigger
+      d_nodeIndividualTrigger[tId] =
+          newTriggerTermSet(newSetTags, newSetTriggers, newSetTriggersSize);
     }
-    // Add it to the list for backtracking
-    d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id));
-    d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
-    // Mark the the new set as a trigger
-    d_nodeIndividualTrigger[tId] = newTriggerTermSet(newSetTags, newSetTriggers, newSetTriggersSize);
   }
 
   // If this is not an internal node, add it to the master