From 68f22235a62f5276b206e9a6692a85001beb8d42 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 28 Nov 2014 16:27:19 +0100 Subject: [PATCH] Synchronize conjecture generation with E-matching. Minor fix to --full-saturate-quant. --- .../quantifiers/conjecture_generator.cpp | 3 +- .../quantifiers/inst_strategy_e_matching.cpp | 14 +++++--- .../quantifiers/instantiation_engine.cpp | 30 ++--------------- src/theory/quantifiers/instantiation_engine.h | 2 -- src/theory/quantifiers_engine.cpp | 32 ++++++++++++++++++- src/theory/quantifiers_engine.h | 5 +++ 6 files changed, 49 insertions(+), 37 deletions(-) diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 06552196d..2f8822b53 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -352,7 +352,8 @@ bool ConjectureGenerator::isGroundTerm( TNode n ) { } bool ConjectureGenerator::needsCheck( Theory::Effort e ) { - return e==Theory::EFFORT_FULL; + // synchonized with instantiation engine + return d_quantEngine->getInstWhenNeedsCheck( e ); } bool ConjectureGenerator::hasEnumeratedUf( Node n ) { diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 8918a6dac..b9e8aef09 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -530,12 +530,11 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ //skip inst constant nodes while( nvgetTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){ - childIndex[index]++; - nv = childIndex[index]+1; + nv++; } } if( nv=0; if( success ){ - Trace("inst-alg-rd") << "Try instantiation..." << std::endl; - index--; + Trace("inst-alg-rd") << "Try instantiation { "; + for( unsigned j=0; j terms; for( unsigned i=0; igetInstantiationEngine()->d_statistics.d_instantiations_guess); return STATUS_UNKNOWN; + }else{ + index--; } } }while( success ); diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index ade6d4313..b53919aaf 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -31,7 +31,7 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) : -QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){ +QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ){ } @@ -178,37 +178,11 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } bool InstantiationEngine::needsCheck( Theory::Effort e ){ - if( e==Theory::EFFORT_FULL ){ - d_ierCounter++; - } - //determine if we should perform check, based on instWhenMode - bool performCheck = false; - if( options::instWhenMode()==INST_WHEN_FULL ){ - performCheck = ( e >= Theory::EFFORT_FULL ); - }else if( options::instWhenMode()==INST_WHEN_FULL_DELAY ){ - performCheck = ( e >= Theory::EFFORT_FULL ) && !d_quantEngine->getTheoryEngine()->needCheck(); - }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){ - performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); - }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){ - performCheck = ( e >= Theory::EFFORT_LAST_CALL ); - }else{ - performCheck = true; - } - static int ierCounter2 = 0; - if( e==Theory::EFFORT_LAST_CALL ){ - ierCounter2++; - //with bounded integers, skip every other last call, - // since matching loops may occur with infinite quantification - if( ierCounter2%2==0 && options::fmfBoundInt() ){ - performCheck = false; - } - } - return performCheck; + return d_quantEngine->getInstWhenNeedsCheck( e ); } void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ - Debug("inst-engine") << "IE: Check " << e << " " << d_ierCounter << std::endl; double clSet = 0; if( Trace.isOn("inst-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 2fa37ac35..2d427ae0a 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -84,8 +84,6 @@ private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; /** whether the instantiation engine should set incomplete if it cannot answer SAT */ bool d_setIncomplete; - /** inst round counter */ - int d_ierCounter; /** whether each quantifier is active */ std::map< Node, bool > d_quant_active; /** whether we have added cbqi lemma */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4dc8df09d..d6c6f4667 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -171,8 +171,9 @@ d_lemmas_produced_c(u){ d_builder = NULL; } - //options d_total_inst_count_debug = 0; + d_ierCounter = 0; + d_ierCounter_lc = 0; } QuantifiersEngine::~QuantifiersEngine(){ @@ -251,6 +252,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl; return; } + if( e==Theory::EFFORT_FULL ){ + d_ierCounter++; + }else if( e==Theory::EFFORT_LAST_CALL ){ + d_ierCounter_lc++; + } bool needsCheck = false; bool needsModel = false; bool needsFullModel = false; @@ -825,6 +831,30 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool return addSplit( fm ); } +bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { + //determine if we should perform check, based on instWhenMode + bool performCheck = false; + if( options::instWhenMode()==quantifiers::INST_WHEN_FULL ){ + performCheck = ( e >= Theory::EFFORT_FULL ); + }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){ + performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck(); + }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){ + performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); + }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){ + performCheck = ( e >= Theory::EFFORT_LAST_CALL ); + }else{ + performCheck = true; + } + if( e==Theory::EFFORT_LAST_CALL ){ + //with bounded integers, skip every other last call, + // since matching loops may occur with infinite quantification + if( d_ierCounter_lc%2==0 && options::fmfBoundInt() ){ + performCheck = false; + } + } + return performCheck; +} + 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 2b466b96b..ac782a536 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -169,6 +169,9 @@ private: std::map< Node, int > d_total_inst_debug; std::map< Node, int > d_temp_inst_debug; int d_total_inst_count_debug; + /** inst round counters */ + int d_ierCounter; + int d_ierCounter_lc; private: KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time"); public: @@ -273,6 +276,8 @@ public: bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } /** get number of waiting lemmas */ int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); } + /** get needs check */ + bool getInstWhenNeedsCheck( Theory::Effort e ); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, uint64_t level ); /** is term eligble for instantiation? */ -- 2.30.2