From: ajreynol Date: Mon, 22 Jun 2015 13:27:44 +0000 (+0200) Subject: Add --user-pat=interleave. Remove unused lte inst strategy. X-Git-Tag: cvc5-1.0.0~6269 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bfb9c562ac509a0c7b00e53c17aab5cda83129ac;p=cvc5.git Add --user-pat=interleave. Remove unused lte inst strategy. --- 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 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; igetPhaseReqTerms( 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::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); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a2d68f7c9..e654a689d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -893,6 +893,14 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { return performCheck; } +quantifiers::UserPatMode QuantifiersEngine::getInstUserPatMode() { + if( options::userPatternsQuant()==quantifiers::USER_PAT_MODE_INTERLEAVE ){ + return d_ierCounter%2==0 ? quantifiers::USER_PAT_MODE_USE : quantifiers::USER_PAT_MODE_RESORT; + }else{ + return options::userPatternsQuant(); + } +} + void QuantifiersEngine::flushLemmas(){ if( !d_lemmas_waiting.empty() ){ //take default output channel if none is provided diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index e613ef284..d5887f907 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -21,6 +21,7 @@ #include "util/hash.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/modes.h" #include "expr/attribute.h" #include "util/statistics_registry.h" @@ -284,6 +285,8 @@ public: int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); } /** get needs check */ bool getInstWhenNeedsCheck( Theory::Effort e ); + /** get user pat mode */ + quantifiers::UserPatMode getInstUserPatMode(); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, uint64_t level ); public: