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.

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 479e3400d69f1c491ba3950c8c84f90f550125c6..693b7bd66d4a059ce95838c04210ba132a71fbd7 100644 (file)
--- 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

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e3c14126ae89b373d67fd34b3bf64659a2667cf9..0416d4f01a8571902667d6d39e3cef422e53662a 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1339,6 +1339,7 @@ set(regress_1_tests
   regress1/nl/issue3647.smt2
   regress1/nl/issue3656.smt2
   regress1/nl/issue3803-nl-check-model.smt2
+  regress1/nl/issue3955-ee-double-notify.smt2
   regress1/nl/metitarski-1025.smt2
   regress1/nl/metitarski-3-4.smt2
   regress1/nl/metitarski_3_4_2e.smt2

diff --git a/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 b/test/regress/regress1/nl/issue3955-ee-double-notify.smt2
new file mode 100644 (file)
index 0000000..8aa8793
--- /dev/null
+++ b/test/regress/regress1/nl/issue3955-ee-double-notify.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_UFNRA)\r
+(set-option :snorm-infer-eq true)\r
+(set-info :status sat)\r
+(declare-const r0 Real)\r
+(declare-const r4 Real)\r
+(assert (<= r4 (- (/ r0 r0))))\r
+(check-sat)\r