diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-09 00:51:34 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-09 00:51:34 +0200 |
commit | 433401b05664d9c8827b19455ef7b93fd27efd9d (patch) | |
tree | 9be15c6804521434d4116b05eb571ecd78ac2767 /src/theory/quantifiers | |
parent | fc573f3512b5345763755c9d7a061d430c46ae5f (diff) |
Accept user-provided triggers with variable terms. Flush lemmas before quantifiers check. Minor fix for conjecture generation.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 29 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 11 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.h | 1 |
4 files changed, 19 insertions, 25 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index c775bb558..0b8e0e462 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -700,7 +700,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { d_tg_alloc[0].reset( this, TypeNode::null() );
while( d_tg_alloc[0].getNextTerm( this, depth ) ){
Assert( d_tg_alloc[0].getGeneralizationDepth( this )==d_tg_gdepth );
- if( d_tg_alloc[0].getDepth( this )==depth ){
+ //if( d_tg_alloc[0].getDepth( this )==depth ){
+ if( (int)d_tg_gdepth==d_tg_gdepth_limit ){
//construct term
Node nn = d_tg_alloc[0].getTerm( this );
if( getUniversalRepresentative( nn )==nn ){
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index df7f06aff..ef1997d4c 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -68,12 +68,12 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ for( int i=0; i<(int)d_user_gen[f].size(); i++ ){ bool processTrigger = true; if( processTrigger ){ - //if( d_user_gen[f][i]->isMultiTrigger() ) - Trace("process-trigger") << " Process (user) " << (*d_user_gen[f][i]) << "..." << std::endl; + 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 ); - //if( d_user_gen[f][i]->isMultiTrigger() ) - Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; + 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; @@ -89,17 +89,22 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ //add to generators + bool usable = true; std::vector< Node > nodes; for( int i=0; i<(int)pat.getNumChildren(); i++ ){ nodes.push_back( pat[i] ); + if( pat[i].getKind()!=INST_CONSTANT && !Trigger::isUsableTrigger( pat[i], f ) ){ + Trace("trigger-warn") << "User-provided trigger is not usable : " << pat << " because of " << pat[i] << std::endl; + usable = false; + break; + } } - if( Trigger::isUsableTrigger( nodes, f ) ){ + if( usable ){ //extend to literal matching 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() ) ); + d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) ); } } @@ -156,14 +161,12 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) bool processTrigger = itt->second; if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){ d_processed_trigger[f][tr] = true; - //if( tr->isMultiTrigger() ) - Trace("process-trigger") << " Process "; - tr->debugPrint("process-trigger"); - Trace("process-trigger") << "..." << std::endl; + Trace("process-trigger") << " Process "; + tr->debugPrint("process-trigger"); + Trace("process-trigger") << "..." << std::endl; InstMatch baseMatch( f ); int numInst = tr->addInstantiations( baseMatch ); - //if( tr->isMultiTrigger() ) - Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; + Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){ d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst; }else{ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 4a99852d1..11ec0210d 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -210,15 +210,6 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOpt return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers ); } -bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ - for( int i=0; i<(int)nodes.size(); i++ ){ - if( !isUsableTrigger( nodes[i], f ) ){ - return false; - } - } - return true; -} - bool Trigger::isUsable( Node n, Node f ){ if( quantifiers::TermDb::getInstConstAttr(n)==f ){ if( isAtomicTrigger( n ) ){ @@ -234,7 +225,7 @@ bool Trigger::isUsable( Node n, Node f ){ std::map< Node, Node > coeffs; if( isBooleanTermTrigger( n ) ){ return true; - } + } } return false; }else{ diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 1a3ae3fcd..74a87591f 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -105,7 +105,6 @@ public: static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst = false ); public: /** is usable trigger */ - static bool isUsableTrigger( std::vector< Node >& nodes, Node f ); static bool isUsableTrigger( Node n, Node f ); static bool isAtomicTrigger( Node n ); static bool isAtomicTriggerKind( Kind k ); |