diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-24 17:44:52 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-24 22:44:52 +0000 |
commit | 77b75a69e51b742e1448d754b6886c10ef76e79f (patch) | |
tree | b3c4f9793fc0db34494e1d914286e32a1bd4c04c /src/theory/quantifiers/ematching | |
parent | cfe207563479a1e9e13d52bdd93446a8c816636a (diff) |
Use inference manager to access intantiate utility instead of quantifiers engine (#6198)
Towards breaking dependencies on quantifers engine.
Diffstat (limited to 'src/theory/quantifiers/ematching')
-rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/im_generator.h | 32 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator_simple.h | 16 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 2 |
4 files changed, 30 insertions, 34 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 6206b24a7..4cdce940e 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_rewriter.h" @@ -236,7 +237,6 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id) d_lchildren.clear(); d_arg_to_arg_rep.clear(); d_arg_vector.clear(); - QuantifiersState& qs = d_quantEngine->getState(); for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs) { TNode var = ha.first; @@ -288,9 +288,9 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id) } else if (!itf->second.isNull()) { - if (!qs.areEqual(itf->second, args[k])) + if (!d_qstate.areEqual(itf->second, args[k])) { - if (!d_quantEngine->getTermDatabase()->isEntailed( + if (!d_treg.getTermDatabase()->isEntailed( itf->second.eqNode(args[k]), true)) { fixed_vals[k] = Node::null(); @@ -323,7 +323,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id) { if (!itf->second.isNull()) { - Node r = qs.getRepresentative(itf->second); + Node r = d_qstate.getRepresentative(itf->second); std::map<Node, unsigned>::iterator itfr = arg_to_rep.find(r); if (itfr != arg_to_rep.end()) { @@ -375,7 +375,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id) else { // do not run higher-order matching - return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id); + return d_qim.getInstantiate()->addInstantiation(d_quant, m, id); } } @@ -389,7 +389,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, if (var_index == d_ho_var_list.size()) { // we now have an instantiation to try - return d_quantEngine->getInstantiate()->addInstantiation( + return d_qim.getInstantiate()->addInstantiation( d_quant, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_HO); } else @@ -476,7 +476,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl; uint64_t numLemmas = 0; // this forces expansion of APPLY_UF terms to curried HO_APPLY chains - TermDb* tdb = d_quantEngine->getTermDatabase(); + TermDb* tdb = d_treg.getTermDatabase(); unsigned size = tdb->getNumOperators(); NodeManager* nm = NodeManager::currentNM(); for (unsigned j = 0; j < size; j++) diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h index 0d0f9498d..efc65cdef 100644 --- a/src/theory/quantifiers/ematching/im_generator.h +++ b/src/theory/quantifiers/ematching/im_generator.h @@ -36,22 +36,22 @@ namespace inst { class Trigger; /** IMGenerator class -* -* Virtual base class for generating InstMatch objects, which correspond to -* quantifier instantiations. The main use of this class is as a backend utility -* to Trigger (see theory/quantifiers/ematching/trigger.h). -* -* Some functions below take as argument a pointer to the current quantifiers -* engine, which is used for making various queries about what terms and -* equalities exist in the current context. -* -* Some functions below take a pointer to a parent Trigger object, which is used -* to post-process and finalize the instantiations through -* sendInstantiation(...), where the parent trigger will make calls to -* qe->getInstantiate()->addInstantiation(...). The latter function is the entry -* point in which instantiate lemmas are enqueued to be sent on the output -* channel. -*/ + * + * Virtual base class for generating InstMatch objects, which correspond to + * quantifier instantiations. The main use of this class is as a backend utility + * to Trigger (see theory/quantifiers/ematching/trigger.h). + * + * Some functions below take as argument a pointer to the current quantifiers + * engine, which is used for making various queries about what terms and + * equalities exist in the current context. + * + * Some functions below take a pointer to a parent Trigger object, which is used + * to post-process and finalize the instantiations through + * sendInstantiation(...), where the parent trigger will make calls to + * Instantiate::addInstantiation(...). The latter function is the entry + * point in which instantiate lemmas are enqueued to be sent on the output + * channel. + */ class IMGenerator { public: IMGenerator(Trigger* tparent); diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h index ad48d9c91..6ae2f915b 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h @@ -41,10 +41,6 @@ namespace inst { * The implementation traverses the term indices in TermDatabase for adding * instantiations, which is more efficient than the techniques required for * handling non-simple single triggers. - * - * In contrast to other instantiation generators, it does not call - * IMGenerator::sendInstantiation and for performance reasons instead calls - * qe->getInstantiate()->addInstantiation(...) directly. */ class InstMatchGeneratorSimple : public IMGenerator { @@ -88,12 +84,12 @@ class InstMatchGeneratorSimple : public IMGenerator std::map<size_t, int> d_var_num; /** add instantiations, helper function. * - * m is the current match we are building, - * addedLemmas is the number of lemmas we have added via calls to - * qe->getInstantiate()->aaddInstantiation(...), - * argIndex is the argument index in d_match_pattern we are currently - * matching, - * tat is the term index we are currently traversing. + * @param m the current match we are building, + * @param addedLemmas the number of lemmas we have added via calls to + * Instantiate::addInstantiation(...), + * @param argIndex the argument index in d_match_pattern we are currently + * matching, + * @param tat the term index we are currently traversing. */ void addInstantiations(InstMatch& m, uint64_t& addedLemmas, diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index af0a0bfbc..c93e1a99b 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -154,7 +154,7 @@ uint64_t Trigger::addInstantiations() bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id) { - return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id); + return d_qim.getInstantiate()->addInstantiation(d_quant, m, id); } bool Trigger::sendInstantiation(InstMatch& m, InferenceId id) |