From 8a3876f74f377817345af405aebfceebc7896059 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 25 Mar 2021 13:17:30 -0500 Subject: Refactor construction of triggers (#6209) This PR centralizes our utilities for generating triggers. It also splits the statistics class from quantifiers off from quantifiers engine. --- src/theory/quantifiers/ematching/ho_trigger.cpp | 3 +- src/theory/quantifiers/ematching/ho_trigger.h | 36 ++-- src/theory/quantifiers/ematching/im_generator.cpp | 5 - src/theory/quantifiers/ematching/im_generator.h | 2 - .../quantifiers/ematching/inst_match_generator.cpp | 5 +- .../ematching/inst_match_generator_simple.cpp | 9 +- src/theory/quantifiers/ematching/inst_strategy.cpp | 4 +- src/theory/quantifiers/ematching/inst_strategy.h | 13 +- .../ematching/inst_strategy_e_matching.cpp | 51 ++---- .../ematching/inst_strategy_e_matching.h | 2 +- .../ematching/inst_strategy_e_matching_user.cpp | 27 +-- .../ematching/inst_strategy_e_matching_user.h | 2 +- .../quantifiers/ematching/instantiation_engine.cpp | 10 +- .../quantifiers/ematching/instantiation_engine.h | 31 ++-- src/theory/quantifiers/ematching/trigger.cpp | 176 +------------------ src/theory/quantifiers/ematching/trigger.h | 68 +------- .../quantifiers/ematching/trigger_database.cpp | 188 +++++++++++++++++++++ .../quantifiers/ematching/trigger_database.h | 110 ++++++++++++ 18 files changed, 390 insertions(+), 352 deletions(-) create mode 100644 src/theory/quantifiers/ematching/trigger_database.cpp create mode 100644 src/theory/quantifiers/ematching/trigger_database.h (limited to 'src/theory/quantifiers/ematching') diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 4cdce940e..a2885cdec 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -34,7 +34,6 @@ namespace quantifiers { namespace inst { HigherOrderTrigger::HigherOrderTrigger( - QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, @@ -42,7 +41,7 @@ HigherOrderTrigger::HigherOrderTrigger( Node q, std::vector& nodes, std::map >& ho_apps) - : Trigger(qe, qs, qim, qr, tr, q, nodes), d_ho_var_apps(ho_apps) + : Trigger(qs, qim, qr, tr, q, nodes), d_ho_var_apps(ho_apps) { NodeManager* nm = NodeManager::currentNM(); // process the higher-order variable applications diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index 87c7adeec..d3489783c 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -90,11 +90,8 @@ class Trigger; */ class HigherOrderTrigger : public Trigger { - friend class Trigger; - - private: - HigherOrderTrigger(QuantifiersEngine* qe, - QuantifiersState& qs, + public: + HigherOrderTrigger(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, @@ -103,7 +100,6 @@ class HigherOrderTrigger : public Trigger std::map >& ho_apps); virtual ~HigherOrderTrigger(); - public: /** Collect higher order var apply terms * * Collect all top-level HO_APPLY terms in n whose head is a variable x in @@ -224,23 +220,23 @@ class HigherOrderTrigger : public Trigger /** higher-order pattern unification algorithm * - * Sends an instantiation that is equivalent to m via - * d_quantEngine->addInstantiation(...), - * based on Huet's algorithm. - * - * This is a helper function of sendInstantiation( m ) above. - * - * var_index is the index of the variable in m that we are currently processing - * i.e. we are processing the var_index^{th} higher-order variable. - * - * For example, say we are processing the match from (EX4) above. - * when var_index = 0,1, we are processing possibilities for - * instantiation of f1,f2 respectively. - */ + * Sends an instantiation that is equivalent to m via + * Instantiate::addInstantiation(...), + * based on Huet's algorithm. + * + * This is a helper function of sendInstantiation( m ) above. + * + * var_index is the index of the variable in m that we are currently + * processing i.e. we are processing the var_index^{th} higher-order variable. + * + * For example, say we are processing the match from (EX4) above. + * when var_index = 0,1, we are processing possibilities for + * instantiation of f1,f2 respectively. + */ bool sendInstantiation(std::vector& m, size_t var_index); /** higher-order pattern unification algorithm * Sends an instantiation that is equivalent to m via - * d_quantEngine->addInstantiation(...). + * Instantiate::addInstantiation(...). * This is a helper function of sendInstantiation( m, var_index ) above. * * var_index is the index of the variable in m that we are currently diff --git a/src/theory/quantifiers/ematching/im_generator.cpp b/src/theory/quantifiers/ematching/im_generator.cpp index 48c07ba4d..06d17dea4 100644 --- a/src/theory/quantifiers/ematching/im_generator.cpp +++ b/src/theory/quantifiers/ematching/im_generator.cpp @@ -33,11 +33,6 @@ bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id) return d_tparent->sendInstantiation(m, id); } -QuantifiersEngine* IMGenerator::getQuantifiersEngine() -{ - return d_tparent->d_quantEngine; -} - } // namespace inst } // namespace quantifiers } // namespace theory diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h index efc65cdef..6968a0dee 100644 --- a/src/theory/quantifiers/ematching/im_generator.h +++ b/src/theory/quantifiers/ematching/im_generator.h @@ -114,8 +114,6 @@ protected: QuantifiersState& d_qstate; /** Reference to the term registry */ TermRegistry& d_treg; - // !!!!!!!!! temporarily available (project #15) - QuantifiersEngine* getQuantifiersEngine(); };/* class IMGenerator */ } // namespace inst diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index ac3e1b9be..3dee6de73 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -26,6 +26,7 @@ #include "theory/quantifiers/instantiate.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" @@ -74,7 +75,7 @@ int InstMatchGenerator::getActiveScore() if( d_match_pattern.isNull() ){ return -1; } - quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); + quantifiers::TermDb* tdb = d_treg.getTermDatabase(); if (TriggerTermInfo::isAtomicTrigger(d_match_pattern)) { Node f = tdb->getMatchOperator(d_match_pattern); @@ -157,7 +158,7 @@ void InstMatchGenerator::initialize(Node q, d_match_pattern_type = d_match_pattern.getType(); Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; - quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); + quantifiers::TermDb* tdb = d_treg.getTermDatabase(); d_match_pattern_op = tdb->getMatchOperator(d_match_pattern); // now, collect children of d_match_pattern diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index c7360d02f..ab30b4b2d 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -15,12 +15,11 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/trigger_term_info.h" -#include "theory/quantifiers/ematching/trigger_trie.h" #include "theory/quantifiers/instantiate.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" using namespace CVC4::kind; @@ -66,7 +65,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent, } d_match_pattern_arg_types.push_back(d_match_pattern[i].getType()); } - TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); + TermDb* tdb = d_treg.getTermDatabase(); d_op = tdb->getMatchOperator(d_match_pattern); } @@ -75,7 +74,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q) { uint64_t addedLemmas = 0; TNodeTrie* tat; - TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); + TermDb* tdb = d_treg.getTermDatabase(); if (d_eqc.isNull()) { tat = tdb->getTermArgTrie(d_op); @@ -188,7 +187,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, int InstMatchGeneratorSimple::getActiveScore() { - TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); + TermDb* tdb = d_treg.getTermDatabase(); Node f = tdb->getMatchOperator(d_match_pattern); size_t ngt = tdb->getNumGroundTerms(f); Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) " diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp index 083331948..5e9899ec3 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy.cpp @@ -20,12 +20,12 @@ namespace CVC4 { namespace theory { namespace quantifiers { -InstStrategy::InstStrategy(QuantifiersEngine* qe, +InstStrategy::InstStrategy(inst::TriggerDatabase& td, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr) + : d_td(td), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr) { } InstStrategy::~InstStrategy() {} diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index cbe6e341b..9d304368c 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -24,11 +24,12 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { +namespace inst { +class TriggerDatabase; +} + class QuantifiersState; class QuantifiersInferenceManager; class QuantifiersRegistry; @@ -49,7 +50,7 @@ enum class InstStrategyStatus class InstStrategy { public: - InstStrategy(QuantifiersEngine* qe, + InstStrategy(inst::TriggerDatabase& td, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, @@ -70,8 +71,8 @@ class InstStrategy * maintained by the quantifiers state. */ options::UserPatMode getInstUserPatMode() const; - /** reference to the instantiation engine */ - QuantifiersEngine* d_quantEngine; + /** reference to the trigger database */ + inst::TriggerDatabase& d_td; /** The quantifiers state object */ QuantifiersState& d_qstate; /** The quantifiers inference manager object */ diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index ba068230d..d489869ae 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -15,11 +15,11 @@ #include "theory/quantifiers/ematching/inst_strategy_e_matching.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" +#include "theory/quantifiers/ematching/trigger_database.h" #include "theory/quantifiers/quant_relevance.h" #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" -#include "theory/quantifiers_engine.h" #include "util/random.h" using namespace CVC4::kind; @@ -62,13 +62,13 @@ struct sortTriggers { }; InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( - QuantifiersEngine* qe, + inst::TriggerDatabase& td, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, QuantRelevance* qrlv) - : InstStrategy(qe, qs, qim, qr, tr), d_quant_rel(qrlv) + : InstStrategy(td, qs, qim, qr, tr), d_quant_rel(qrlv) { //how to select trigger terms d_tr_strategy = options::triggerSelMode(); @@ -281,16 +281,11 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ Trigger* tr = NULL; if (d_is_single_trigger[patTerms[0]]) { - tr = Trigger::mkTrigger(d_quantEngine, - d_qstate, - d_qim, - d_qreg, - d_treg, - f, - patTerms[0], - false, - Trigger::TR_RETURN_NULL, - d_num_trigger_vars[f]); + tr = d_td.mkTrigger(f, + patTerms[0], + false, + TriggerDatabase::TR_RETURN_NULL, + d_num_trigger_vars[f]); d_single_trigger_gen[patTerms[0]] = true; } else @@ -321,16 +316,11 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_made_multi_trigger[f] = true; } // will possibly want to get an old trigger - tr = Trigger::mkTrigger(d_quantEngine, - d_qstate, - d_qim, - d_qreg, - d_treg, - f, - patTerms, - false, - Trigger::TR_GET_OLD, - d_num_trigger_vars[f]); + tr = d_td.mkTrigger(f, + patTerms, + false, + TriggerDatabase::TR_GET_OLD, + d_num_trigger_vars[f]); } if (tr == nullptr) { @@ -366,16 +356,11 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ <= nqfs_curr) { d_single_trigger_gen[patTerms[index]] = true; - Trigger* tr2 = Trigger::mkTrigger(d_quantEngine, - d_qstate, - d_qim, - d_qreg, - d_treg, - f, - patTerms[index], - false, - Trigger::TR_RETURN_NULL, - d_num_trigger_vars[f]); + Trigger* tr2 = d_td.mkTrigger(f, + patTerms[index], + false, + TriggerDatabase::TR_RETURN_NULL, + d_num_trigger_vars[f]); addTrigger(tr2, f); success = true; } diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index f4c74c43a..a17e7bbb5 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -85,7 +85,7 @@ class InstStrategyAutoGenTriggers : public InstStrategy std::map d_hasUserPatterns; public: - InstStrategyAutoGenTriggers(QuantifiersEngine* qe, + InstStrategyAutoGenTriggers(inst::TriggerDatabase& td, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, 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 412676ad4..a15baa5e4 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -15,8 +15,8 @@ #include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" +#include "theory/quantifiers/ematching/trigger_database.h" #include "theory/quantifiers/quantifiers_state.h" -#include "theory/quantifiers_engine.h" using namespace CVC4::kind; using namespace CVC4::theory::quantifiers::inst; @@ -26,12 +26,12 @@ namespace theory { namespace quantifiers { InstStrategyUserPatterns::InstStrategyUserPatterns( - QuantifiersEngine* ie, + inst::TriggerDatabase& td, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : InstStrategy(ie, qs, qim, qr, tr) + : InstStrategy(td, qs, qim, qr, tr) { } InstStrategyUserPatterns::~InstStrategyUserPatterns() {} @@ -107,15 +107,8 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q, std::vector >& ugw = d_user_gen_wait[q]; for (size_t i = 0, usize = ugw.size(); i < usize; i++) { - Trigger* t = Trigger::mkTrigger(d_quantEngine, - d_qstate, - d_qim, - d_qreg, - d_treg, - q, - ugw[i], - true, - Trigger::TR_RETURN_NULL); + Trigger* t = + d_td.mkTrigger(q, ugw[i], true, TriggerDatabase::TR_RETURN_NULL); if (t) { d_user_gen[q].push_back(t); @@ -168,15 +161,7 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) d_user_gen_wait[q].push_back(nodes); return; } - Trigger* t = Trigger::mkTrigger(d_quantEngine, - d_qstate, - d_qim, - d_qreg, - d_treg, - q, - nodes, - true, - Trigger::TR_MAKE_NEW); + Trigger* t = d_td.mkTrigger(q, nodes, true, TriggerDatabase::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 e63154a60..821d7de77 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -34,7 +34,7 @@ namespace quantifiers { class InstStrategyUserPatterns : public InstStrategy { public: - InstStrategyUserPatterns(QuantifiersEngine* qe, + InstStrategyUserPatterns(inst::TriggerDatabase& td, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 1c301141c..9153d9280 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -42,6 +42,7 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe, d_isup(), d_i_ag(), d_quants(), + d_trdb(qs, qim, qr, tr), d_quant_rel(nullptr) { if (options::relevantTriggers()) @@ -53,14 +54,13 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe, // user-provided patterns if (options::userPatternsQuant() != options::UserPatMode::IGNORE) { - d_isup.reset( - new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr, tr)); + d_isup.reset(new InstStrategyUserPatterns(d_trdb, qs, qim, qr, tr)); d_instStrategies.push_back(d_isup.get()); } // auto-generated patterns d_i_ag.reset(new InstStrategyAutoGenTriggers( - d_quantEngine, qs, qim, qr, tr, d_quant_rel.get())); + d_trdb, qs, qim, qr, tr, d_quant_rel.get())); d_instStrategies.push_back(d_i_ag.get()); } } @@ -135,7 +135,7 @@ void InstantiationEngine::reset_round( Theory::Effort e ){ void InstantiationEngine::check(Theory::Effort e, QEffort quant_e) { - CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time); + CodeTimer codeTimer(d_qstate.getStats().d_ematching_time); if (quant_e != QEFFORT_STANDARD) { return; @@ -154,7 +154,7 @@ void InstantiationEngine::check(Theory::Effort e, QEffort quant_e) size_t nquant = m->getNumAssertedQuantifiers(); for (size_t i = 0; i < nquant; i++) { - Node q = d_quantEngine->getModel()->getAssertedQuantifier(i, true); + Node q = m->getAssertedQuantifier(i, true); if (shouldProcess(q) && m->isQuantifierActive(q)) { quantActive = true; diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index 4042e3424..26df4f548 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -20,6 +20,7 @@ #include #include "theory/quantifiers/ematching/inst_strategy.h" +#include "theory/quantifiers/ematching/trigger_database.h" #include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/quant_relevance.h" @@ -31,22 +32,6 @@ class InstStrategyUserPatterns; class InstStrategyAutoGenTriggers; class InstantiationEngine : public QuantifiersModule { - private: - /** instantiation strategies */ - std::vector d_instStrategies; - /** user-pattern instantiation strategy */ - std::unique_ptr d_isup; - /** auto gen triggers; only kept for destructor cleanup */ - std::unique_ptr d_i_ag; - - /** current processing quantified formulas */ - std::vector d_quants; - - /** is the engine incomplete for this quantifier */ - bool isIncomplete(Node q); - /** do instantiation round */ - void doInstantiationRound(Theory::Effort effort); - public: InstantiationEngine(QuantifiersEngine* qe, QuantifiersState& qs, @@ -69,8 +54,22 @@ class InstantiationEngine : public QuantifiersModule { std::string identify() const override { return "InstEngine"; } private: + /** is the engine incomplete for this quantifier */ + bool isIncomplete(Node q); + /** do instantiation round */ + void doInstantiationRound(Theory::Effort effort); /** Return true if this module should process quantified formula q */ bool shouldProcess(Node q); + /** instantiation strategies */ + std::vector d_instStrategies; + /** user-pattern instantiation strategy */ + std::unique_ptr d_isup; + /** auto gen triggers; only kept for destructor cleanup */ + std::unique_ptr d_i_ag; + /** current processing quantified formulas */ + std::vector d_quants; + /** all triggers will be stored in this database */ + inst::TriggerDatabase d_trdb; /** for computing relevance of quantifiers */ std::unique_ptr d_quant_rel; }; /* class InstantiationEngine */ diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index c93e1a99b..c739623bc 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -17,7 +17,6 @@ #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/candidate_generator.h" -#include "theory/quantifiers/ematching/ho_trigger.h" #include "theory/quantifiers/ematching/inst_match_generator.h" #include "theory/quantifiers/ematching/inst_match_generator_multi.h" #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" @@ -31,7 +30,6 @@ #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/valuation.h" using namespace CVC4::kind; @@ -42,19 +40,13 @@ namespace quantifiers { namespace inst { /** trigger class constructor */ -Trigger::Trigger(QuantifiersEngine* qe, - QuantifiersState& qs, +Trigger::Trigger(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, Node q, std::vector& nodes) - : d_quantEngine(qe), - d_qstate(qs), - d_qim(qim), - d_qreg(qr), - d_treg(tr), - d_quant(q) + : d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), d_quant(q) { // We must ensure that the ground subterms of the trigger have been // preprocessed. @@ -74,14 +66,15 @@ Trigger::Trigger(QuantifiersEngine* qe, Trace("trigger") << " " << n << std::endl; } } + QuantifiersStatistics& stats = qs.getStats(); if( d_nodes.size()==1 ){ if (TriggerTermInfo::isSimpleTrigger(d_nodes[0])) { d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]); - ++(qe->d_statistics.d_triggers); + ++(stats.d_triggers); }else{ d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]); - ++(qe->d_statistics.d_simple_triggers); + ++(stats.d_simple_triggers); } }else{ if( options::multiTriggerCache() ){ @@ -97,7 +90,7 @@ Trigger::Trigger(QuantifiersEngine* qe, Trace("multi-trigger") << " " << nc << std::endl; } } - ++(qe->d_statistics.d_multi_triggers); + ++(stats.d_multi_triggers); } Trace("trigger-debug") << "Finished making trigger." << std::endl; @@ -162,163 +155,6 @@ bool Trigger::sendInstantiation(InstMatch& m, InferenceId id) return sendInstantiation(m.d_vals, id); } -bool Trigger::mkTriggerTerms(Node q, - std::vector& nodes, - size_t nvars, - std::vector& trNodes) -{ - //only take nodes that contribute variables to the trigger when added - std::vector< Node > temp; - temp.insert( temp.begin(), nodes.begin(), nodes.end() ); - std::map< Node, bool > vars; - std::map< Node, std::vector< Node > > patterns; - size_t varCount = 0; - std::map< Node, std::vector< Node > > varContains; - for (const Node& pat : temp) - { - TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]); - } - for (const Node& t : temp) - { - const std::vector& vct = varContains[t]; - bool foundVar = false; - for (const Node& v : vct) - { - Assert(TermUtil::getInstConstAttr(v) == q); - if( vars.find( v )==vars.end() ){ - varCount++; - vars[ v ] = true; - foundVar = true; - } - } - if( foundVar ){ - trNodes.push_back(t); - for (const Node& v : vct) - { - patterns[v].push_back(t); - } - } - if (varCount == nvars) - { - break; - } - } - if (varCount < nvars) - { - Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl; - Trace("trigger-debug") << nodes << std::endl; - //do not generate multi-trigger if it does not contain all variables - return false; - } - // now, minimize the trigger - for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++) - { - bool keepPattern = false; - Node n = trNodes[i]; - const std::vector& vcn = varContains[n]; - for (const Node& v : vcn) - { - if (patterns[v].size() == 1) - { - keepPattern = true; - break; - } - } - if (!keepPattern) - { - // remove from pattern vector - for (const Node& v : vcn) - { - std::vector& pv = patterns[v]; - for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++) - { - if (pv[k] == n) - { - pv.erase(pv.begin() + k, pv.begin() + k + 1); - break; - } - } - } - // remove from trigger nodes - trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1); - i--; - } - } - return true; -} - -Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, - QuantifiersState& qs, - QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr, - TermRegistry& tr, - Node f, - std::vector& nodes, - bool keepAll, - int trOption, - size_t useNVars) -{ - std::vector< Node > trNodes; - if( !keepAll ){ - size_t nvars = useNVars == 0 ? f[0].getNumChildren() : useNVars; - if (!mkTriggerTerms(f, nodes, nvars, trNodes)) - { - return nullptr; - } - }else{ - trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() ); - } - - //check for duplicate? - if( trOption!=TR_MAKE_NEW ){ - Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes ); - if( t ){ - if( trOption==TR_GET_OLD ){ - //just return old trigger - return t; - }else{ - return nullptr; - } - } - } - - // check if higher-order - Trace("trigger-debug") << "Collect higher-order variable triggers..." - << std::endl; - std::map > ho_apps; - HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps); - Trace("trigger-debug") << "...got " << ho_apps.size() - << " higher-order applications." << std::endl; - Trigger* t; - if (!ho_apps.empty()) - { - t = new HigherOrderTrigger(qe, qs, qim, qr, tr, f, trNodes, ho_apps); - } - else - { - t = new Trigger(qe, qs, qim, qr, tr, f, trNodes); - } - - qe->getTriggerDatabase()->addTrigger( trNodes, t ); - return t; -} - -Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, - QuantifiersState& qs, - QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr, - TermRegistry& tr, - Node f, - Node n, - bool keepAll, - int trOption, - size_t useNVars) -{ - std::vector< Node > nodes; - nodes.push_back( n ); - return mkTrigger(qe, qs, qim, qr, tr, f, nodes, keepAll, trOption, useNVars); -} - int Trigger::getActiveScore() { return d_mg->getActiveScore(); } Node Trigger::ensureGroundTermPreprocessed(Valuation& val, diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 3c218ca7b..5dd8db452 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -102,6 +102,13 @@ class Trigger { friend class IMGenerator; public: + /** trigger constructor */ + Trigger(QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr, + Node q, + std::vector& nodes); virtual ~Trigger(); /** get the generator associated with this trigger */ IMGenerator* getGenerator() { return d_mg; } @@ -144,67 +151,8 @@ class Trigger { int getActiveScore(); /** print debug information for the trigger */ void debugPrint(const char* c) const; - /** mkTrigger method - * - * This makes an instance of a trigger object. - * qe : pointer to the quantifier engine; - * q : the quantified formula we are making a trigger for - * nodes : the nodes comprising the (multi-)trigger - * keepAll: don't remove unneeded patterns; - * trOption : policy for dealing with triggers that already exist - * (see below) - * useNVars : number of variables that should be bound by the trigger - * typically, the number of quantified variables in q. - */ - enum{ - TR_MAKE_NEW, //make new trigger even if it already may exist - TR_GET_OLD, //return a previous trigger if it had already been created - TR_RETURN_NULL //return null if a duplicate is found - }; - static Trigger* mkTrigger(QuantifiersEngine* qe, - QuantifiersState& qs, - QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr, - TermRegistry& tr, - Node q, - std::vector& nodes, - bool keepAll = true, - int trOption = TR_MAKE_NEW, - size_t useNVars = 0); - /** single trigger version that calls the above function */ - static Trigger* mkTrigger(QuantifiersEngine* qe, - QuantifiersState& qs, - QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr, - TermRegistry& tr, - Node q, - Node n, - bool keepAll = true, - int trOption = TR_MAKE_NEW, - size_t useNVars = 0); - /** make trigger terms - * - * This takes a set of eligible trigger terms and stores a subset of them in - * trNodes, such that : - * (1) the terms in trNodes contain at least n_vars of the quantified - * variables in quantified formula q, and - * (2) the set trNodes is minimal, i.e. removing one term from trNodes - * always violates (1). - */ - static bool mkTriggerTerms(Node q, - std::vector& nodes, - size_t nvars, - std::vector& trNodes); protected: - /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */ - Trigger(QuantifiersEngine* ie, - QuantifiersState& qs, - QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr, - TermRegistry& tr, - Node q, - std::vector& nodes); /** add an instantiation (called by InstMatchGenerator) * * This calls Instantiate::addInstantiation(...) for instantiations @@ -250,8 +198,6 @@ class Trigger { * This example would fail to match when f(a) is not registered. */ std::vector d_groundTerms; - // !!!!!!!!!!!!!!!!!! temporarily available (project #15) - QuantifiersEngine* d_quantEngine; /** Reference to the quantifiers state */ QuantifiersState& d_qstate; /** Reference to the quantifiers inference manager */ diff --git a/src/theory/quantifiers/ematching/trigger_database.cpp b/src/theory/quantifiers/ematching/trigger_database.cpp new file mode 100644 index 000000000..fae7a10a0 --- /dev/null +++ b/src/theory/quantifiers/ematching/trigger_database.cpp @@ -0,0 +1,188 @@ +/********************* */ +/*! \file trigger_database.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief trigger database class + **/ + +#include "theory/quantifiers/ematching/trigger_database.h" + +#include "theory/quantifiers/ematching/ho_trigger.h" +#include "theory/quantifiers/ematching/trigger.h" +#include "theory/quantifiers/term_util.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { +namespace inst { + +TriggerDatabase::TriggerDatabase(QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr) + : d_qs(qs), d_qim(qim), d_qreg(qr), d_treg(tr) +{ +} +TriggerDatabase::~TriggerDatabase() {} + +Trigger* TriggerDatabase::mkTrigger(Node q, + const std::vector& nodes, + bool keepAll, + int trOption, + size_t useNVars) +{ + std::vector trNodes; + if (!keepAll) + { + size_t nvars = useNVars == 0 ? q[0].getNumChildren() : useNVars; + if (!mkTriggerTerms(q, nodes, nvars, trNodes)) + { + return nullptr; + } + } + else + { + trNodes.insert(trNodes.begin(), nodes.begin(), nodes.end()); + } + + // check for duplicate? + if (trOption != TR_MAKE_NEW) + { + Trigger* t = d_trie.getTrigger(trNodes); + if (t) + { + if (trOption == TR_GET_OLD) + { + // just return old trigger + return t; + } + return nullptr; + } + } + + // check if higher-order + Trace("trigger-debug") << "Collect higher-order variable triggers..." + << std::endl; + std::map > hoApps; + HigherOrderTrigger::collectHoVarApplyTerms(q, trNodes, hoApps); + Trace("trigger-debug") << "...got " << hoApps.size() + << " higher-order applications." << std::endl; + Trigger* t; + if (!hoApps.empty()) + { + t = new HigherOrderTrigger(d_qs, d_qim, d_qreg, d_treg, q, trNodes, hoApps); + } + else + { + t = new Trigger(d_qs, d_qim, d_qreg, d_treg, q, trNodes); + } + d_trie.addTrigger(trNodes, t); + return t; +} + +Trigger* TriggerDatabase::mkTrigger( + Node q, Node n, bool keepAll, int trOption, size_t useNVars) +{ + std::vector nodes; + nodes.push_back(n); + return mkTrigger(q, nodes, keepAll, trOption, useNVars); +} + +bool TriggerDatabase::mkTriggerTerms(Node q, + const std::vector& nodes, + size_t nvars, + std::vector& trNodes) +{ + // only take nodes that contribute variables to the trigger when added + std::map vars; + std::map > patterns; + size_t varCount = 0; + std::map > varContains; + for (const Node& pat : nodes) + { + TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]); + } + for (const Node& t : nodes) + { + const std::vector& vct = varContains[t]; + bool foundVar = false; + for (const Node& v : vct) + { + Assert(TermUtil::getInstConstAttr(v) == q); + if (vars.find(v) == vars.end()) + { + varCount++; + vars[v] = true; + foundVar = true; + } + } + if (foundVar) + { + trNodes.push_back(t); + for (const Node& v : vct) + { + patterns[v].push_back(t); + } + } + if (varCount == nvars) + { + break; + } + } + if (varCount < nvars) + { + Trace("trigger-debug") << "Don't consider trigger since it does not " + "contain specified number of variables." + << std::endl; + Trace("trigger-debug") << nodes << std::endl; + // do not generate multi-trigger if it does not contain all variables + return false; + } + // now, minimize the trigger + for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++) + { + bool keepPattern = false; + Node n = trNodes[i]; + const std::vector& vcn = varContains[n]; + for (const Node& v : vcn) + { + if (patterns[v].size() == 1) + { + keepPattern = true; + break; + } + } + if (!keepPattern) + { + // remove from pattern vector + for (const Node& v : vcn) + { + std::vector& pv = patterns[v]; + for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++) + { + if (pv[k] == n) + { + pv.erase(pv.begin() + k, pv.begin() + k + 1); + break; + } + } + } + // remove from trigger nodes + trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1); + i--; + } + } + return true; +} + +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/trigger_database.h b/src/theory/quantifiers/ematching/trigger_database.h new file mode 100644 index 000000000..21df0e536 --- /dev/null +++ b/src/theory/quantifiers/ematching/trigger_database.h @@ -0,0 +1,110 @@ +/********************* */ +/*! \file trigger_database.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief trigger trie class + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H +#define CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H + +#include + +#include "expr/node.h" +#include "theory/quantifiers/ematching/trigger_trie.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class QuantifiersInferenceManager; +class QuantifiersState; +class QuantifiersRegistry; +class TermRegistry; + +namespace inst { + +/** + * A database of triggers, which manages how triggers are constructed. + */ +class TriggerDatabase +{ + public: + TriggerDatabase(QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr); + ~TriggerDatabase(); + + /** mkTrigger method + * + * This makes an instance of a trigger object. + * qe : pointer to the quantifier engine; + * q : the quantified formula we are making a trigger for + * nodes : the nodes comprising the (multi-)trigger + * keepAll: don't remove unneeded patterns; + * trOption : policy for dealing with triggers that already exist + * (see below) + * useNVars : number of variables that should be bound by the trigger + * typically, the number of quantified variables in q. + */ + enum + { + TR_MAKE_NEW, // make new trigger even if it already may exist + TR_GET_OLD, // return a previous trigger if it had already been created + TR_RETURN_NULL // return null if a duplicate is found + }; + Trigger* mkTrigger(Node q, + const std::vector& nodes, + bool keepAll = true, + int trOption = TR_MAKE_NEW, + size_t useNVars = 0); + /** single trigger version that calls the above function */ + Trigger* mkTrigger(Node q, + Node n, + bool keepAll = true, + int trOption = TR_MAKE_NEW, + size_t useNVars = 0); + + /** make trigger terms + * + * This takes a set of eligible trigger terms and stores a subset of them in + * trNodes, such that : + * (1) the terms in trNodes contain at least n_vars of the quantified + * variables in quantified formula q, and + * (2) the set trNodes is minimal, i.e. removing one term from trNodes + * always violates (1). + */ + static bool mkTriggerTerms(Node q, + const std::vector& nodes, + size_t nvars, + std::vector& trNodes); + + private: + /** The trigger trie, containing the triggers */ + TriggerTrie d_trie; + /** Reference to the quantifiers state */ + QuantifiersState& d_qs; + /** Reference to the quantifiers inference manager */ + QuantifiersInferenceManager& d_qim; + /** The quantifiers registry */ + QuantifiersRegistry& d_qreg; + /** Reference to the term registry */ + TermRegistry& d_treg; +}; + +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H */ -- cgit v1.2.3