Add mbqi interleave option, change option fs-inst to fs-interleave.

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 2cbf158732e813ff5704325c6db97714927a83c9..c94360671d0c8a347216c2d2d2f9aceb6dde1688 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -128,7 +128,7 @@ option fullSaturateQuant --full-saturate-quant bool :default false :read-write
  when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
 option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
  whether to use relevant domain first for full saturation instantiation strategy
-option fullSaturateInst --fs-inst bool :default false
+option fullSaturateInterleave --fs-interleave bool :default false
  interleave full saturate instantiation with other techniques
 
 option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_USE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode
@@ -154,6 +154,8 @@ option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default fa
  only add one instantiation per quantifier per round for mbqi
 option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
  only add instantiations for one quantifier per round for mbqi
+option mbqiInterleave --mbqi-interleave bool :default false
+ interleave model-based quantifier instantiation with other techniques
 
 option fmfInstEngine --fmf-inst-engine bool :default false :read-write
  use instantiation engine in conjunction with finite model finding

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index b4821cfd6159ebe7786fe3aa02ad61b4e49f66a5..096e0933dfc1ef0a60f32b5b0b8242f66fce7dea 100644 (file)
--- 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 c431871635fd271b788404732a2ce195fd94a0f1..24c2d12543f2bf0771b22425c8c2c2dacb41abbc 100644 (file)
--- 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 fa1394f3976212f3eac992b7d3f3fd9095c0e78a..fd831001f1937d896b556d773036a41cf5352533 100644 (file)
--- 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;