diff options
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 |