diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-16 11:07:36 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-16 11:07:36 +0200 |
commit | 548582b252170f35a602705a109d88a608611cca (patch) | |
tree | abcfe42578de4b4a99905ed76e1df23c396820ef /src/theory/quantifiers/model_engine.cpp | |
parent | bad7f4fe4dca4c6511c2862bf81b6791640ac78f (diff) |
Add option --fmf-fun-rlv, remove deprecated option --axiom-inst.
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 83 |
1 files changed, 44 insertions, 39 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 2ad8be3a1..752e88c5a 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -52,7 +52,7 @@ bool ModelEngine::needsCheck( Theory::Effort e ) { } unsigned ModelEngine::needsModel( Theory::Effort e ) { - return QuantifiersEngine::QEFFORT_MODEL; + return QuantifiersEngine::QEFFORT_MODEL; } void ModelEngine::reset_round( Theory::Effort e ) { @@ -64,7 +64,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ int addedLemmas = 0; FirstOrderModel* fm = d_quantEngine->getModel(); - //the following will test that the model satisfies all asserted universal quantifiers by + //the following will test that the model satisfies all asserted universal quantifiers by // (model-based) exhaustive instantiation. double clSet = 0; if( Trace.isOn("model-engine") ){ @@ -88,7 +88,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ }else{ addedLemmas++; } - + if( Trace.isOn("model-engine") ){ double clSet2 = double(clock())/double(CLOCKS_PER_SEC); Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; @@ -143,8 +143,6 @@ bool ModelEngine::optOneQuantPerRound(){ int ModelEngine::checkModel(){ FirstOrderModel* fm = d_quantEngine->getModel(); - quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); - Assert( mb!=NULL ); //flatten the representatives //Trace("model-engine-debug") << "Flattening representatives...." << std::endl; @@ -192,52 +190,59 @@ int ModelEngine::checkModel(){ } Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; - //default : 1 : conj,axiom - //priority : 0 : conj, 1 : axiom - //trust : 0 : conj - int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; - for( int effort=startEffort; effort<2; effort++ ){ - // 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++) { - if (d_addedLemmas==0) { - for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - bool isAx = getTermDatabase()->isQAttrAxiom( f ); - Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; - //determine if we should check this quantifier - if( ( ( effort==1 && ( options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT || isAx ) ) || ( effort==0 && !isAx ) ) && mb->isQuantifierActive( f ) ){ - exhaustiveInstantiate( f, e ); - if( Trace.isOn("model-engine-warn") ){ - if( d_addedLemmas>10000 ){ - Debug("fmf-exit") << std::endl; - debugPrint("fmf-exit"); - exit( 0 ); - } + // 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++) { + if (d_addedLemmas==0) { + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; + //determine if we should check this quantifier + if( considerQuantifiedFormula( f ) ){ + exhaustiveInstantiate( f, e ); + if( Trace.isOn("model-engine-warn") ){ + if( d_addedLemmas>10000 ){ + Debug("fmf-exit") << std::endl; + debugPrint("fmf-exit"); + exit( 0 ); } - if( optOneQuantPerRound() && d_addedLemmas>0 ){ - break; - } - }else{ - Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; } + if( optOneQuantPerRound() && d_addedLemmas>0 ){ + break; + } + }else{ + Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; } } } - if( d_addedLemmas==0 && options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){ - //set incomplete - if( effort==0 ){ - d_incomplete_check = true; - } - break; - } } + //print debug information Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / "; Trace("model-engine") << d_totalLemmas << std::endl; return d_addedLemmas; } +bool ModelEngine::considerQuantifiedFormula( Node q ) { + if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){ //!d_quantEngine->getModel()->isQuantifierActive( q ); + return false; + }else{ + if( options::fmfFunWellDefinedRelevant() ){ + if( q[0].getNumChildren()==1 ){ + TypeNode tn = q[0][0].getType(); + if( tn.getAttribute(AbsTypeFunDefAttribute()) ){ + //we are allowed to assume the introduced type is empty + if( d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn )==0 ){ + Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl; + return false; + } + } + } + } + return true; + } +} + void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ //first check if the builder can do the exhaustive instantiation quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); |