diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-08-17 11:53:11 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-08-17 11:53:11 +0200 |
commit | 7766f0ba088ad6d6c58ea9678477b255c9e52fee (patch) | |
tree | e8f1374804ab2df1f67c48793993eb65d68a6496 /src/theory | |
parent | 6432a16bd86c7540dad4ce5321ee68b7a7287c66 (diff) |
Add mbqi interleave option, change option fs-inst to fs-interleave.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 15 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 |
3 files changed, 17 insertions, 6 deletions
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index b4821cfd6..096e0933d 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -603,7 +603,7 @@ FullSaturation::FullSaturation( QuantifiersEngine* qe ) : QuantifiersModule( qe } bool FullSaturation::needsCheck( Theory::Effort e ){ - if( options::fullSaturateInst() ){ + if( options::fullSaturateInterleave() ){ if( d_quantEngine->getInstWhenNeedsCheck( e ) ){ return true; } @@ -623,7 +623,7 @@ void FullSaturation::reset_round( Theory::Effort e ) { void FullSaturation::check( Theory::Effort e, unsigned quant_e ) { bool doCheck = false; bool fullEffort = false; - if( options::fullSaturateInst() ){ + if( options::fullSaturateInterleave() ){ //we only add when interleaved with other strategies doCheck = quant_e==QuantifiersEngine::QEFFORT_STANDARD && d_quantEngine->hasAddedLemma(); } @@ -653,7 +653,7 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) { if( Trace.isOn("fs-engine") ){ Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl; double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("fs-engine") << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl; + Trace("fs-engine") << "Finished full saturation engine, time = " << (clSet2-clSet) << std::endl; } } } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index c43187163..24c2d1254 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -53,7 +53,11 @@ bool ModelEngine::needsCheck( Theory::Effort e ) { } unsigned ModelEngine::needsModel( Theory::Effort e ) { - return QuantifiersEngine::QEFFORT_MODEL; + if( options::mbqiInterleave() ){ + return QuantifiersEngine::QEFFORT_STANDARD; + }else{ + return QuantifiersEngine::QEFFORT_MODEL; + } } void ModelEngine::reset_round( Theory::Effort e ) { @@ -61,7 +65,14 @@ void ModelEngine::reset_round( Theory::Effort e ) { } void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ - if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){ + bool doCheck = false; + if( options::mbqiInterleave() ){ + doCheck = quant_e==QuantifiersEngine::QEFFORT_STANDARD && d_quantEngine->hasAddedLemma(); + } + if( !doCheck ){ + doCheck = quant_e==QuantifiersEngine::QEFFORT_MODEL; + } + if( doCheck ){ Assert( !d_quantEngine->inConflict() ); int addedLemmas = 0; FirstOrderModel* fm = d_quantEngine->getModel(); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index fa1394f39..fd831001f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -265,7 +265,7 @@ void QuantifiersEngine::finishInit(){ d_modules.push_back( d_uee ); } //full saturation : instantiate from relevant domain, then arbitrary terms - if( options::fullSaturateQuant() || options::fullSaturateInst() ){ + if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){ d_fs = new quantifiers::FullSaturation( this ); d_modules.push_back( d_fs ); needsRelDom = true; |