diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-25 13:17:30 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-25 18:17:30 +0000 |
commit | 8a3876f74f377817345af405aebfceebc7896059 (patch) | |
tree | 82474f0df4b65274e6fbbb8a2d3f56ec42815a40 /src | |
parent | f9e3d2dccd5018e07df1c2cd323c5e192b020819 (diff) |
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.
Diffstat (limited to 'src')
27 files changed, 528 insertions, 443 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 44ba4e261..febb34281 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -693,6 +693,8 @@ libcvc4_add_sources( theory/quantifiers/ematching/pattern_term_selector.h theory/quantifiers/ematching/trigger.cpp theory/quantifiers/ematching/trigger.h + theory/quantifiers/ematching/trigger_database.cpp + theory/quantifiers/ematching/trigger_database.h theory/quantifiers/ematching/trigger_term_info.cpp theory/quantifiers/ematching/trigger_term_info.h theory/quantifiers/ematching/trigger_trie.cpp @@ -763,6 +765,8 @@ libcvc4_add_sources( theory/quantifiers/quantifiers_rewriter.h theory/quantifiers/quantifiers_state.cpp theory/quantifiers/quantifiers_state.h + theory/quantifiers/quantifiers_statistics.cpp + theory/quantifiers/quantifiers_statistics.h theory/quantifiers/query_generator.cpp theory/quantifiers/query_generator.h theory/quantifiers/relevant_domain.cpp 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<Node>& nodes, std::map<Node, std::vector<Node> >& 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<Node, std::vector<Node> >& 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<Node>& 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<Node, bool> 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<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_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 <vector> #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<InstStrategy*> d_instStrategies; - /** user-pattern instantiation strategy */ - std::unique_ptr<InstStrategyUserPatterns> d_isup; - /** auto gen triggers; only kept for destructor cleanup */ - std::unique_ptr<InstStrategyAutoGenTriggers> d_i_ag; - - /** current processing quantified formulas */ - std::vector<Node> 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<InstStrategy*> d_instStrategies; + /** user-pattern instantiation strategy */ + std::unique_ptr<InstStrategyUserPatterns> d_isup; + /** auto gen triggers; only kept for destructor cleanup */ + std::unique_ptr<InstStrategyAutoGenTriggers> d_i_ag; + /** current processing quantified formulas */ + std::vector<Node> d_quants; + /** all triggers will be stored in this database */ + inst::TriggerDatabase d_trdb; /** for computing relevance of quantifiers */ std::unique_ptr<QuantRelevance> 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<Node>& 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<Node>& nodes, - size_t nvars, - std::vector<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node, std::vector<Node> > 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<Node>& 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<Node>& 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<Node>& nodes, - size_t nvars, - std::vector<Node>& trNodes); protected: - /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */ - Trigger(QuantifiersEngine* ie, - QuantifiersState& qs, - QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr, - TermRegistry& tr, - Node q, - std::vector<Node>& 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<Node> 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<Node>& nodes, + bool keepAll, + int trOption, + size_t useNVars) +{ + std::vector<Node> 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<Node, std::vector<Node> > 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<Node> nodes; + nodes.push_back(n); + return mkTrigger(q, nodes, keepAll, trOption, useNVars); +} + +bool TriggerDatabase::mkTriggerTerms(Node q, + const std::vector<Node>& nodes, + size_t nvars, + std::vector<Node>& trNodes) +{ + // only take nodes that contribute variables to the trigger when added + 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 : nodes) + { + TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]); + } + for (const Node& t : nodes) + { + const std::vector<Node>& 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<Node>& 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<Node>& 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 <vector> + +#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<Node>& 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<Node>& nodes, + size_t nvars, + std::vector<Node>& 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 */ diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index c58bcc863..f2a41975f 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -22,16 +22,13 @@ #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -namespace CVC4 { - -using namespace kind; -using namespace context; +using namespace CVC4::kind; +using namespace CVC4::context; +namespace CVC4 { namespace theory { namespace quantifiers { -using namespace inst; - InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 62f15a6a6..52096a8ec 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1988,7 +1988,7 @@ inline QuantConflictFind::Effort QcfEffortEnd() { /** check */ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) { - CodeTimer codeTimer(d_quantEngine->d_statistics.d_qcf_time); + CodeTimer codeTimer(d_qstate.getStats().d_qcf_time); if (quant_e != QEFFORT_CONFLICT) { return; diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp index 5916c446c..be691ae27 100644 --- a/src/theory/quantifiers/quantifiers_state.cpp +++ b/src/theory/quantifiers/quantifiers_state.cpp @@ -156,6 +156,8 @@ void QuantifiersState::debugPrintEqualityEngine(const char* c) const const LogicInfo& QuantifiersState::getLogicInfo() const { return d_logicInfo; } +QuantifiersStatistics& QuantifiersState::getStats() { return d_statistics; } + } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h index 40101f3e3..6b4daec61 100644 --- a/src/theory/quantifiers/quantifiers_state.h +++ b/src/theory/quantifiers/quantifiers_state.h @@ -17,6 +17,7 @@ #ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H +#include "theory/quantifiers/quantifiers_statistics.h" #include "theory/theory.h" #include "theory/theory_state.h" @@ -56,6 +57,8 @@ class QuantifiersState : public TheoryState void debugPrintEqualityEngine(const char* c) const; /** get the logic info */ const LogicInfo& getLogicInfo() const; + /** get the stats */ + QuantifiersStatistics& getStats(); private: /** The number of instantiation rounds in this SAT context */ @@ -77,6 +80,8 @@ class QuantifiersState : public TheoryState uint64_t d_instWhenPhase; /** Information about the logic we're operating within. */ const LogicInfo& d_logicInfo; + /** The statistics */ + QuantifiersStatistics d_statistics; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/quantifiers_statistics.cpp b/src/theory/quantifiers/quantifiers_statistics.cpp new file mode 100644 index 000000000..4567a6d4f --- /dev/null +++ b/src/theory/quantifiers/quantifiers_statistics.cpp @@ -0,0 +1,64 @@ +/********************* */ +/*! \file quantifiers_statistics.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Implementation of quantifiers statistics class + **/ + +#include "theory/quantifiers/quantifiers_statistics.h" + +#include "smt/smt_statistics_registry.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +QuantifiersStatistics::QuantifiersStatistics() + : d_time("theory::QuantifiersEngine::time"), + d_qcf_time("theory::QuantifiersEngine::time_qcf"), + d_ematching_time("theory::QuantifiersEngine::time_ematching"), + d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), + d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), + d_instantiation_rounds_lc( + "QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), + d_triggers("QuantifiersEngine::Triggers", 0), + d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), + d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), + d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0) +{ + smtStatisticsRegistry()->registerStat(&d_time); + smtStatisticsRegistry()->registerStat(&d_qcf_time); + smtStatisticsRegistry()->registerStat(&d_ematching_time); + smtStatisticsRegistry()->registerStat(&d_num_quant); + smtStatisticsRegistry()->registerStat(&d_instantiation_rounds); + smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc); + smtStatisticsRegistry()->registerStat(&d_triggers); + smtStatisticsRegistry()->registerStat(&d_simple_triggers); + smtStatisticsRegistry()->registerStat(&d_multi_triggers); + smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv); +} + +QuantifiersStatistics::~QuantifiersStatistics() +{ + smtStatisticsRegistry()->unregisterStat(&d_time); + smtStatisticsRegistry()->unregisterStat(&d_qcf_time); + smtStatisticsRegistry()->unregisterStat(&d_ematching_time); + smtStatisticsRegistry()->unregisterStat(&d_num_quant); + smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds); + smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc); + smtStatisticsRegistry()->unregisterStat(&d_triggers); + smtStatisticsRegistry()->unregisterStat(&d_simple_triggers); + smtStatisticsRegistry()->unregisterStat(&d_multi_triggers); + smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h new file mode 100644 index 000000000..1fa053484 --- /dev/null +++ b/src/theory/quantifiers/quantifiers_statistics.h @@ -0,0 +1,52 @@ +/********************* */ +/*! \file quantifiers_statistics.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Quantifiers statistics class + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H +#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H + +#include "util/statistics_registry.h" +#include "util/stats_timer.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** + * Statistics class for quantifiers, which contains all statistics that need + * to be tracked globally within the quantifiers theory. + */ +class QuantifiersStatistics +{ + public: + QuantifiersStatistics(); + ~QuantifiersStatistics(); + TimerStat d_time; + TimerStat d_qcf_time; + TimerStat d_ematching_time; + IntStat d_num_quant; + IntStat d_instantiation_rounds; + IntStat d_instantiation_rounds_lc; + IntStat d_triggers; + IntStat d_simple_triggers; + IntStat d_multi_triggers; + IntStat d_red_alpha_equiv; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0155eb05a..17a76468c 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -19,8 +19,6 @@ #include "options/smt_options.h" #include "options/uf_options.h" #include "smt/smt_engine_scope.h" -#include "smt/smt_statistics_registry.h" -#include "theory/quantifiers/ematching/trigger_trie.h" #include "theory/quantifiers/equality_query.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/first_order_model_fmc.h" @@ -32,13 +30,11 @@ #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/quantifiers_statistics.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/skolemize.h" -#include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_registry.h" -#include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" -#include "theory/uf/equality_engine.h" using namespace std; using namespace CVC4::kind; @@ -59,7 +55,6 @@ QuantifiersEngine::QuantifiersEngine( d_pnm(pnm), d_qreg(qr), d_treg(tr), - d_tr_trie(new quantifiers::inst::TriggerTrie), d_model(d_treg.getModel()), d_quants_prereg(qstate.getUserContext()), d_quants_red(qstate.getUserContext()) @@ -137,11 +132,6 @@ quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const { return d_treg.getTermDatabase(); } - -quantifiers::inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const -{ - return d_tr_trie.get(); -} /// !!!!!!!!!!!!!! void QuantifiersEngine::presolve() { @@ -186,7 +176,8 @@ void QuantifiersEngine::ppNotifyAssertions( } void QuantifiersEngine::check( Theory::Effort e ){ - CodeTimer codeTimer(d_statistics.d_time); + quantifiers::QuantifiersStatistics& stats = d_qstate.getStats(); + CodeTimer codeTimer(stats.d_time); Assert(d_qstate.getEqualityEngine() != nullptr); if (!d_qstate.getEqualityEngine()->consistent()) { @@ -332,9 +323,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ } if( e==Theory::EFFORT_LAST_CALL ){ - ++(d_statistics.d_instantiation_rounds_lc); + ++(stats.d_instantiation_rounds_lc); }else if( e==Theory::EFFORT_FULL ){ - ++(d_statistics.d_instantiation_rounds); + ++(stats.d_instantiation_rounds); } Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl; for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT; @@ -511,7 +502,7 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) { id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ; if( !lem.isNull() ){ Trace("quant-engine-red") << "...alpha equivalence success." << std::endl; - ++(d_statistics.d_red_alpha_equiv); + ++(d_qstate.getStats().d_red_alpha_equiv); } } d_quants_red_lem[q] = lem; @@ -535,7 +526,7 @@ void QuantifiersEngine::registerQuantifierInternal(Node f) Trace("quant") << "QuantifiersEngine : Register quantifier "; Trace("quant") << " : " << f << std::endl; size_t prev_lemma_waiting = d_qim.numPendingLemmas(); - ++(d_statistics.d_num_quant); + ++(d_qstate.getStats().d_num_quant); Assert(f.getKind() == FORALL); // register with utilities for (unsigned i = 0; i < d_util.size(); i++) @@ -666,44 +657,6 @@ void QuantifiersEngine::getSkolemTermVectors( d_qim.getSkolemize()->getSkolemTermVectors(sks); } -QuantifiersEngine::Statistics::Statistics() - : d_time("theory::QuantifiersEngine::time"), - d_qcf_time("theory::QuantifiersEngine::time_qcf"), - d_ematching_time("theory::QuantifiersEngine::time_ematching"), - d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), - d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), - d_instantiation_rounds_lc( - "QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), - d_triggers("QuantifiersEngine::Triggers", 0), - d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), - d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), - d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0) -{ - smtStatisticsRegistry()->registerStat(&d_time); - smtStatisticsRegistry()->registerStat(&d_qcf_time); - smtStatisticsRegistry()->registerStat(&d_ematching_time); - smtStatisticsRegistry()->registerStat(&d_num_quant); - smtStatisticsRegistry()->registerStat(&d_instantiation_rounds); - smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc); - smtStatisticsRegistry()->registerStat(&d_triggers); - smtStatisticsRegistry()->registerStat(&d_simple_triggers); - smtStatisticsRegistry()->registerStat(&d_multi_triggers); - smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv); -} - -QuantifiersEngine::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_time); - smtStatisticsRegistry()->unregisterStat(&d_qcf_time); - smtStatisticsRegistry()->unregisterStat(&d_ematching_time); - smtStatisticsRegistry()->unregisterStat(&d_num_quant); - smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds); - smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc); - smtStatisticsRegistry()->unregisterStat(&d_triggers); - smtStatisticsRegistry()->unregisterStat(&d_simple_triggers); - smtStatisticsRegistry()->unregisterStat(&d_multi_triggers); - smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv); -} - Node QuantifiersEngine::getNameForQuant(Node q) const { return d_qreg.getNameForQuant(q); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index cb60c8e88..15ea004e2 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -24,7 +24,6 @@ #include "context/cdhashset.h" #include "context/cdlist.h" #include "theory/quantifiers/quant_util.h" -#include "util/statistics_registry.h" namespace CVC4 { @@ -38,10 +37,6 @@ class RepSetIterator; namespace quantifiers { -namespace inst { -class TriggerTrie; -} - class FirstOrderModel; class Instantiate; class QModelBuilder; @@ -60,8 +55,6 @@ class TermRegistry; class QuantifiersEngine { friend class ::CVC4::TheoryEngine; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - typedef context::CDList<Node> NodeList; - typedef context::CDList<bool> BoolList; typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; public: @@ -92,8 +85,6 @@ class QuantifiersEngine { quantifiers::FirstOrderModel* getModel() const; /** get term database sygus */ quantifiers::TermDbSygus* getTermDatabaseSygus() const; - /** get trigger database */ - quantifiers::inst::TriggerTrie* getTriggerDatabase() const; //---------------------- end utilities private: //---------------------- private initialization @@ -191,25 +182,6 @@ public: //----------end user interface for instantiations - /** statistics class */ - class Statistics - { - public: - TimerStat d_time; - TimerStat d_qcf_time; - TimerStat d_ematching_time; - IntStat d_num_quant; - IntStat d_instantiation_rounds; - IntStat d_instantiation_rounds_lc; - IntStat d_triggers; - IntStat d_simple_triggers; - IntStat d_multi_triggers; - IntStat d_red_alpha_equiv; - Statistics(); - ~Statistics(); - };/* class QuantifiersEngine::Statistics */ - Statistics d_statistics; - private: /** The quantifiers state object */ quantifiers::QuantifiersState& d_qstate; @@ -230,8 +202,6 @@ public: quantifiers::QuantifiersRegistry& d_qreg; /** The term registry */ quantifiers::TermRegistry& d_treg; - /** all triggers will be stored in this trie */ - std::unique_ptr<quantifiers::inst::TriggerTrie> d_tr_trie; /** extended model object */ quantifiers::FirstOrderModel* d_model; //------------- end quantifiers utilities |