diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-28 16:27:19 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-28 16:27:27 +0100 |
commit | 68f22235a62f5276b206e9a6692a85001beb8d42 (patch) | |
tree | f9700ab9aaacf866121c7e4f947dffd20710f628 /src/theory/quantifiers | |
parent | 388a6acf4acd50a7611faae91b3489ac2209e584 (diff) |
Synchronize conjecture generation with E-matching. Minor fix to --full-saturate-quant.
Diffstat (limited to 'src/theory/quantifiers')
-rwxr-xr-x | src/theory/quantifiers/conjecture_generator.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 30 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 2 |
4 files changed, 13 insertions, 36 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( nv<maxs[index] && nv<=max_i && r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){ - childIndex[index]++; - nv = childIndex[index]+1; + nv++; } } if( nv<maxs[index] && nv<=max_i ){ - childIndex[index]++; + childIndex[index] = nv; index++; }else{ childIndex.pop_back(); @@ -545,8 +544,11 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ } success = index>=0; if( success ){ - Trace("inst-alg-rd") << "Try instantiation..." << std::endl; - index--; + Trace("inst-alg-rd") << "Try instantiation { "; + for( unsigned j=0; j<childIndex.size(); j++ ){ + Trace("inst-alg-rd") << childIndex[j] << " "; + } + Trace("inst-alg-rd") << "}" << std::endl; //try instantiation std::vector< Node > terms; for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ @@ -560,6 +562,8 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ Trace("inst-alg-rd") << "Success!" << std::endl; ++(d_quantEngine->getInstantiationEngine()->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 */ |