Add options related to interleaving quantifiers and theory combination, changes default behavior.

3 files changed, 33 insertions, 30 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 1363626c6..d001684a0 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -99,8 +99,12 @@ option incrementTriggers --increment-triggers bool :default true
  
 option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "options/quantifiers_modes.h" :handler stringToInstWhenMode :predicate checkInstWhenMode
  when to apply instantiation
-option instWhenDelayIncrement --inst-when-delay-increment bool :default false
- delay incrementing counters for inst-when mode to ensure theory combination and standard quantifier effort strategies take turns
+option instWhenStrictInterleave --inst-when-strict-interleave bool :default true :read-write
+ ensure theory combination and standard quantifier effort strategies take turns 
+option instWhenPhase --inst-when-phase=N int :read-write :default 2 :read-write
+ instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen
+option instWhenTcFirst --inst-when-tc-first bool :default true :read-write
+ allow theory combination to happen once initially, before quantifier strategies are run
  
 option instMaxLevel --inst-max-level=N int :read-write :default -1
  maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 93623408e..0a2f50a78 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1683,16 +1683,25 @@ void SmtEngine::setDefaults() {
     options::sortInference.set( false );
     options::ufssFairnessMonotone.set( false );
   }
+  if( d_logic.hasCardinalityConstraints() ){
+    //must have finite model finding on
+    options::finiteModelFind.set( true );
+  }
+  
+  //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved
+  if( d_logic.isTheoryEnabled(THEORY_STRINGS) || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) ){
+    if( !options::instWhenStrictInterleave.wasSetByUser() ){
+      options::instWhenStrictInterleave.set( false );
+    }
+  }
+  
   //local theory extensions
   if( options::localTheoryExt() ){
     if( !options::instMaxLevel.wasSetByUser() ){
       options::instMaxLevel.set( 0 );
     }
   }
-  if( d_logic.hasCardinalityConstraints() ){
-    //must have finite model finding on
-    options::finiteModelFind.set( true );
-  }
+
   if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) {
     options::fmfBoundInt.set( true );
   }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 5d19d603c..568483380 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -138,12 +138,11 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   d_builder = NULL;
 
   d_total_inst_count_debug = 0;
-  //allow theory combination to go first, once initially, when instWhenDelayIncrement = true
-  d_ierCounter = options::instWhenDelayIncrement() ? 1 : 0;
-  d_ierCounter_lc = options::instWhenDelayIncrement() ? 1 : 0;
-  d_ierCounterLastLc = -1;
-  //if any strategy called only on last call, use phase 3
-  d_inst_when_phase = options::cbqi() ? 3 : 2;
+  //allow theory combination to go first, once initially
+  d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
+  d_ierCounter_lc = 0;
+  d_ierCounterLastLc = d_ierCounter_lc;
+  d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
 }
 
 QuantifiersEngine::~QuantifiersEngine(){
@@ -340,13 +339,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
     Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
     return;
   }
-  if( !options::instWhenDelayIncrement() ){
-    if( e==Theory::EFFORT_FULL ){
-      d_ierCounter++;
-    }else if( e==Theory::EFFORT_LAST_CALL ){
-      d_ierCounter_lc++;
-    }
-  }
   bool needsCheck = !d_lemmas_waiting.empty();
   unsigned needsModelE = QEFFORT_NONE;
   std::vector< QuantifiersModule* > qm;
@@ -470,16 +462,14 @@ void QuantifiersEngine::check( Theory::Effort e ){
         break;
       }else{
         if( quant_e==QEFFORT_CONFLICT ){
-          if( options::instWhenDelayIncrement() ){
-            if( e==Theory::EFFORT_FULL ){
-              //increment if a last call happened, or if we already were in phase
-              if( d_ierCounterLastLc!=d_ierCounter_lc || d_ierCounter%d_inst_when_phase==0 ){
-                d_ierCounter++;
-                d_ierCounterLastLc = d_ierCounter_lc;
-              }
-            }else if( e==Theory::EFFORT_LAST_CALL ){
-              d_ierCounter_lc++;
+          if( e==Theory::EFFORT_FULL ){
+            //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
+            if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){
+              d_ierCounter++;
+              d_ierCounterLastLc = d_ierCounter_lc;
             }
+          }else if( e==Theory::EFFORT_LAST_CALL ){
+            d_ierCounter_lc++;
           }
         }else if( quant_e==QEFFORT_MODEL ){
           if( e==Theory::EFFORT_LAST_CALL ){
@@ -1052,9 +1042,9 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){
     performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){
-    performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase==0 ) || e==Theory::EFFORT_LAST_CALL );
+    performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL ){
-    performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase==0 ) || e==Theory::EFFORT_LAST_CALL );
+    performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
   }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){
     performCheck = ( e >= Theory::EFFORT_LAST_CALL );
   }else{