From 433401b05664d9c8827b19455ef7b93fd27efd9d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 9 Sep 2014 00:51:34 +0200 Subject: [PATCH] Accept user-provided triggers with variable terms. Flush lemmas before quantifiers check. Minor fix for conjecture generation. --- .../quantifiers/conjecture_generator.cpp | 3 +- .../quantifiers/inst_strategy_e_matching.cpp | 29 ++++++++++--------- src/theory/quantifiers/trigger.cpp | 11 +------ src/theory/quantifiers/trigger.h | 1 - src/theory/quantifiers_engine.cpp | 7 +++++ 5 files changed, 26 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 ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a00592e8b..4c29c8f9a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -195,6 +195,13 @@ void QuantifiersEngine::check( Theory::Effort e ){ //reset relevant information d_conflict = false; d_hasAddedLemma = false; + + //flush previous lemmas (for instance, if was interupted) + flushLemmas(); + if( d_hasAddedLemma ){ + return; + } + d_term_db->reset( e ); d_eq_query->reset(); if( d_rel_dom ){ -- 2.30.2