diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-12-17 13:43:44 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-17 13:43:44 -0800 |
commit | e9499c41f405df8b42fd9ae10004b1b91a869106 (patch) | |
tree | fa1475f43a3e61b8f6ffdcb903b65919eba28661 /src/theory/quantifiers/ematching | |
parent | 9b2914ed9f7b14ecf535ffe9e1328d0fa042e072 (diff) |
Generate code for options with modes. (#3561)
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
Diffstat (limited to 'src/theory/quantifiers/ematching')
5 files changed, 148 insertions, 76 deletions
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 3420f282d..40216f7c9 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -85,14 +85,17 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ if( e==0 ){ return STATUS_UNFINISHED; }else{ - int peffort = d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ? 2 : 1; + int peffort = + d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT ? 2 + : 1; if( e<peffort ){ return STATUS_UNFINISHED; }else if( e==peffort ){ d_counter[f]++; Trace("inst-alg") << "-> User-provided instantiate " << f << "..." << std::endl; - if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){ + if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT) + { for( unsigned i=0; i<d_user_gen_wait[f].size(); i++ ){ Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], true, Trigger::TR_RETURN_NULL ); if( t ){ @@ -142,9 +145,12 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){ if( usable ){ Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl; //check match option - if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){ + if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT) + { d_user_gen_wait[q].push_back( nodes ); - }else{ + } + else + { Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW ); if( t ){ d_user_gen[q].push_back( t ); @@ -187,11 +193,17 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort } int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){ - UserPatMode upMode = d_quantEngine->getInstUserPatMode(); - if( hasUserPatterns( f ) && upMode==USER_PAT_MODE_TRUST ){ + options::UserPatMode upMode = d_quantEngine->getInstUserPatMode(); + if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST) + { return STATUS_UNKNOWN; - }else{ - int peffort = ( hasUserPatterns( f ) && upMode!=USER_PAT_MODE_IGNORE && upMode!=USER_PAT_MODE_RESORT ) ? 2 : 1; + } + else + { + int peffort = (hasUserPatterns(f) && upMode != options::UserPatMode::IGNORE + && upMode != options::UserPatMode::RESORT) + ? 2 + : 1; if( e<peffort ){ return STATUS_UNFINISHED; }else{ @@ -219,17 +231,22 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) // d_processed_trigger.clear(); // d_quantEngine->getEqualityQuery()->setLiberal( true ); //} - if( options::triggerActiveSelMode()!=TRIGGER_ACTIVE_SEL_ALL ){ + if (options::triggerActiveSelMode() != options::TriggerActiveSelMode::ALL) + { int max_score = -1; Trigger * max_trigger = NULL; for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[0][f].begin(); itt != d_auto_gen_trigger[0][f].end(); ++itt ){ int score = itt->first->getActiveScore(); - if( options::triggerActiveSelMode()==TRIGGER_ACTIVE_SEL_MIN ){ + if (options::triggerActiveSelMode() + == options::TriggerActiveSelMode::MIN) + { if( score>=0 && ( score<max_score || max_score<0 ) ){ max_score = score; max_trigger = itt->first; - } - }else{ + } + } + else + { if( score>max_score ){ max_score = score; max_trigger = itt->first; @@ -241,7 +258,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) d_auto_gen_trigger[0][f][max_trigger] = true; } } - + bool hasInst = false; for( unsigned r=0; r<2; r++ ){ for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[r][f].begin(); itt != d_auto_gen_trigger[r][f].end(); ++itt ){ @@ -374,20 +391,28 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ }else{ Assert(Trigger::isAtomicTrigger(pat)); if( pat.getType().isBoolean() && rpoleq.isNull() ){ - if( options::literalMatchMode()==LITERAL_MATCH_USE ){ + if (options::literalMatchMode() == options::LiteralMatchMode::USE) + { pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate(); - }else if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){ + } + else if (options::literalMatchMode() + != options::LiteralMatchMode::NONE) + { pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==1 ) ); } }else{ Assert(!rpoleq.isNull()); if( rpol==-1 ){ - if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){ + if (options::literalMatchMode() + != options::LiteralMatchMode::NONE) + { //all equivalence classes except rpoleq pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate(); } }else if( rpol==1 ){ - if( options::literalMatchMode()==LITERAL_MATCH_AGG ){ + if (options::literalMatchMode() + == options::LiteralMatchMode::AGG) + { //only equivalence class rpoleq pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ); } diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index 1a014939f..052bc910c 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -54,63 +54,67 @@ public: std::string identify() const override { return std::string("UserPatterns"); } };/* class InstStrategyUserPatterns */ -class InstStrategyAutoGenTriggers : public InstStrategy { -public: - enum { +class InstStrategyAutoGenTriggers : public InstStrategy +{ + public: + enum + { RELEVANCE_NONE, RELEVANCE_DEFAULT, }; -private: + + private: /** trigger generation strategy */ - TriggerSelMode d_tr_strategy; + options::TriggerSelMode d_tr_strategy; /** regeneration */ bool d_regenerate; int d_regenerate_frequency; /** (single,multi) triggers for each quantifier */ - std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger[2]; - std::map< Node, int > d_counter; + std::map<Node, std::map<inst::Trigger*, bool> > d_auto_gen_trigger[2]; + std::map<Node, int> d_counter; /** single, multi triggers for each quantifier */ - std::map< Node, std::vector< Node > > d_patTerms[2]; - std::map< Node, std::map< Node, bool > > d_patReqPol; + std::map<Node, std::vector<Node> > d_patTerms[2]; + std::map<Node, std::map<Node, bool> > d_patReqPol; /** information about triggers */ - std::map< Node, bool > d_is_single_trigger; - std::map< Node, bool > d_single_trigger_gen; - std::map< Node, bool > d_made_multi_trigger; - //processed trigger this round - std::map< Node, std::map< inst::Trigger*, bool > > d_processed_trigger; - //instantiation no patterns - std::map< Node, std::vector< Node > > d_user_no_gen; + std::map<Node, bool> d_is_single_trigger; + std::map<Node, bool> d_single_trigger_gen; + std::map<Node, bool> d_made_multi_trigger; + // processed trigger this round + std::map<Node, std::map<inst::Trigger*, bool> > d_processed_trigger; + // instantiation no patterns + std::map<Node, std::vector<Node> > d_user_no_gen; // number of trigger variables per quantifier - std::map< Node, unsigned > d_num_trigger_vars; - std::map< Node, Node > d_vc_partition[2]; - std::map< Node, Node > d_pat_to_mpat; -private: + std::map<Node, unsigned> d_num_trigger_vars; + std::map<Node, Node> d_vc_partition[2]; + std::map<Node, Node> d_pat_to_mpat; + + private: /** process functions */ - void processResetInstantiationRound(Theory::Effort effort) override; - int process(Node q, Theory::Effort effort, int e) override; - /** generate triggers */ - void generateTriggers(Node q); - void addPatternToPool(Node q, Node pat, unsigned num_fv, Node mpat); - void addTrigger(inst::Trigger* tr, Node f); - /** has user patterns */ - bool hasUserPatterns(Node q); - /** has user patterns */ - std::map<Node, bool> d_hasUserPatterns; + void processResetInstantiationRound(Theory::Effort effort) override; + int process(Node q, Theory::Effort effort, int e) override; + /** generate triggers */ + void generateTriggers(Node q); + void addPatternToPool(Node q, Node pat, unsigned num_fv, Node mpat); + void addTrigger(inst::Trigger* tr, Node f); + /** has user patterns */ + bool hasUserPatterns(Node q); + /** has user patterns */ + std::map<Node, bool> d_hasUserPatterns; -public: - InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr); - ~InstStrategyAutoGenTriggers() {} + public: + InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr); + ~InstStrategyAutoGenTriggers() {} -public: + public: /** get auto-generated trigger */ - inst::Trigger* getAutoGenTrigger( Node q ); + inst::Trigger* getAutoGenTrigger(Node q); /** identify */ std::string identify() const override { return std::string("AutoGenTriggers"); } /** add pattern */ - void addUserNoPattern( Node q, Node pat ); + void addUserNoPattern(Node q, Node pat); private: /** @@ -118,9 +122,7 @@ public: * owned by the instantiation engine that owns this class. */ QuantRelevance* d_quant_rel; -};/* class InstStrategyAutoGenTriggers */ - - +}; /* class InstStrategyAutoGenTriggers */ } }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 23b1ff6c9..b91a9ba63 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -46,7 +46,8 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe) if (options::eMatching()) { // these are the instantiation strategies for E-matching // user-provided patterns - if (options::userPatternsQuant() != USER_PAT_MODE_IGNORE) { + if (options::userPatternsQuant() != options::UserPatMode::IGNORE) + { d_isup.reset(new InstStrategyUserPatterns(d_quantEngine)); d_instStrategies.push_back(d_isup.get()); } diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index f539bccf5..e177e24a6 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -429,9 +429,19 @@ bool Trigger::isSimpleTrigger( Node n ){ } //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula -void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, - quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added, - bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable ){ +void Trigger::collectPatTerms2(Node q, + Node n, + std::map<Node, std::vector<Node> >& visited, + std::map<Node, TriggerTermInfo>& tinfo, + options::TriggerSelMode tstrt, + std::vector<Node>& exclude, + std::vector<Node>& added, + bool pol, + bool hasPol, + bool epol, + bool hasEPol, + bool knowIsUsable) +{ std::map< Node, std::vector< Node > >::iterator itv = visited.find( n ); if( itv==visited.end() ){ visited[ n ].clear(); @@ -488,7 +498,10 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod Assert(added2[i] != nu); // if child was not already removed if( tinfo.find( added2[i] )!=tinfo.end() ){ - if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){ + if (tstrt == options::TriggerSelMode::MAX + || (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX + && !nu_single)) + { // discard all subterms // do not remove if it has smaller weight if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight) @@ -498,7 +511,9 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod visited[added2[i]].clear(); tinfo.erase(added2[i]); } - }else{ + } + else + { if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){ if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight) { @@ -516,9 +531,15 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod } } } - if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){ + if (rm_nu + && (tstrt == options::TriggerSelMode::MIN + || (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL + && nu_single))) + { tinfo.erase( nu ); - }else{ + } + else + { if( std::find( added.begin(), added.end(), nu )==added.end() ){ added.push_back( nu ); } @@ -593,14 +614,21 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< return true; } -void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, - std::map< Node, TriggerTermInfo >& tinfo, bool filterInst ){ +void Trigger::collectPatTerms(Node q, + Node n, + std::vector<Node>& patTerms, + options::TriggerSelMode tstrt, + std::vector<Node>& exclude, + std::map<Node, TriggerTermInfo>& tinfo, + bool filterInst) +{ std::map< Node, std::vector< Node > > visited; if( filterInst ){ //immediately do not consider any term t for which another term is an instance of t std::vector< Node > patTerms2; std::map< Node, TriggerTermInfo > tinfo2; - collectPatTerms( q, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo2, false ); + collectPatTerms( + q, n, patTerms2, options::TriggerSelMode::ALL, exclude, tinfo2, false); std::vector< Node > temp; temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); filterTriggerInstances(temp); @@ -623,7 +651,8 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu Trace("trigger-filter-instance") << std::endl; } } - if( tstrt==quantifiers::TRIGGER_SEL_ALL ){ + if (tstrt == options::TriggerSelMode::ALL) + { for( unsigned i=0; i<temp.size(); i++ ){ //copy information tinfo[temp[i]].d_fv.insert( tinfo[temp[i]].d_fv.end(), tinfo2[temp[i]].d_fv.begin(), tinfo2[temp[i]].d_fv.end() ); @@ -632,7 +661,9 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu patTerms.push_back( temp[i] ); } return; - }else{ + } + else + { //do not consider terms that have instances for( unsigned i=0; i<patTerms2.size(); i++ ){ if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){ @@ -875,7 +906,7 @@ void Trigger::getTriggerVariables(Node n, Node q, std::vector<Node>& t_vars) std::map< Node, TriggerTermInfo > tinfo; // collect all patterns from n std::vector< Node > exclude; - collectPatTerms(q, n, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo); + collectPatTerms(q, n, patTerms, options::TriggerSelMode::ALL, exclude, tinfo); //collect all variables from all patterns in patTerms, add to t_vars for (const Node& pat : patTerms) { diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index d47ea72ee..e955543db 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -273,9 +273,13 @@ class Trigger { * in the vector we are returning, e.g. we do not return f( x ) if we are * also returning f( f( x ) ). TODO: revisit this (issue #1211) */ - static void collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, - std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo, - bool filterInst = false ); + static void collectPatTerms(Node q, + Node n, + std::vector<Node>& patTerms, + options::TriggerSelMode tstrt, + std::vector<Node>& exclude, + std::map<Node, TriggerTermInfo>& tinfo, + bool filterInst = false); /** Is n a usable trigger in quantified formula q? * @@ -380,9 +384,18 @@ class Trigger { * * We add the triggers we collected recursively in n into added. */ - static void collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, - quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added, - bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable = false ); + static void collectPatTerms2(Node q, + Node n, + std::map<Node, std::vector<Node> >& visited, + std::map<Node, TriggerTermInfo>& tinfo, + options::TriggerSelMode tstrt, + std::vector<Node>& exclude, + std::vector<Node>& added, + bool pol, + bool hasPol, + bool epol, + bool hasEPol, + bool knowIsUsable = false); /** filter all nodes that have trigger instances * |