diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-28 16:50:08 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-28 21:50:08 +0000 |
commit | 48a58687cd7a5b3d1e69153b2178ba535f1e6724 (patch) | |
tree | ff0b4c493164b5203a0d0783b9d511b99b3e7bc8 /src | |
parent | 25e124deb3c69256b35641cd1055b5328b309bf6 (diff) |
Minor changes to arrays in preparation for central equality engine (#6917)
Makes arrays more robust to the order in which terms can be added to the equality engine vs. when they are preregistered.
We should probably performance test this.
FYI @barrettcw
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 20 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 5 |
2 files changed, 16 insertions, 9 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 8fa7e0fd3..7a764feba 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -646,7 +646,9 @@ void TheoryArrays::preRegisterTermInternal(TNode node) { return; } - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) + << "TheoryArrays::preRegisterTerm(" << node << ")" + << std::endl; Kind nk = node.getKind(); if (nk == kind::EQUAL) { @@ -655,13 +657,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node) d_equalityEngine->addTriggerPredicate(node); return; } - else if (d_equalityEngine->hasTerm(node)) - { - // Invariant: array terms should be preregistered before being added to the equality engine - Assert(nk != kind::SELECT - || d_isPreRegistered.find(node) != d_isPreRegistered.end()); - return; - } // add to equality engine and the may equality engine TypeNode nodeType = node.getType(); if (nodeType.isArray()) @@ -676,6 +671,15 @@ void TheoryArrays::preRegisterTermInternal(TNode node) } d_mayEqualEqualityEngine.addTerm(node); } + if (d_equalityEngine->hasTerm(node)) + { + // Notice that array terms may be added to its equality engine before + // being preregistered in the central equality engine architecture. + // Prior to this, an assertion in this case was: + // Assert(nk != kind::SELECT + // || d_isPreRegistered.find(node) != d_isPreRegistered.end()); + return; + } d_equalityEngine->addTerm(node); switch (node.getKind()) diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index c85b382e4..772fc1b79 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -334,7 +334,10 @@ class TheoryArrays : public Theory { d_arrays.conflict(t1, t2); } - void eqNotifyNewClass(TNode t) override {} + void eqNotifyNewClass(TNode t) override + { + d_arrays.preRegisterTermInternal(t); + } void eqNotifyMerge(TNode t1, TNode t2) override { if (t1.getType().isArray()) { |