diff options
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 8 | ||||
| -rw-r--r-- | 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 |