From 246a0bc47aa23f3d4225a78e0600094d0e6ac639 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 17 Aug 2019 13:50:31 -0500 Subject: [PATCH] Move quantifiers relevance module inside E-matching module (#3186) --- .../ematching/inst_strategy_e_matching.cpp | 41 ++++++++++---- .../ematching/inst_strategy_e_matching.h | 18 ++++-- .../ematching/instantiation_engine.cpp | 55 ++++++++++++------- .../ematching/instantiation_engine.h | 7 ++- src/theory/quantifiers_engine.cpp | 10 ---- src/theory/quantifiers_engine.h | 5 -- 6 files changed, 81 insertions(+), 55 deletions(-) diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index c4b15a852..876e4e369 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -42,11 +42,11 @@ namespace quantifiers { // user-pat=interleave alternates between use and resort struct sortQuantifiersForSymbol { - QuantifiersEngine* d_qe; + QuantRelevance* d_quant_rel; std::map< Node, Node > d_op_map; bool operator() (Node i, Node j) { - int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_op_map[i] ); - int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_op_map[j] ); + int nqfsi = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[i]); + int nqfsj = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[j]); if( nqfsinqfsj ){ @@ -155,7 +155,10 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){ } } -InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){ +InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(QuantifiersEngine* qe, + QuantRelevance* qr) + : InstStrategy(qe), d_quant_rel(qr) +{ //how to select trigger terms d_tr_strategy = options::triggerSelMode(); //whether to select new triggers during the search @@ -429,8 +432,9 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl; //sort terms based on relevance if( options::relevantTriggers() ){ + Assert(d_quant_rel); sortQuantifiersForSymbol sqfs; - sqfs.d_qe = d_quantEngine; + sqfs.d_quant_rel = d_quant_rel; for( unsigned i=0; igetQuantifierRelevance()->getNumQuantifiersForSymbol( d_pat_to_mpat[patTerms[i]].getOperator() ) << ")" << std::endl; + if (Debug.isOn("relevant-trigger")) + { + Debug("relevant-trigger") + << "Terms based on relevance: " << std::endl; + for (const Node& p : patTerms) + { + Debug("relevant-trigger") + << " " << p << " from " << d_pat_to_mpat[p] << " ("; + Debug("relevant-trigger") + << d_quant_rel->getNumQuantifiersForSymbol( + d_pat_to_mpat[p].getOperator()) + << ")" << std::endl; + } } } //now, generate the trigger... @@ -482,14 +495,18 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ //check if similar patterns exist, and if so, add them additionally unsigned nqfs_curr = 0; if( options::relevantTriggers() ){ - nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() ); + nqfs_curr = d_quant_rel->getNumQuantifiersForSymbol( + patTerms[0].getOperator()); } index++; bool success = true; while( success && indexgetQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){ + if (!options::relevantTriggers() + || d_quant_rel->getNumQuantifiersForSymbol( + patTerms[index].getOperator()) + <= nqfs_curr) + { d_single_trigger_gen[ patTerms[index] ] = true; Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], false, Trigger::TR_RETURN_NULL, d_num_trigger_vars[f] ); addTrigger( tr2, f ); diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index b71b8ee47..1a014939f 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -17,12 +17,9 @@ #ifndef CVC4__INST_STRATEGY_E_MATCHING_H #define CVC4__INST_STRATEGY_E_MATCHING_H -#include "context/context.h" -#include "context/context_mm.h" #include "theory/quantifiers/ematching/instantiation_engine.h" #include "theory/quantifiers/ematching/trigger.h" -#include "util/statistics_registry.h" -#include "options/quantifiers_options.h" +#include "theory/quantifiers/quant_relevance.h" namespace CVC4 { namespace theory { @@ -99,9 +96,11 @@ private: bool hasUserPatterns(Node q); /** has user patterns */ std::map d_hasUserPatterns; + public: - InstStrategyAutoGenTriggers( QuantifiersEngine* qe ); - ~InstStrategyAutoGenTriggers(){} + InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr); + ~InstStrategyAutoGenTriggers() {} + public: /** get auto-generated trigger */ inst::Trigger* getAutoGenTrigger( Node q ); @@ -112,6 +111,13 @@ public: } /** add pattern */ void addUserNoPattern( Node q, Node pat ); + + private: + /** + * Pointer to the module that computes relevance of quantifiers, which is + * owned by the instantiation engine that owns this class. + */ + QuantRelevance* d_quant_rel; };/* class InstStrategyAutoGenTriggers */ diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index bb70002a0..2fe28fc61 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -36,7 +36,13 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe) d_instStrategies(), d_isup(), d_i_ag(), - d_quants() { + d_quants(), + d_quant_rel(nullptr) +{ + if (options::relevantTriggers()) + { + d_quant_rel.reset(new quantifiers::QuantRelevance); + } if (options::eMatching()) { // these are the instantiation strategies for E-matching // user-provided patterns @@ -46,7 +52,8 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe) } // auto-generated patterns - d_i_ag.reset(new InstStrategyAutoGenTriggers(d_quantEngine)); + d_i_ag.reset( + new InstStrategyAutoGenTriggers(d_quantEngine, d_quant_rel.get())); d_instStrategies.push_back(d_i_ag.get()); } } @@ -175,24 +182,32 @@ void InstantiationEngine::checkOwnership(Node q) } } -void InstantiationEngine::registerQuantifier( Node f ){ - if( d_quantEngine->hasOwnership( f, this ) ){ - //for( unsigned i=0; iregisterQuantifier( f ); - //} - //take into account user patterns - if( f.getNumChildren()==3 ){ - Node subsPat = - d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants( - f[2], f); - //add patterns - for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){ - //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl; - if( subsPat[i].getKind()==INST_PATTERN ){ - addUserPattern( f, subsPat[i] ); - }else if( subsPat[i].getKind()==INST_NO_PATTERN ){ - addUserNoPattern( f, subsPat[i] ); - } +void InstantiationEngine::registerQuantifier(Node q) +{ + if (!d_quantEngine->hasOwnership(q, this)) + { + return; + } + if (d_quant_rel) + { + d_quant_rel->registerQuantifier(q); + } + // take into account user patterns + if (q.getNumChildren() == 3) + { + Node subsPat = + d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants( + q[2], q); + // add patterns + for (const Node& p : subsPat) + { + if (p.getKind() == INST_PATTERN) + { + addUserPattern(q, p); + } + else if (p.getKind() == INST_NO_PATTERN) + { + addUserNoPattern(q, p); } } } diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index b959bef2d..26fc3767b 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -19,6 +19,7 @@ #include +#include "theory/quantifiers/quant_relevance.h" #include "theory/quantifiers/quant_util.h" namespace CVC4 { @@ -50,8 +51,6 @@ public: virtual int process( Node f, Theory::Effort effort, int e ) = 0; /** identify */ virtual std::string identify() const { return std::string("Unknown"); } - /** register quantifier */ - //virtual void registerQuantifier( Node q ) {} };/* class InstStrategy */ class InstantiationEngine : public QuantifiersModule { @@ -87,6 +86,10 @@ class InstantiationEngine : public QuantifiersModule { void addUserNoPattern(Node q, Node pat); /** Identify this module */ std::string identify() const override { return "InstEngine"; } + + private: + /** for computing relevance of quantifiers */ + std::unique_ptr d_quant_rel; }; /* class InstantiationEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index c17af1e1f..5bac55462 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -189,7 +189,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_eq_inference(nullptr), d_tr_trie(new inst::TriggerTrie), d_model(nullptr), - d_quant_rel(nullptr), d_rel_dom(nullptr), d_bv_invert(nullptr), d_builder(nullptr), @@ -253,11 +252,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; - if( options::relevantTriggers() ){ - d_quant_rel.reset(new quantifiers::QuantRelevance); - d_util.push_back(d_quant_rel.get()); - } - if( options::quantEpr() ){ Assert( !options::incrementalSolving() ); d_qepr.reset(new quantifiers::QuantEPR); @@ -351,10 +345,6 @@ quantifiers::BvInverter* QuantifiersEngine::getBvInverter() const { return d_bv_invert.get(); } -quantifiers::QuantRelevance* QuantifiersEngine::getQuantifierRelevance() const -{ - return d_quant_rel.get(); -} quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const { return d_builder.get(); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 7a9f5e7da..dfe8a44ad 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -34,7 +34,6 @@ #include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_epr.h" -#include "theory/quantifiers/quant_relevance.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/relevant_domain.h" @@ -117,8 +116,6 @@ public: quantifiers::RelevantDomain* getRelevantDomain() const; /** get the BV inverter utility */ quantifiers::BvInverter* getBvInverter() const; - /** get quantifier relevance */ - quantifiers::QuantRelevance* getQuantifierRelevance() const; //---------------------- end utilities //---------------------- modules (TODO remove these #1163) /** get bounded integers utility */ @@ -310,8 +307,6 @@ public: std::unique_ptr d_tr_trie; /** extended model object */ std::unique_ptr d_model; - /** for computing relevance of quantifiers */ - std::unique_ptr d_quant_rel; /** relevant domain */ std::unique_ptr d_rel_dom; /** inversion utility for BV instantiation */ -- 2.30.2