From 08431f8a51a62d02e3d3911db2e7754862953320 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 Mar 2020 01:55:18 -0500 Subject: [PATCH] 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. --- src/theory/uf/equality_engine.cpp | 68 ++++++++++++------- test/regress/CMakeLists.txt | 1 + .../nl/issue3955-ee-double-notify.smt2 | 7 ++ 3 files changed, 50 insertions(+), 26 deletions(-) create mode 100644 test/regress/regress1/nl/issue3955-ee-double-notify.smt2 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 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e3c14126a..0416d4f01 100644 --- 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 index 000000000..8aa8793df --- /dev/null +++ b/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_UFNRA) +(set-option :snorm-infer-eq true) +(set-info :status sat) +(declare-const r0 Real) +(declare-const r4 Real) +(assert (<= r4 (- (/ r0 r0)))) +(check-sat) -- 2.30.2