From 7766f0ba088ad6d6c58ea9678477b255c9e52fee Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 17 Aug 2017 11:53:11 +0200
Subject: [PATCH] Add mbqi interleave option, change option fs-inst to
 fs-interleave.

---
 src/options/quantifiers_options                   |  4 +++-
 .../quantifiers/inst_strategy_e_matching.cpp      |  6 +++---
 src/theory/quantifiers/model_engine.cpp           | 15 +++++++++++++--
 src/theory/quantifiers_engine.cpp                 |  2 +-
 4 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 2cbf15873..c94360671 100644
--- 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 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;
-- 
2.30.2