diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-17 13:34:54 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-17 13:34:54 -0600 |
commit | 0f03dbb1378354adcfef635a93f8b13987c2d983 (patch) | |
tree | 6c6dcc0e806b0867d19d01cb045a5a50764bf0e0 /src/theory/quantifiers/ematching | |
parent | d107bf9b8b4dd206580681e601a033742029ec79 (diff) |
Move methods from term util to quantifiers registry (#5916)
Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.
Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.
Diffstat (limited to 'src/theory/quantifiers/ematching')
13 files changed, 54 insertions, 34 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 0ab2988d2..4c606a273 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -17,7 +17,6 @@ #include "theory/quantifiers/ematching/ho_trigger.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_rewriter.h" #include "util/hash.h" @@ -31,10 +30,11 @@ namespace inst { HigherOrderTrigger::HigherOrderTrigger( QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node q, std::vector<Node>& nodes, std::map<Node, std::vector<Node> >& ho_apps) - : Trigger(qe, qim, q, nodes), d_ho_var_apps(ho_apps) + : Trigger(qe, qim, qr, q, nodes), d_ho_var_apps(ho_apps) { NodeManager* nm = NodeManager::currentNM(); // process the higher-order variable applications @@ -201,11 +201,10 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) // get substitution corresponding to m std::vector<TNode> vars; std::vector<TNode> subs; - quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil(); for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++) { subs.push_back(m.d_vals[i]); - vars.push_back(tutil->getInstantiationConstant(d_quant, i)); + vars.push_back(d_qreg.getInstantiationConstant(d_quant, i)); } Trace("ho-unif-debug") << "Run higher-order unification..." << std::endl; diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index e424f69d1..af7020bfc 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -94,6 +94,7 @@ class HigherOrderTrigger : public Trigger private: HigherOrderTrigger(QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node q, std::vector<Node>& nodes, std::map<Node, std::vector<Node> >& ho_apps); diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index a0114ba80..4f393bc4f 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -238,8 +238,6 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, if (trieIndex < iio->d_order.size()) { size_t curr_index = iio->d_order[trieIndex]; - // Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant, - // curr_index ); Node n = m.get(curr_index); if (n.isNull()) { diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp index fc85703c0..fe771b4e7 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy.cpp @@ -22,8 +22,9 @@ namespace quantifiers { InstStrategy::InstStrategy(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : d_quantEngine(qe), d_qstate(qs), d_qim(qim) + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr) { } InstStrategy::~InstStrategy() {} diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index b9d0aa745..1455ce0c5 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -31,6 +31,7 @@ namespace quantifiers { class QuantifiersState; class QuantifiersInferenceManager; +class QuantifiersRegistry; /** A status response to process */ enum class InstStrategyStatus @@ -49,7 +50,8 @@ class InstStrategy public: InstStrategy(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim); + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr); virtual ~InstStrategy(); /** presolve */ virtual void presolve(); @@ -72,6 +74,8 @@ class InstStrategy QuantifiersState& d_qstate; /** The quantifiers inference manager object */ QuantifiersInferenceManager& d_qim; + /** The quantifiers registry */ + QuantifiersRegistry& d_qreg; }; /* class InstStrategy */ } // namespace quantifiers diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 90d8de128..2a1e38c3c 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -62,8 +62,9 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantRelevance* qr) - : InstStrategy(qe, qs, qim), d_quant_rel(qr) + QuantifiersRegistry& qr, + QuantRelevance* qrlv) + : InstStrategy(qe, qs, qim, qr), d_quant_rel(qrlv) { //how to select trigger terms d_tr_strategy = options::triggerSelMode(); @@ -283,6 +284,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ { tr = Trigger::mkTrigger(d_quantEngine, d_qim, + d_qreg, f, patTerms[0], false, @@ -320,6 +322,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ // will possibly want to get an old trigger tr = Trigger::mkTrigger(d_quantEngine, d_qim, + d_qreg, f, patTerms, false, @@ -362,6 +365,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_single_trigger_gen[patTerms[index]] = true; Trigger* tr2 = Trigger::mkTrigger(d_quantEngine, d_qim, + d_qreg, f, patTerms[index], false, @@ -390,7 +394,6 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) bool ntrivTriggers = options::relationalTriggers(); std::vector<Node> patTermsF; std::map<Node, inst::TriggerTermInfo> tinfo; - TermUtil* tu = d_quantEngine->getTermUtil(); NodeManager* nm = NodeManager::currentNM(); // well-defined function: can assume LHS is only pattern if (options::quantFunWellDefined()) @@ -398,7 +401,7 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) Node hd = QuantAttributes::getFunDefHead(f); if (!hd.isNull()) { - hd = tu->substituteBoundVariablesToInstConstants(hd, f); + hd = d_qreg.substituteBoundVariablesToInstConstants(hd, f); patTermsF.push_back(hd); tinfo[hd].init(f, hd); } @@ -406,7 +409,7 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) // otherwise, use algorithm for collecting pattern terms if (patTermsF.empty()) { - Node bd = tu->getInstConstantBody(f); + Node bd = d_qreg.getInstConstantBody(f); PatternTermSelector pts(f, d_tr_strategy, d_user_no_gen[f], true); pts.collect(bd, patTermsF, tinfo); if (ntrivTriggers) @@ -486,7 +489,7 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) std::vector<Node> vcs[2]; for (size_t i = 0, nchild = f[0].getNumChildren(); i < nchild; i++) { - Node ic = tu->getInstantiationConstant(f, i); + Node ic = d_qreg.getInstantiationConstant(f, i); vcs[vcMap.find(ic) == vcMap.end() ? 0 : 1].push_back(f[0][i]); } for (size_t i = 0; i < 2; i++) @@ -621,8 +624,7 @@ void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) { NodeManager* nm = NodeManager::currentNM(); // partial trigger : generate implication to mark user pattern Node pat = - d_quantEngine->getTermUtil()->substituteInstConstantsToBoundVariables( - tr->getInstPattern(), q); + d_qreg.substituteInstConstantsToBoundVariables(tr->getInstPattern(), q); Node ipl = nm->mkNode(INST_PATTERN_LIST, pat); Node qq = nm->mkNode(FORALL, d_vc_partition[1][q], diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index 81b40f067..6170d3067 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -88,7 +88,8 @@ class InstStrategyAutoGenTriggers : public InstStrategy InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantRelevance* qr); + QuantifiersRegistry& qr, + QuantRelevance* qrlv); ~InstStrategyAutoGenTriggers() {} /** get auto-generated trigger */ diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index cf6405b38..ca2f1bdc5 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -27,8 +27,9 @@ namespace quantifiers { InstStrategyUserPatterns::InstStrategyUserPatterns( QuantifiersEngine* ie, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : InstStrategy(ie, qs, qim) + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : InstStrategy(ie, qs, qim, qr) { } InstStrategyUserPatterns::~InstStrategyUserPatterns() {} @@ -105,8 +106,13 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q, std::vector<std::vector<Node> >& ugw = d_user_gen_wait[q]; for (size_t i = 0, usize = ugw.size(); i < usize; i++) { - Trigger* t = Trigger::mkTrigger( - d_quantEngine, d_qim, q, ugw[i], true, Trigger::TR_RETURN_NULL); + Trigger* t = Trigger::mkTrigger(d_quantEngine, + d_qim, + d_qreg, + q, + ugw[i], + true, + Trigger::TR_RETURN_NULL); if (t) { d_user_gen[q].push_back(t); @@ -165,7 +171,7 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) return; } Trigger* t = Trigger::mkTrigger( - d_quantEngine, d_qim, q, nodes, true, Trigger::TR_MAKE_NEW); + d_quantEngine, d_qim, d_qreg, q, nodes, true, Trigger::TR_MAKE_NEW); if (t) { d_user_gen[q].push_back(t); diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h index 996adc444..1cad77fef 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -36,7 +36,8 @@ class InstStrategyUserPatterns : public InstStrategy public: InstStrategyUserPatterns(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim); + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr); ~InstStrategyUserPatterns(); /** add pattern */ void addUserPattern(Node q, Node pat); diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 50d91a1e1..3e344f7fb 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -53,13 +53,13 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe, // user-provided patterns if (options::userPatternsQuant() != options::UserPatMode::IGNORE) { - d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim)); + d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr)); d_instStrategies.push_back(d_isup.get()); } // auto-generated patterns d_i_ag.reset(new InstStrategyAutoGenTriggers( - d_quantEngine, qs, qim, d_quant_rel.get())); + d_quantEngine, qs, qim, qr, d_quant_rel.get())); d_instStrategies.push_back(d_i_ag.get()); } } @@ -228,9 +228,7 @@ void InstantiationEngine::registerQuantifier(Node q) // take into account user patterns if (q.getNumChildren() == 3) { - Node subsPat = - d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants( - q[2], q); + Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q); // add patterns for (const Node& p : subsPat) { diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index 016784152..e27277933 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -20,8 +20,8 @@ #include <vector> #include "theory/quantifiers/ematching/inst_strategy.h" +#include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/quant_relevance.h" -#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 3bc5ded16..ac43d3bc9 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -36,9 +36,10 @@ namespace inst { /** trigger class constructor */ Trigger::Trigger(QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node q, std::vector<Node>& nodes) - : d_quantEngine(qe), d_qim(qim), d_quant(q) + : d_quantEngine(qe), d_qim(qim), d_qreg(qr), d_quant(q) { // We must ensure that the ground subterms of the trigger have been // preprocessed. @@ -233,6 +234,7 @@ bool Trigger::mkTriggerTerms(Node q, Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node f, std::vector<Node>& nodes, bool keepAll, @@ -273,11 +275,11 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, Trigger* t; if (!ho_apps.empty()) { - t = new HigherOrderTrigger(qe, qim, f, trNodes, ho_apps); + t = new HigherOrderTrigger(qe, qim, qr, f, trNodes, ho_apps); } else { - t = new Trigger(qe, qim, f, trNodes); + t = new Trigger(qe, qim, qr, f, trNodes); } qe->getTriggerDatabase()->addTrigger( trNodes, t ); @@ -286,6 +288,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node f, Node n, bool keepAll, @@ -294,7 +297,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, { std::vector< Node > nodes; nodes.push_back( n ); - return mkTrigger(qe, qim, f, nodes, keepAll, trOption, useNVars); + return mkTrigger(qe, qim, qr, f, nodes, keepAll, trOption, useNVars); } int Trigger::getActiveScore() { diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index e2ce61bd1..21888ff8f 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -31,6 +31,7 @@ class QuantifiersEngine; namespace quantifiers { class QuantifiersInferenceManager; +class QuantifiersRegistry; } namespace inst { @@ -163,6 +164,7 @@ class Trigger { }; static Trigger* mkTrigger(QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node q, std::vector<Node>& nodes, bool keepAll = true, @@ -171,6 +173,7 @@ class Trigger { /** single trigger version that calls the above function */ static Trigger* mkTrigger(QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node q, Node n, bool keepAll = true, @@ -194,6 +197,7 @@ class Trigger { /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */ Trigger(QuantifiersEngine* ie, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node q, std::vector<Node>& nodes); /** add an instantiation (called by InstMatchGenerator) @@ -243,6 +247,8 @@ class Trigger { QuantifiersEngine* d_quantEngine; /** Reference to the quantifiers inference manager */ quantifiers::QuantifiersInferenceManager& d_qim; + /** The quantifiers registry */ + quantifiers::QuantifiersRegistry& d_qreg; /** The quantified formula this trigger is for. */ Node d_quant; /** match generator |