diff options
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
-rwxr-xr-x | src/theory/quantifiers/model_engine.cpp | 53 |
1 files changed, 24 insertions, 29 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 7658f2b6b..9c09371c4 100755 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -73,7 +73,6 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ Trace("model-engine") << "---Model Engine Round---" << std::endl; clSet = double(clock())/double(CLOCKS_PER_SEC); } - ++(d_statistics.d_inst_rounds); Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; //let the strong solver verify that the model is minimal @@ -99,7 +98,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ } if( addedLemmas==0 ){ - Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl; + Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check || !d_incomplete_quants.empty() ) << std::endl; //CVC4 will answer SAT or unknown if( Trace.isOn("fmf-consistent") ){ Trace("fmf-consistent") << std::endl; @@ -113,6 +112,10 @@ bool ModelEngine::checkComplete() { return !d_incomplete_check; } +bool ModelEngine::checkCompleteFor( Node q ) { + return std::find( d_incomplete_quants.begin(), d_incomplete_quants.end(), q )==d_incomplete_quants.end(); +} + void ModelEngine::registerQuantifier( Node f ){ if( Trace.isOn("fmf-warn") ){ bool canHandle = true; @@ -195,17 +198,18 @@ int ModelEngine::checkModel(){ // FMC uses two sub-effort levels int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); for( int e=0; e<e_max; e++) { + d_incomplete_quants.clear(); for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i, true ); - Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; + Node q = fm->getAssertedQuantifier( i, true ); + Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl; //determine if we should check this quantifier - if( considerQuantifiedFormula( f ) ){ - exhaustiveInstantiate( f, e ); + if( considerQuantifiedFormula( q ) ){ + exhaustiveInstantiate( q, e ); if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){ break; } }else{ - Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; + Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl; } } if( d_addedLemmas>0 ){ @@ -260,13 +264,17 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); mb->d_triedLemmas = 0; mb->d_addedLemmas = 0; - mb->d_incomplete_check = false; - if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){ - Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl; + int retEi = mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ); + if( retEi!=0 ){ + if( retEi<0 ){ + Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl; + d_incomplete_quants.push_back( f ); + }else{ + Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl; + } d_triedLemmas += mb->d_triedLemmas; d_addedLemmas += mb->d_addedLemmas; - d_incomplete_check = d_incomplete_check || mb->d_incomplete_check; - d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas; + d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->d_addedLemmas; }else{ if( Trace.isOn("fmf-exh-inst-debug") ){ Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; @@ -303,13 +311,15 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } d_addedLemmas += addedLemmas; d_triedLemmas += triedLemmas; - d_statistics.d_exh_inst_lemmas += addedLemmas; + d_quantEngine->d_statistics.d_instantiations_fmf_exh += addedLemmas; } }else{ Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl; } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round - d_incomplete_check = d_incomplete_check || riter.isIncomplete(); + if( riter.isIncomplete() ){ + d_incomplete_quants.push_back( f ); + } } } @@ -328,18 +338,3 @@ void ModelEngine::debugPrint( const char* c ){ //d_quantEngine->getModel()->debugPrint( c ); } -ModelEngine::Statistics::Statistics(): - d_inst_rounds("ModelEngine::Inst_Rounds", 0), - d_exh_inst_lemmas("ModelEngine::Instantiations_Exhaustive", 0 ), - d_mbqi_inst_lemmas("ModelEngine::Instantiations_Mbqi", 0 ) -{ - smtStatisticsRegistry()->registerStat(&d_inst_rounds); - smtStatisticsRegistry()->registerStat(&d_exh_inst_lemmas); - smtStatisticsRegistry()->registerStat(&d_mbqi_inst_lemmas); -} - -ModelEngine::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_inst_rounds); - smtStatisticsRegistry()->unregisterStat(&d_exh_inst_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_mbqi_inst_lemmas); -} |