From 821681f181ef9cdced728ba585bec83b3fab16c0 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 24 Oct 2014 15:12:26 +0200 Subject: [PATCH] Add --user-pat=resort. Minor cleanup of options. --- .../quantifiers/inst_strategy_e_matching.cpp | 67 ++++++++++--------- .../quantifiers/inst_strategy_e_matching.h | 2 + src/theory/quantifiers/modes.h | 2 + src/theory/quantifiers/options_handlers.h | 17 +++-- 4 files changed, 52 insertions(+), 36 deletions(-) diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 4abdb66f6..e95936220 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -59,30 +59,39 @@ void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort ef int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ if( e==0 ){ return STATUS_UNFINISHED; - }else if( e==1 ){ - d_counter[f]++; + }else{ + int peffort = options::userPatternsQuant()==USER_PAT_MODE_RESORT ? 2 : 1; + if( e User-provided instantiate " << f << "..." << std::endl; - - Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl; - //Notice() << "Try user-provided patterns..." << std::endl; - for( int i=0; i<(int)d_user_gen[f].size(); i++ ){ - bool processTrigger = true; - if( processTrigger ){ - Trace("process-trigger") << " Process (user) "; - d_user_gen[f][i]->debugPrint("process-trigger"); - Trace("process-trigger") << "..." << std::endl; - InstMatch baseMatch( f ); - int numInst = d_user_gen[f][i]->addInstantiations( baseMatch ); - Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; - d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst; - if( d_user_gen[f][i]->isMultiTrigger() ){ - d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; + if( options::userPatternsQuant()==USER_PAT_MODE_RESORT ){ + int matchOption = 0; + for( unsigned i=0; idebugPrint("process-trigger"); + Trace("process-trigger") << "..." << std::endl; + InstMatch baseMatch( f ); + int numInst = d_user_gen[f][i]->addInstantiations( baseMatch ); + Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; + d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst; + if( d_user_gen[f][i]->isMultiTrigger() ){ + d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; + } + //d_quantEngine->d_hasInstantiated[f] = true; } - //d_quantEngine->d_hasInstantiated[f] = true; } } - Debug("quant-uf-strategy") << "done." << std::endl; - //Notice() << "done" << std::endl; } return STATUS_UNKNOWN; } @@ -106,7 +115,11 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ d_quantEngine->getPhaseReqTerms( f, nodes ); //check match option int matchOption = 0; - d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) ); + if( options::userPatternsQuant()==USER_PAT_MODE_RESORT ){ + d_user_gen_wait[f].push_back( nodes ); + }else{ + d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) ); + } } } @@ -136,11 +149,11 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) if( hasUserPatterns( f ) && options::userPatternsQuant()==USER_PAT_MODE_TRUST ){ return STATUS_UNKNOWN; }else{ - int peffort = ( hasUserPatterns( f ) && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ) ? 2 : 1; - //int peffort = 1; + int peffort = ( hasUserPatterns( f ) && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE && options::userPatternsQuant()!=USER_PAT_MODE_RESORT ) ? 2 : 1; if( e Auto-gen instantiate " << f << "..." << std::endl; int status = STATUS_UNKNOWN; bool gen = false; if( e==peffort ){ @@ -160,14 +173,11 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) Trace("no-trigger") << "Could not find trigger for " << f << std::endl; } } - Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl; //if( e==4 ){ // d_processed_trigger.clear(); // d_quantEngine->getEqualityQuery()->setLiberal( true ); //} - Debug("quant-uf-strategy") << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl; - //Notice() << "Try auto-generated triggers..." << std::endl; for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){ Trigger* tr = itt->first; if( tr ){ @@ -195,8 +205,6 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) //if( e==4 ){ // d_quantEngine->getEqualityQuery()->setLiberal( false ); //} - Debug("quant-uf-strategy") << "done." << std::endl; - //Notice() << "done" << std::endl; return status; } } @@ -281,8 +289,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor 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, options::smartTriggers() ); d_single_trigger_gen[ patTerms[0] ] = true; }else{ //only generate multi trigger if effort level > 5, or if no single triggers exist diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index 935432683..dd4486803 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -36,6 +36,8 @@ class InstStrategyUserPatterns : public InstStrategy{ private: /** explicitly provided patterns */ std::map< Node, std::vector< inst::Trigger* > > d_user_gen; + /** waiting to be generated patterns */ + std::map< Node, std::vector< std::vector< Node > > > d_user_gen_wait; /** counter for quantifiers */ std::map< Node, int > d_counter; /** process functions */ diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 53842b373..acc883f2a 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -103,6 +103,8 @@ typedef enum { USER_PAT_MODE_USE, /** default, if patterns are supplied for a quantifier, use only those */ USER_PAT_MODE_TRUST, + /** resort to user patterns only when necessary */ + USER_PAT_MODE_RESORT, /** ignore user patterns */ USER_PAT_MODE_IGNORE, } UserPatMode; diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 461dbafe9..c2afbbd3e 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -148,6 +148,9 @@ use \n\ + Use both user-provided and auto-generated patterns when patterns\n\ are provided for a quantified formula.\n\ \n\ +resort \n\ ++ Use user-provided patterns only after auto-generated patterns saturate.\n\ +\n\ ignore \n\ + Ignore user-provided patterns. \n\ \n\ @@ -181,11 +184,11 @@ none \n\ static const std::string cegqiFairModeHelp = "\ Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --cegqi-fair:\n\ \n\ -default \n\ -+ Default, enforce fairness using an uninterpreted function for datatypes size.\n\ +uf-dt-size \n\ ++ Enforce fairness using an uninterpreted function for datatypes size.\n\ \n\ -dt-size \n\ -+ Enforce fairness using size theory operator.\n\ +default | dt-size \n\ ++ Default, enforce fairness using size theory operator.\n\ \n\ none \n\ + Do not enforce fairness. \n\ @@ -326,6 +329,8 @@ inline UserPatMode stringToUserPatMode(std::string option, std::string optarg, S return USER_PAT_MODE_USE; } else if(optarg == "default" || optarg == "trust") { return USER_PAT_MODE_TRUST; + } else if(optarg == "resort") { + return USER_PAT_MODE_RESORT; } else if(optarg == "ignore") { return USER_PAT_MODE_IGNORE; } else if(optarg == "help") { @@ -370,9 +375,9 @@ inline PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string o } inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default" || optarg == "uf-dt-size" ) { + if(optarg == "uf-dt-size" ) { return CEGQI_FAIR_UF_DT_SIZE; - } else if(optarg == "dt-size") { + } else if(optarg == "default" || optarg == "dt-size") { return CEGQI_FAIR_DT_SIZE; } else if(optarg == "none") { return CEGQI_FAIR_NONE; -- 2.30.2