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

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 1363626c694f267e8e81edda3f41f020ed4ebc53..d001684a0af66e91ce3cb63acc169f1e457c6f76 100644 (file)
--- 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 93623408ecb0d8f6a701f7410657fa14cc1b0469..0a2f50a78ff4715bdb3464c9cab7eaafd38045ea 100644 (file)
--- 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 5d19d603c62ed9810407b0ef0b27d55b92186e8f..568483380a91acf0a010e8b45eef8399a2ff4b8c 100644 (file)
--- 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{

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 6e7b2528620b0bab85ff1411373e0c64c04029fb..e8000eff14d3893a797efcc54b5a7210c841a13b 100644 (file)
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -38,10 +38,9 @@ TESTS =      \
        gauss_init_0030.fof.smt2 \
        qcft-javafe.filespace.TreeWalker.006.smt2 \
        qcft-smtlib3dbc51.smt2 \
-       symmetric_unsat_7.smt2 \
        javafe.ast.StmtVec.009.smt2 \
        ARI176e1.smt2 \
-  bi-artm-s.smt2 \
+       bi-artm-s.smt2 \
        simp-typ-test.smt2 \
        macros-int-real.smt2 \
        stream-x2014-09-18-unsat.smt2 \
@@ -65,18 +64,18 @@ TESTS =     \
        ext-ex-deq-trigger.smt2 \
        matching-lia-1arg.smt2 \
        RND_4_16.smt2 \
-  cdt-0208-to.smt2 \
-  psyco-196.smt2 \
-  agg-rew-test.smt2 \
-  agg-rew-test-cf.smt2 \
-  rew-to-0211-dd.smt2 \
-  rew-to-scala.smt2 \
-  macro-subtype-param.smt2 \
-  macros-real-arg.smt2 \
-  subtype-param-unk.smt2 \
-  subtype-param.smt2 \
-  anti-sk-simp.smt2 \
-  pure_dt_cbqi.smt2
+       cdt-0208-to.smt2 \
+       psyco-196.smt2 \
+       agg-rew-test.smt2 \
+       agg-rew-test-cf.smt2 \
+       rew-to-0211-dd.smt2 \
+       rew-to-scala.smt2 \
+       macro-subtype-param.smt2 \
+       macros-real-arg.smt2 \
+       subtype-param-unk.smt2 \
+       subtype-param.smt2 \
+       anti-sk-simp.smt2 \
+       pure_dt_cbqi.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine