From 9ea213066b989a8154b1ebd40ebea3bc7e18c42d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 21 Aug 2020 17:53:46 -0500 Subject: [PATCH] Limit trigger terms to shared terms in arrays (#4932) There is a non-standard use of trigger terms in the array theory via `EqualityEngine::addTriggerTerm`. Trigger terms are only supposed to be shared terms, and are added to the equality engine for the sake of propagating equalities between shared terms. The array theory does two non-standard things: (1) it registers (possibly) non-shared terms as triggers in its `preRegisterInternal` method, (2) it filters propagations between anything except non-shared arrays in its `eqNotifyTriggerTermEquality` method. The latter is only necessary because of the former. It is unnecessary to do *either* of these things. Instead, the array theory should simply add the terms to the equality engine (as non-triggers) during preRegisterInternal. Note that it additionally correctly adds trigger terms in its `notifySharedTerm` method. With this commit, the array theory uses the equality engine (wrt propagation) in a standard way. --- src/theory/arrays/theory_arrays.cpp | 8 ++++---- src/theory/arrays/theory_arrays.h | 14 +------------- 2 files changed, 5 insertions(+), 17 deletions(-) diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index d659aff11..34c4fd156 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -721,7 +721,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) if (node.getType().isArray()) { d_mayEqualEqualityEngine.addTerm(node); - d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS); + d_equalityEngine->addTerm(node); } else { @@ -765,7 +765,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) { break; } - d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS); + d_equalityEngine->addTerm(node); TNode a = d_equalityEngine->getRepresentative(node[0]); @@ -828,7 +828,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) d_infoMap.setConstArr(node, node); d_mayEqualEqualityEngine.addTerm(node); Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node); - d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS); + d_equalityEngine->addTerm(node); d_defValues[node] = defaultValue; break; } @@ -837,7 +837,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) if (node.getType().isArray()) { // The may equal needs the node d_mayEqualEqualityEngine.addTerm(node); - d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS); + d_equalityEngine->addTerm(node); Assert(d_equalityEngine->getSize(node) == 1); } else { diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 24ebb4916..a1fa19631 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -317,22 +317,10 @@ class TheoryArrays : public Theory { { Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl; if (value) { - if (t1.getType().isArray()) { - if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) { - return true; - } - } // Propagate equality between shared terms return d_arrays.propagateLit(t1.eqNode(t2)); - } else { - if (t1.getType().isArray()) { - if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) { - return true; - } - } - return d_arrays.propagateLit(t1.eqNode(t2).notNode()); } - return true; + return d_arrays.propagateLit(t1.eqNode(t2).notNode()); } void eqNotifyConstantTermMerge(TNode t1, TNode t2) override -- 2.30.2