From fb6acf659fbf69327f8044e35e6919c1243bc848 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 9 Feb 2021 16:09:54 -0600 Subject: [PATCH] Eliminating dependencies from inst utils (#5882) Towards eliminating dependence on QuantifierEngine from inst_match_trie. --- .../ematching/inst_match_generator_multi.cpp | 2 +- src/theory/quantifiers/inst_match_trie.cpp | 24 ++++---- src/theory/quantifiers/inst_match_trie.h | 56 +++++++++---------- src/theory/quantifiers/instantiate.cpp | 9 ++- 4 files changed, 43 insertions(+), 48 deletions(-) diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index 371bc3378..a0114ba80 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -191,7 +191,7 @@ void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe, uint64_t& addedLemmas) { // see if these produce new matches - d_children_trie[fromChildIndex].addInstMatch(qe, d_quant, m); + d_children_trie[fromChildIndex].addInstMatch(qe->getState(), d_quant, m); // possibly only do the following if we know that new matches will be // produced? the issue is that instantiations are filtered in quantifiers // engine, and so there is no guarentee that diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index 0bd5000f1..0eef03d9d 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" @@ -25,7 +26,7 @@ namespace CVC4 { namespace theory { namespace inst { -bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe, +bool InstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs, Node f, std::vector& m, bool modEq, @@ -44,7 +45,7 @@ bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe, if (it != d_data.end()) { bool ret = - it->second.addInstMatch(qe, f, m, modEq, imtio, onlyExist, index + 1); + it->second.addInstMatch(qs, f, m, modEq, imtio, onlyExist, index + 1); if (!onlyExist || !ret) { return ret; @@ -52,7 +53,6 @@ bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe, } if (modEq) { - quantifiers::QuantifiersState& qs = qe->getState(); // check modulo equality if any other instantiation match exists if (!n.isNull() && qs.hasTerm(n)) { @@ -66,7 +66,7 @@ bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe, if (itc != d_data.end()) { if (itc->second.addInstMatch( - qe, f, m, modEq, imtio, true, index + 1)) + qs, f, m, modEq, imtio, true, index + 1)) { return false; } @@ -78,7 +78,7 @@ bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe, } if (!onlyExist) { - d_data[n].addInstMatch(qe, f, m, modEq, imtio, false, index + 1); + d_data[n].addInstMatch(qs, f, m, modEq, imtio, false, index + 1); } return true; } @@ -291,10 +291,9 @@ CDInstMatchTrie::~CDInstMatchTrie() d_data.clear(); } -bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe, +bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs, Node f, std::vector& m, - context::Context* c, bool modEq, unsigned index, bool onlyExist) @@ -320,8 +319,7 @@ bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe, std::map::iterator it = d_data.find(n); if (it != d_data.end()) { - bool ret = - it->second->addInstMatch(qe, f, m, c, modEq, index + 1, onlyExist); + bool ret = it->second->addInstMatch(qs, f, m, modEq, index + 1, onlyExist); if (!onlyExist || !ret) { return reset || ret; @@ -330,7 +328,6 @@ bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe, if (modEq) { // check modulo equality if any other instantiation match exists - quantifiers::QuantifiersState& qs = qe->getState(); if (!n.isNull() && qs.hasTerm(n)) { eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine()); @@ -342,7 +339,7 @@ bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe, std::map::iterator itc = d_data.find(en); if (itc != d_data.end()) { - if (itc->second->addInstMatch(qe, f, m, c, modEq, index + 1, true)) + if (itc->second->addInstMatch(qs, f, m, modEq, index + 1, true)) { return false; } @@ -355,11 +352,10 @@ bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe, if (!onlyExist) { - // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); - CDInstMatchTrie* imt = new CDInstMatchTrie(c); + CDInstMatchTrie* imt = new CDInstMatchTrie(qs.getUserContext()); Assert(d_data.find(n) == d_data.end()); d_data[n] = imt; - imt->addInstMatch(qe, f, m, c, modEq, index + 1, false); + imt->addInstMatch(qs, f, m, modEq, index + 1, false); } return true; } diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index c978a6952..51b19f2ef 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -29,6 +29,10 @@ namespace theory { class QuantifiersEngine; +namespace { +class QuantifiersState; +} + namespace inst { /** trie for InstMatch objects @@ -57,26 +61,26 @@ class InstMatchTrie * The domain of m is the bound variables of quantified formula q. * It returns true if (the suffix) of m exists in this trie. * If modEq is true, we check for duplication modulo equality the current - * equalities in the active equality engine of qe. + * equalities in the equality engine of qs. */ - bool existsInstMatch(QuantifiersEngine* qe, + bool existsInstMatch(quantifiers::QuantifiersState& qs, Node q, InstMatch& m, bool modEq = false, ImtIndexOrder* imtio = NULL, unsigned index = 0) { - return !addInstMatch(qe, q, m, modEq, imtio, true, index); + return !addInstMatch(qs, q, m, modEq, imtio, true, index); } /** exists inst match, vector version */ - bool existsInstMatch(QuantifiersEngine* qe, + bool existsInstMatch(quantifiers::QuantifiersState& qs, Node q, std::vector& m, bool modEq = false, ImtIndexOrder* imtio = NULL, unsigned index = 0) { - return !addInstMatch(qe, q, m, modEq, imtio, true, index); + return !addInstMatch(qs, q, m, modEq, imtio, true, index); } /** add inst match * @@ -84,9 +88,9 @@ class InstMatchTrie * trie, and returns true if and only if m did not already occur in this trie. * The domain of m is the bound variables of quantified formula q. * If modEq is true, we check for duplication modulo equality the current - * equalities in the active equality engine of qe. + * equalities in the equality engine of qs. */ - bool addInstMatch(QuantifiersEngine* qe, + bool addInstMatch(quantifiers::QuantifiersState& qs, Node q, InstMatch& m, bool modEq = false, @@ -94,10 +98,10 @@ class InstMatchTrie bool onlyExist = false, unsigned index = 0) { - return addInstMatch(qe, q, m.d_vals, modEq, imtio, onlyExist, index); + return addInstMatch(qs, q, m.d_vals, modEq, imtio, onlyExist, index); } /** add inst match, vector version */ - bool addInstMatch(QuantifiersEngine* qe, + bool addInstMatch(quantifiers::QuantifiersState& qs, Node f, std::vector& m, bool modEq = false, @@ -235,27 +239,25 @@ class CDInstMatchTrie * The domain of m is the bound variables of quantified formula q. * It returns true if (the suffix) of m exists in this trie. * If modEq is true, we check for duplication modulo equality the current - * equalities in the active equality engine of qe. + * equalities in the equality engine of qs. * It additionally takes a context c, for which the entry is valid in. */ - bool existsInstMatch(QuantifiersEngine* qe, + bool existsInstMatch(quantifiers::QuantifiersState& qs, Node q, InstMatch& m, - context::Context* c, bool modEq = false, unsigned index = 0) { - return !addInstMatch(qe, q, m, c, modEq, index, true); + return !addInstMatch(qs, q, m, modEq, index, true); } /** exists inst match, vector version */ - bool existsInstMatch(QuantifiersEngine* qe, + bool existsInstMatch(quantifiers::QuantifiersState& qs, Node q, std::vector& m, - context::Context* c, bool modEq = false, unsigned index = 0) { - return !addInstMatch(qe, q, m, c, modEq, index, true); + return !addInstMatch(qs, q, m, modEq, index, true); } /** add inst match * @@ -263,24 +265,22 @@ class CDInstMatchTrie * trie, and returns true if and only if m did not already occur in this trie. * The domain of m is the bound variables of quantified formula q. * If modEq is true, we check for duplication modulo equality the current - * equalities in the active equality engine of qe. + * equalities in the equality engine of qs. * It additionally takes a context c, for which the entry is valid in. */ - bool addInstMatch(QuantifiersEngine* qe, + bool addInstMatch(quantifiers::QuantifiersState& qs, Node q, InstMatch& m, - context::Context* c, bool modEq = false, unsigned index = 0, bool onlyExist = false) { - return addInstMatch(qe, q, m.d_vals, c, modEq, index, onlyExist); + return addInstMatch(qs, q, m.d_vals, modEq, index, onlyExist); } /** add inst match, vector version */ - bool addInstMatch(QuantifiersEngine* qe, + bool addInstMatch(quantifiers::QuantifiersState& qs, Node q, std::vector& m, - context::Context* c, bool modEq = false, unsigned index = 0, bool onlyExist = false); @@ -413,27 +413,27 @@ class InstMatchTrieOrdered * * This method returns true if the match m was not previously added to this * class. If modEq is true, we consider duplicates modulo the current - * equalities stored in the active equality engine of quantifiers engine. + * equalities stored in the equality engine of qs. */ - bool addInstMatch(QuantifiersEngine* qe, + bool addInstMatch(quantifiers::QuantifiersState& qs, Node q, InstMatch& m, bool modEq = false) { - return d_imt.addInstMatch(qe, q, m, modEq, d_imtio); + return d_imt.addInstMatch(qs, q, m, modEq, d_imtio); } /** returns true if this trie contains m * * This method returns true if the match m exists in this * class. If modEq is true, we consider duplicates modulo the current - * equalities stored in the active equality engine of quantifiers engine. + * equalities stored in the equality engine of qs. */ - bool existsInstMatch(QuantifiersEngine* qe, + bool existsInstMatch(quantifiers::QuantifiersState& qs, Node q, InstMatch& m, bool modEq = false) { - return d_imt.existsInstMatch(qe, q, m, modEq, d_imtio); + return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio); } private: diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 4db53c4b7..361796735 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -419,8 +419,7 @@ bool Instantiate::existsInstantiation(Node q, d_c_inst_match_trie.find(q); if (it != d_c_inst_match_trie.end()) { - return it->second->existsInstMatch( - d_qe, q, terms, d_qstate.getUserContext(), modEq); + return it->second->existsInstMatch(d_qstate, q, terms, modEq); } } else @@ -429,7 +428,7 @@ bool Instantiate::existsInstantiation(Node q, d_inst_match_trie.find(q); if (it != d_inst_match_trie.end()) { - return it->second.existsInstMatch(d_qe, q, terms, modEq); + return it->second.existsInstMatch(d_qstate, q, terms, modEq); } } return false; @@ -519,10 +518,10 @@ bool Instantiate::recordInstantiationInternal(Node q, d_c_inst_match_trie[q] = imt; } d_c_inst_match_trie_dom.insert(q); - return imt->addInstMatch(d_qe, q, terms, d_qstate.getUserContext(), modEq); + return imt->addInstMatch(d_qstate, q, terms, modEq); } Trace("inst-add-debug") << "Adding into inst trie" << std::endl; - return d_inst_match_trie[q].addInstMatch(d_qe, q, terms, modEq); + return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms, modEq); } bool Instantiate::removeInstantiationInternal(Node q, std::vector& terms) -- 2.30.2