diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-28 13:27:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-28 13:27:27 -0600 |
commit | 3234db430074e278258e6d687c07146a59769a92 (patch) | |
tree | 17db55e1ff335c3998e1c4e172d174dc9f6e3b21 /src/theory/quantifiers/inst_match_trie.cpp | |
parent | 4cd2d73366aba081a38900ddc2f4f172ce9ed2f8 (diff) |
Use standard equality engine information in quantifiers state (#5824)
This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.
This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.
Diffstat (limited to 'src/theory/quantifiers/inst_match_trie.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_match_trie.cpp | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index aaf7cb4bc..0bd5000f1 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -52,12 +52,11 @@ bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe, } if (modEq) { + quantifiers::QuantifiersState& qs = qe->getState(); // check modulo equality if any other instantiation match exists - if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n)) + if (!n.isNull() && qs.hasTerm(n)) { - eq::EqClassIterator eqc( - qe->getEqualityQuery()->getEngine()->getRepresentative(n), - qe->getEqualityQuery()->getEngine()); + eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine()); while (!eqc.isFinished()) { Node en = (*eqc); @@ -331,11 +330,10 @@ bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe, if (modEq) { // check modulo equality if any other instantiation match exists - if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n)) + quantifiers::QuantifiersState& qs = qe->getState(); + if (!n.isNull() && qs.hasTerm(n)) { - eq::EqClassIterator eqc( - qe->getEqualityQuery()->getEngine()->getRepresentative(n), - qe->getEqualityQuery()->getEngine()); + eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine()); while (!eqc.isFinished()) { Node en = (*eqc); |