From 576d50ac7c13233a589771401537b587eb36361e Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 4 Apr 2016 17:18:36 -0500 Subject: [PATCH] New options for trigger selection, add option --strict-triggers. Do not infer alpha equivalence for quantifiers with annotations, limit rewrite operations when triggers are trusted. --- src/options/options_handler.cpp | 18 ++++-- src/options/quantifiers_modes.h | 4 ++ src/options/quantifiers_options | 6 +- src/smt/smt_engine.cpp | 5 ++ src/theory/quantifiers/alpha_equivalence.cpp | 17 +++-- .../quantifiers/inst_strategy_e_matching.cpp | 22 +++---- .../quantifiers/inst_strategy_e_matching.h | 3 +- .../quantifiers/instantiation_engine.cpp | 16 +++++ src/theory/quantifiers/instantiation_engine.h | 1 + src/theory/quantifiers/model_builder.cpp | 2 +- .../quantifiers/quantifiers_rewriter.cpp | 17 +++-- src/theory/quantifiers/term_database.cpp | 12 ++-- src/theory/quantifiers/term_database.h | 3 +- src/theory/quantifiers/trigger.cpp | 64 ++++++++----------- src/theory/quantifiers/trigger.h | 20 ++---- src/theory/quantifiers_engine.cpp | 11 ++-- src/theory/quantifiers_engine.h | 3 +- 17 files changed, 126 insertions(+), 98 deletions(-) diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 90202d6f5..d08f5f533 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -347,15 +347,21 @@ interleave \n\ const std::string OptionsHandler::s_triggerSelModeHelp = "\ Trigger selection modes currently supported by the --trigger-sel option:\n\ \n\ -default \n\ -+ Default, consider all subterms of quantified formulas for trigger selection.\n\ -\n\ -min \n\ +min | default \n\ + Consider only minimal subterms that meet criteria for triggers.\n\ \n\ max \n\ + Consider only maximal subterms that meet criteria for triggers. \n\ \n\ +all \n\ ++ Consider all subterms that meet criteria for triggers. \n\ +\n\ +min-s-max \n\ ++ Consider only minimal subterms that meet criteria for single triggers, maximal otherwise. \n\ +\n\ +min-s-all \n\ ++ Consider only minimal subterms that meet criteria for single triggers, all otherwise. \n\ +\n\ "; const std::string OptionsHandler::s_prenexQuantModeHelp = "\ Prenex quantifiers modes currently supported by the --prenex-quant option:\n\ @@ -608,6 +614,10 @@ theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std:: return theory::quantifiers::TRIGGER_SEL_MIN; } else if(optarg == "max") { return theory::quantifiers::TRIGGER_SEL_MAX; + } else if(optarg == "min-s-max") { + return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX; + } else if(optarg == "min-s-all") { + return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL; } else if(optarg == "all") { return theory::quantifiers::TRIGGER_SEL_ALL; } else if(optarg == "help") { diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 8ecf65a33..a437cfc97 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -107,6 +107,10 @@ enum TriggerSelMode { TRIGGER_SEL_MIN, /** only consider maximal terms for triggers */ TRIGGER_SEL_MAX, + /** consider minimal terms for single triggers, maximal for non-single */ + TRIGGER_SEL_MIN_SINGLE_MAX, + /** consider minimal terms for single triggers, all for non-single */ + TRIGGER_SEL_MIN_SINGLE_ALL, /** consider all terms for triggers */ TRIGGER_SEL_ALL, }; diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 5f23a02e0..8ed4f24c0 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -69,8 +69,8 @@ option inferArithTriggerEq --infer-arith-trigger-eq bool :default false option inferArithTriggerEqExp --infer-arith-trigger-eq-exp bool :default false record explanations for inferArithTriggerEq -option smartTriggers --smart-triggers bool :default true - enable smart triggers +option strictTriggers --strict-triggers bool :default false + only instantiate quantifiers with user patterns based on triggers option relevantTriggers --relevant-triggers bool :default false prefer triggers that are more relevant based on SInE style analysis option relationalTriggers --relational-triggers bool :default false @@ -89,7 +89,7 @@ option multiTriggerPriority --multi-trigger-priority bool :default false only try multi triggers if single triggers give no instantiations option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "options/quantifiers_modes.h" :handler stringToTriggerSelMode selection mode for triggers -option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "options/quantifiers_modes.h" :handler stringToUserPatMode +option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :read-write :include "options/quantifiers_modes.h" :handler stringToUserPatMode policy for handling user-provided patterns for quantifier instantiation option incrementTriggers --increment-triggers bool :default true generate additional triggers as needed during search diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ddbb9eef7..bff8e187f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1846,6 +1846,11 @@ void SmtEngine::setDefaults() { } } //implied options... + if( options::strictTriggers() ){ + if( !options::userPatternsQuant.wasSetByUser() ){ + options::userPatternsQuant.set( quantifiers::USER_PAT_MODE_TRUST ); + } + } if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); } diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 16a9d3bc7..8abc3f65a 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -54,12 +54,17 @@ bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE aen->d_quant = q; return true; }else{ - //lemma ( q <=> d_quant ) - Trace("quant-ae") << "Alpha equivalent : " << std::endl; - Trace("quant-ae") << " " << q << std::endl; - Trace("quant-ae") << " " << aen->d_quant << std::endl; - qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) ); - return false; + if( q.getNumChildren()==2 ){ + //lemma ( q <=> d_quant ) + Trace("quant-ae") << "Alpha equivalent : " << std::endl; + Trace("quant-ae") << " " << q << std::endl; + Trace("quant-ae") << " " << aen->d_quant << std::endl; + qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) ); + return false; + }else{ + //do not reduce annotated quantified formulas based on alpha equivalence + return true; + } } } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index d43d7a792..491da7116 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -13,8 +13,6 @@ **/ #include "theory/quantifiers/inst_strategy_e_matching.h" - -#include "options/quantifiers_options.h" #include "theory/quantifiers/inst_match_generator.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/term_database.h" @@ -85,7 +83,7 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){ int matchOption = 0; for( unsigned i=0; igetInstUserPatMode()==USER_PAT_MODE_RESORT ){ d_user_gen_wait[q].push_back( nodes ); }else{ - d_user_gen[q].push_back( Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) ); + d_user_gen[q].push_back( Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW ) ); } } } InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){ //how to select trigger terms - if( options::triggerSelMode()==TRIGGER_SEL_MIN || options::triggerSelMode()==TRIGGER_SEL_DEFAULT ){ - d_tr_strategy = Trigger::TS_MIN_TRIGGER; - }else if( options::triggerSelMode()==TRIGGER_SEL_MAX ){ - d_tr_strategy = Trigger::TS_MAX_TRIGGER; + if( options::triggerSelMode()==quantifiers::TRIGGER_SEL_DEFAULT ){ + d_tr_strategy = quantifiers::TRIGGER_SEL_MIN; }else{ - d_tr_strategy = Trigger::TS_ALL; + d_tr_strategy = options::triggerSelMode(); } //whether to select new triggers during the search if( options::incrementTriggers() ){ @@ -358,7 +354,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ int matchOption = 0; Trigger* tr = NULL; if( d_is_single_trigger[ patTerms[0] ] ){ - tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL, options::smartTriggers() ); + tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL ); d_single_trigger_gen[ patTerms[0] ] = true; }else{ //only generate multi trigger if option set, or if no single triggers exist @@ -376,7 +372,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_made_multi_trigger[f] = true; } //will possibly want to get an old trigger - tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD, options::smartTriggers() ); + tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD ); } if( tr ){ unsigned tindex; @@ -412,7 +408,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if( !options::relevantTriggers() || d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){ d_single_trigger_gen[ patTerms[index] ] = true; - Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL, options::smartTriggers() ); + Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL ); if( tr2 ){ //Notice() << "Add additional trigger " << patTerms[index] << std::endl; tr2->resetInstantiationRound(); @@ -484,7 +480,7 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) { } Trace("local-t-ext") << std::endl; int matchOption = 0; - Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, true, Trigger::TR_GET_OLD, options::smartTriggers() ); + Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, true, Trigger::TR_GET_OLD ); d_lte_trigger[f] = tr; }else{ Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index ac4eb9d98..d48084514 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -23,6 +23,7 @@ #include "theory/quantifiers/trigger.h" #include "theory/quantifiers_engine.h" #include "util/statistics_registry.h" +#include "options/quantifiers_options.h" namespace CVC4 { namespace theory { @@ -64,7 +65,7 @@ public: }; private: /** trigger generation strategy */ - int d_tr_strategy; + TriggerSelMode d_tr_strategy; /** regeneration */ bool d_regenerate; int d_regenerate_frequency; diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index f98ab2b7c..8e88d3434 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -165,6 +165,22 @@ bool InstantiationEngine::isIncomplete( Node q ) { return true; } +void InstantiationEngine::preRegisterQuantifier( Node q ) { + if( options::strictTriggers() && q.getNumChildren()==3 ){ + //if strict triggers, take ownership of this quantified formula + bool hasPat = false; + for( unsigned i=0; isetOwner( q, this, 1 ); + } + } +} + void InstantiationEngine::registerQuantifier( Node f ){ if( d_quantEngine->hasOwnership( f, this ) ){ //for( unsigned i=0; i children; @@ -251,6 +252,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { if( doOperation( in, op, qa ) ){ ret = computeOperation( in, op, qa ); if( ret!=in ){ + rew_op = op; status = REWRITE_AGAIN_FULL; break; } @@ -260,7 +262,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { } //print if changed if( in!=ret ){ - Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl; + Trace("quantifiers-rewrite") << "*** rewrite (op=" << rew_op << ") " << in << std::endl; Trace("quantifiers-rewrite") << " to " << std::endl; Trace("quantifiers-rewrite") << ret << std::endl; } @@ -1537,8 +1539,9 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg return mkForAll( args, body, qa ); } -bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& qa ){ - bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef(); +bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& qa ){ + bool is_strict_trigger = qa.d_hasPattern && options::userPatternsQuant()==USER_PAT_MODE_TRUST; + bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef() && !is_strict_trigger; if( computeOption==COMPUTE_ELIM_SYMBOLS ){ return true; }else if( computeOption==COMPUTE_MINISCOPING ){ @@ -1551,15 +1554,15 @@ bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& q return true; //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); }else if( computeOption==COMPUTE_COND_SPLIT ){ - return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && is_std; + return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && !is_strict_trigger; }else if( computeOption==COMPUTE_PRENEX ){ - return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); + return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std; }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std; //}else if( computeOption==COMPUTE_CNF ){ // return options::cnfQuant(); }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ - return options::purifyQuant(); + return options::purifyQuant() && is_std; }else{ return false; } @@ -1617,7 +1620,7 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut std::vector< Node > children; children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); children.push_back( n ); - if( !qa.d_ipl.isNull() ){ + if( !qa.d_ipl.isNull() && args.size()==f[0].getNumChildren() ){ children.push_back( qa.d_ipl ); } return NodeManager::currentNM()->mkNode(kind::FORALL, children ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 372aefaf4..5d20a7048 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1945,7 +1945,7 @@ void TermDb::computeAttributes( Node q ) { Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl; } //set rewrite engine as owner - d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() ); + d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine(), 2 ); } if( d_qattr[q].isFunDef() ){ Node f = d_qattr[q].d_fundef_f; @@ -1954,19 +1954,19 @@ void TermDb::computeAttributes( Node q ) { exit( 1 ); } d_fun_defs[f] = true; - d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() ); + d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 ); } if( d_qattr[q].d_sygus ){ if( d_quantEngine->getCegInstantiation()==NULL ){ Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; } - d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); + d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 ); } if( d_qattr[q].d_synthesis ){ if( d_quantEngine->getCegInstantiation()==NULL ){ Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; } - d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); + d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 ); } } @@ -1976,7 +1976,9 @@ void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){ qa.d_ipl = q[2]; for( unsigned i=0; i& nodes, - int matchOption, bool smartTriggers ) +Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption ) : d_quantEngine( qe ), d_f( f ) { d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() ); Trace("trigger") << "Trigger for " << f << ": " << std::endl; - for( int i=0; i<(int)d_nodes.size(); i++ ){ + for( unsigned i=0; isetActiveAdd(true); - } + if( d_nodes.size()==1 ){ + if( isSimpleTrigger( d_nodes[0] ) ){ + d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] ); }else{ - d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe ); - //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); - //d_mg->setActiveAdd(); + d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe ); + d_mg->setActiveAdd(true); } }else{ - d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes, qe ); - d_mg->setActiveAdd(true); + d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe ); + //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); + //d_mg->setActiveAdd(); } if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ @@ -68,11 +58,10 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, ++(qe->d_statistics.d_simple_triggers); } }else{ - Trace("multi-trigger") << "Multi-trigger "; - debugPrint("multi-trigger"); - Trace("multi-trigger") << " for " << f << std::endl; - //Notice() << "Multi-trigger for " << f << " : " << std::endl; - //Notice() << " " << (*this) << std::endl; + Trace("multi-trigger") << "Trigger for " << f << ": " << std::endl; + for( unsigned i=0; id_statistics.d_multi_triggers); } //Notice() << "Trigger : " << (*this) << " for " << f << std::endl; @@ -123,8 +112,7 @@ int Trigger::addInstantiations( InstMatch& baseMatch ){ return addedLemmas; } -Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption, - bool smartTriggers ){ +Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption ){ std::vector< Node > trNodes; if( !keepAll ){ //only take nodes that contribute variables to the trigger when added @@ -211,15 +199,15 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } } } - Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers ); + Trigger* t = new Trigger( qe, f, trNodes, matchOption ); qe->getTriggerDatabase()->addTrigger( trNodes, t ); return t; } -Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){ +Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption ){ std::vector< Node > nodes; nodes.push_back( n ); - return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers ); + return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption ); } bool Trigger::isUsable( Node n, Node q ){ @@ -360,7 +348,7 @@ bool Trigger::isSimpleTrigger( Node n ){ //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv, - int tstrt, std::vector< Node >& exclude, + quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::map< Node, int >& reqPol, std::vector< Node >& added, bool pol, bool hasPol, bool epol, bool hasEPol ){ std::map< Node, Node >::iterator itv = visited.find( n ); @@ -371,14 +359,16 @@ bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, if( n.getKind()!=FORALL ){ bool rec = true; Node nu; + bool nu_single = false; if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){ nu = getIsUsableTrigger( n, f, pol, hasPol ); if( !nu.isNull() ){ reqPol[ nu ] = hasEPol ? ( epol ? 1 : -1 ) : 0; visited[ nu ] = nu; quantifiers::TermDb::computeVarContains( nu, visited_fv[ nu ] ); + nu_single = visited_fv[nu].size()==f[0].getNumChildren(); retVal = true; - if( tstrt==TS_MAX_TRIGGER ){ + if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){ rec = false; } } @@ -404,7 +394,7 @@ bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, } added.push_back( added2[i] ); } - if( rm_nu && tstrt==TS_MIN_TRIGGER ){ + if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){ visited[nu] = Node::null(); reqPol.erase( nu ); }else{ @@ -502,14 +492,14 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< return true; } -void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, +void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::map< Node, int >& reqPol, bool filterInst ){ std::map< Node, 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, int > reqPol2; - collectPatTerms( qe, f, n, patTerms2, TS_ALL, exclude, reqPol2, false ); + collectPatTerms( qe, f, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, reqPol2, false ); std::vector< Node > temp; temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); qe->getTermDatabase()->filterInstances( temp ); @@ -525,7 +515,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } Trace("trigger-filter-instance") << std::endl; } - if( tstrt==TS_ALL ){ + if( tstrt==quantifiers::TRIGGER_SEL_ALL ){ for( unsigned i=0; i reqPol; //collect all patterns from icn std::vector< Node > exclude; - collectPatTerms( qe, f, icn, patTerms, TS_ALL, exclude, reqPol ); + collectPatTerms( qe, f, icn, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, reqPol ); //collect all variables from all patterns in patTerms, add to t_vars for( unsigned i=0; igetTermDatabase()->getVarContainsNode( f, patTerms[i], t_vars ); diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 97ed51fe0..06e9011c7 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -21,6 +21,7 @@ #include "expr/node.h" #include "theory/quantifiers/inst_match.h" +#include "options/quantifiers_options.h" // Forward declarations for defining the Trigger and TriggerTrie. namespace CVC4 { @@ -86,20 +87,12 @@ class Trigger { }; static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption = 0, - bool keepAll = true, int trOption = TR_MAKE_NEW, - bool smartTriggers = false ); + bool keepAll = true, int trOption = TR_MAKE_NEW ); static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption = 0, bool keepAll = true, - int trOption = TR_MAKE_NEW, - bool smartTriggers = false ); - //different strategies for choosing trigger terms - enum { - TS_MAX_TRIGGER = 0, - TS_MIN_TRIGGER, - TS_ALL, - }; + int trOption = TR_MAKE_NEW ); static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, - std::vector< Node >& patTerms, int tstrt, + std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::map< Node, int >& reqPol, bool filterInst = false ); /** is usable trigger */ @@ -132,8 +125,7 @@ class Trigger { private: /** trigger constructor */ - Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, - int matchOption = 0, bool smartTriggers = false ); + Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0 ); /** is subterm of trigger usable */ static bool isUsable( Node n, Node q ); @@ -141,7 +133,7 @@ private: bool hasPol = false ); /** collect all APPLY_UF pattern terms for f in n */ static bool collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv, - int tstrt, std::vector< Node >& exclude, + quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::map< Node, int >& reqPol, std::vector< Node >& added, bool pol, bool hasPol, bool epol, bool hasEPol ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ad226681d..1a2762409 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -315,13 +315,17 @@ QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { } } -void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m ) { +void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority ) { QuantifiersModule * mo = getOwner( q ); if( mo!=m ){ if( mo!=NULL ){ - Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << "!" << std::endl; + if( priority<=d_owner_priority[q] ){ + Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << " with higher priority!" << std::endl; + return; + } } d_owner[q] = m; + d_owner_priority[q] = priority; } } @@ -393,9 +397,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } Trace("quant-engine-debug") << std::endl; Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl; - //if( d_model->getNumToReduceQuantifiers()>0 ){ - // Trace("quant-engine-debug") << " # quantified formulas to reduce = " << d_model->getNumToReduceQuantifiers() << std::endl; - //} if( !d_lemmas_waiting.empty() ){ Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 83849cd60..641c7624e 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -271,11 +271,12 @@ public: //modules private: /** owner of quantified formulas */ std::map< Node, QuantifiersModule * > d_owner; + std::map< Node, int > d_owner_priority; public: /** get owner */ QuantifiersModule * getOwner( Node q ); /** set owner */ - void setOwner( Node q, QuantifiersModule * m ); + void setOwner( Node q, QuantifiersModule * m, int priority = 0 ); /** considers */ bool hasOwnership( Node q, QuantifiersModule * m = NULL ); public: -- 2.30.2