diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 49 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.h | 20 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/modes.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/options_handlers.h | 5 |
6 files changed, 19 insertions, 69 deletions
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 414df2882..81771c374 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -29,12 +29,13 @@ using namespace CVC4::theory::inst; using namespace CVC4::theory::quantifiers; //priority levels : -//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers) -//2 : user patterns (when user-pat=resort ), auto gen patterns (for user pattern quantifiers, when user-pat=use) +//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={ignore,resort}) +//2 : user patterns (when user-pat=resort), auto gen patterns (for user pattern quantifiers when user-pat=use) //3 : //4 : //5 : full saturate quantifiers +// user-pat=interleave alternates between use and resort //#define MULTI_TRIGGER_FULL_EFFORT_HALF @@ -67,14 +68,14 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ if( e==0 ){ return STATUS_UNFINISHED; }else{ - int peffort = options::userPatternsQuant()==USER_PAT_MODE_RESORT ? 2 : 1; + int peffort = d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_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( options::userPatternsQuant()==USER_PAT_MODE_RESORT ){ + if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){ int matchOption = 0; 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], matchOption, true, Trigger::TR_RETURN_NULL, options::smartTriggers() ); @@ -125,7 +126,7 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ d_quantEngine->getPhaseReqTerms( f, nodes ); //check match option int matchOption = 0; - if( options::userPatternsQuant()==USER_PAT_MODE_RESORT ){ + if( d_quantEngine->getInstUserPatMode()==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() ) ); @@ -165,10 +166,11 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort } int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){ - if( hasUserPatterns( f ) && options::userPatternsQuant()==USER_PAT_MODE_TRUST ){ + UserPatMode upMode = d_quantEngine->getInstUserPatMode(); + if( hasUserPatterns( f ) && upMode==USER_PAT_MODE_TRUST ){ return STATUS_UNKNOWN; }else{ - int peffort = ( hasUserPatterns( f ) && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE && options::userPatternsQuant()!=USER_PAT_MODE_RESORT ) ? 2 : 1; + int peffort = ( hasUserPatterns( f ) && upMode!=USER_PAT_MODE_IGNORE && upMode!=USER_PAT_MODE_RESORT ) ? 2 : 1; if( e<peffort ){ return STATUS_UNFINISHED; }else{ @@ -417,37 +419,7 @@ void InstStrategyAutoGenTriggers::addUserNoPattern( Node f, Node pat ) { } } - -void InstStrategyLocalTheoryExt::processResetInstantiationRound( Theory::Effort effort ){ - //reset triggers - for( std::map< Node, Trigger* >::iterator it = d_lte_trigger.begin(); it != d_lte_trigger.end(); ++it ){ - it->second->resetInstantiationRound(); - it->second->reset( Node::null() ); - } -} - -int InstStrategyLocalTheoryExt::process( Node f, Theory::Effort effort, int e ) { - if( e<3 ){ - return STATUS_UNFINISHED; - }else if( e==3 ){ - if( isLocalTheoryExt( f ) ){ - std::map< Node, Trigger* >::iterator it = d_lte_trigger.find( f ); - if( it!=d_lte_trigger.end() ){ - Trigger * tr = it->second; - //process the trigger - Trace("process-trigger") << " LTE process "; - tr->debugPrint("process-trigger"); - Trace("process-trigger") << "..." << std::endl; - InstMatch baseMatch( f ); - int numInst = tr->addInstantiations( baseMatch ); - Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; - d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_lte += numInst; - } - } - } - return STATUS_UNKNOWN; -} - +/* TODO? bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) { std::map< Node, bool >::iterator itq = d_quant.find( f ); if( itq==d_quant.end() ){ @@ -483,6 +455,7 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) { return itq->second; } } +*/ void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index f630a0830..02ddd233e 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -105,26 +105,6 @@ public: void addUserNoPattern( Node f, Node pat ); };/* class InstStrategyAutoGenTriggers */ - -class InstStrategyLocalTheoryExt : public InstStrategy { -private: - /** have we registered quantifier, value is whether it is an LTE term */ - std::map< Node, bool > d_quant; - /** triggers for each quantifier */ - std::map< Node, inst::Trigger* > d_lte_trigger; -private: - /** process functions */ - void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e ); -public: - InstStrategyLocalTheoryExt( QuantifiersEngine* qe ) : InstStrategy( qe ){} - /** identify */ - std::string identify() const { return std::string("LocalTheoryExt"); } - /** is local theory quantifier? */ - bool isLocalTheoryExt( Node f ); -}; - - class InstStrategyFreeVariable : public InstStrategy{ private: /** guessed instantiations */ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index e867aae1e..4fbf298f4 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -31,14 +31,13 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) : -QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){ +QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){ } InstantiationEngine::~InstantiationEngine() { delete d_i_ag; delete d_isup; - delete d_i_lte; delete d_i_fs; delete d_i_splx; delete d_i_cegqi; @@ -59,12 +58,6 @@ void InstantiationEngine::finishInit(){ d_instStrategies.push_back( d_i_ag ); } - //local theory extensions TODO? - //if( options::localTheoryExt() ){ - // d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine ); - // d_instStrategies.push_back( d_i_lte ); - //} - //full saturation : instantiate from relevant domain, then arbitrary terms if( options::fullSaturateQuant() ){ d_i_fs = new InstStrategyFreeVariable( d_quantEngine ); diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index dc5b976f0..5d46a9815 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -26,7 +26,6 @@ namespace quantifiers { class InstStrategyUserPatterns; class InstStrategyAutoGenTriggers; -class InstStrategyLocalTheoryExt; class InstStrategyFreeVariable; class InstStrategySimplex; class InstStrategyCegqi; @@ -63,8 +62,6 @@ private: InstStrategyUserPatterns* d_isup; /** auto gen triggers; only kept for destructor cleanup */ InstStrategyAutoGenTriggers* d_i_ag; - /** local theory extensions */ - InstStrategyLocalTheoryExt * d_i_lte; /** full saturate */ InstStrategyFreeVariable * d_i_fs; /** simplex (cbqi) */ diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index d0bed023d..47cb62715 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -103,6 +103,8 @@ typedef enum { USER_PAT_MODE_RESORT, /** ignore user patterns */ USER_PAT_MODE_IGNORE, + /** interleave use/resort for user patterns */ + USER_PAT_MODE_INTERLEAVE, } UserPatMode; typedef enum { diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index f492eb094..9fb5dd69d 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -148,6 +148,9 @@ resort \n\ ignore \n\ + Ignore user-provided patterns. \n\ \n\ +interleave \n\ ++ Alternate between use/resort. \n\ +\n\ "; static const std::string triggerSelModeHelp = "\ Trigger selection modes currently supported by the --trigger-sel option:\n\ @@ -336,6 +339,8 @@ inline UserPatMode stringToUserPatMode(std::string option, std::string optarg, S return USER_PAT_MODE_RESORT; } else if(optarg == "ignore") { return USER_PAT_MODE_IGNORE; + } else if(optarg == "interleave") { + return USER_PAT_MODE_INTERLEAVE; } else if(optarg == "help") { puts(userPatModeHelp.c_str()); exit(1); |