Minor change to defaults, update smt comp script, minor changes to options in regressions.

19 files changed, 67 insertions, 29 deletions

diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017
index bb3425d91..8a0ff92ea 100644
--- a/contrib/run-script-smtcomp2017
+++ b/contrib/run-script-smtcomp2017
@@ -81,22 +81,23 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA)
   # finish 9min
   finishwith --full-saturate-quant
   ;;
-UFBV)
+BV|UFBV)
   # many problems in UFBV are essentially BV
-  trywith 300 --full-saturate-quant 
-  trywith 300 --finite-model-find
-  finishwith --cbqi-all --full-saturate-quant
+  trywith 30 --full-saturate-quant
+  trywith 30 --finite-model-find
+  finishwith --full-saturate-quant --decision=internal
   ;;
-BV)
-  trywith 300 --finite-model-find
-  finishwith --cbqi-all --full-saturate-quant
+LIA|LRA)
+  trywith 30 --full-saturate-quant
+  trywith 300 --full-saturate-quant --cbqi-midpoint
+  trywith 300 --full-saturate-quant --cbqi-nested-qe
+  finishwith  --full-saturate-quant --cbqi-nested-qe --decision=internal
   ;;
-LIA|LRA|NIA|NRA)
+NIA|NRA)
   trywith 30 --full-saturate-quant
-  trywith 300 --full-saturate-quant --cbqi-min-bounds
-  trywith 300 --full-saturate-quant --decision=internal
-  trywith 1800  --full-saturate-quant --cbqi-nested-qe
-  finishwith --full-saturate-quant --cbqi-midpoint
+  trywith 300 --full-saturate-quant --nl-ext
+  trywith 300 --full-saturate-quant --cbqi-nested-qe
+  finishwith  --full-saturate-quant --cbqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)
   trywith 600
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b5fbecf7d..ace33a164 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1852,8 +1852,10 @@ void SmtEngine::setDefaults() {
   }
   //counterexample-guided instantiation for non-sygus
   // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
-  if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) ||
-      options::cbqiAll() ){
+  if( d_logic.isQuantified() && 
+      ( ( options::decisionMode()!=decision::DECISION_STRATEGY_INTERNAL &&
+          ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) ||
+        options::cbqiAll() ) ){
     if( !options::cbqi.wasSetByUser() ){
       options::cbqi.set( true );
     }
@@ -1889,11 +1891,14 @@ void SmtEngine::setDefaults() {
   if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
     options::quantConflictFind.set( true );
   }
-  if( options::cbqiNestedQE() ){
-    //only sound with prenex = disj_normal or normal
+  if( options::cbqi() && 
+      ( options::cbqiNestedQE() || options::decisionMode()==decision::DECISION_STRATEGY_INTERNAL ) ){
+    //only complete with prenex = disj_normal or normal
     if( options::prenexQuant()<=quantifiers::PRENEX_QUANT_DISJ_NORMAL ){
       options::prenexQuant.set( quantifiers::PRENEX_QUANT_DISJ_NORMAL );
     }
+  }
+  if( options::cbqiNestedQE() ){
     options::prenexQuantUser.set( true );
     if( !options::preSkolemQuant.wasSetByUser() ){
       options::preSkolemQuant.set( true );
diff --git a/test/regress/regress0/bv/bv-int-collapse2-sat.smt2 b/test/regress/regress0/bv/bv-int-collapse2-sat.smt2
index 1a355a495..4b97a3de9 100644
--- a/test/regress/regress0/bv/bv-int-collapse2-sat.smt2
+++ b/test/regress/regress0/bv/bv-int-collapse2-sat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --rewrite-divk --no-check-proofs --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/bv/cmu-rdk-3.smt2 b/test/regress/regress0/bv/cmu-rdk-3.smt2
index 742dd593b..9e7733889 100644
--- a/test/regress/regress0/bv/cmu-rdk-3.smt2
+++ b/test/regress/regress0/bv/cmu-rdk-3.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --rewrite-divk
+; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 
diff --git a/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2 b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2
index dd9cb6886..0618e28cb 100644
--- a/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2
+++ b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun --no-check-models --rewrite-divk
 ; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)
diff --git a/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2 b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2
index ea5a5e4b7..07f1e6674 100644
--- a/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2
+++ b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun --no-check-models --rewrite-divk
 ; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index faa2abe9a..9c31204e8 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -88,7 +88,8 @@ TESTS =	\
 	quaternion_ds1_symm_0428.fof.smt2 \
 	bug749-rounding.smt2 \
 	RNDPRE_4_1-dd-nqe.smt2 \
-	mix-complete-strat.smt2
+	mix-complete-strat.smt2 \
+	cbqi-sdlx-fixpoint-3-dd.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/RND-small.smt2 b/test/regress/regress0/quantifiers/RND-small.smt2
index 1401e5de8..cf5c3bc7e 100644
--- a/test/regress/regress0/quantifiers/RND-small.smt2
+++ b/test/regress/regress0/quantifiers/RND-small.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-recurse
+; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic LRA)
 (declare-fun y1 () Real)
diff --git a/test/regress/regress0/quantifiers/anti-sk-simp.smt2 b/test/regress/regress0/quantifiers/anti-sk-simp.smt2
index ba4f9cbb9..2ae54a075 100644
--- a/test/regress/regress0/quantifiers/anti-sk-simp.smt2
+++ b/test/regress/regress0/quantifiers/anti-sk-simp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --quant-anti-skolem
+; COMMAND-LINE: --cbqi --quant-anti-skolem
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
diff --git a/test/regress/regress0/quantifiers/ari056.smt2 b/test/regress/regress0/quantifiers/ari056.smt2
index ed4d2bf4a..a1f4aef04 100644
--- a/test/regress/regress0/quantifiers/ari056.smt2
+++ b/test/regress/regress0/quantifiers/ari056.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --cbqi
+; EXPECT: unsat
 (set-logic UFNIRA)
 (set-info :status unsat)
 (assert (forall ((X Int)) (= X 12) ))
diff --git a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2
index bd7ca19cd..b8b1683a9 100644
--- a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2
+++ b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --dt-rewrite-error-sel
+; COMMAND-LINE: --cbqi --dt-rewrite-error-sel
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
diff --git a/test/regress/regress0/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 b/test/regress/regress0/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
new file mode 100644
index 000000000..4d5cf4ec4
--- /dev/null
+++ b/test/regress/regress0/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --cbqi --decision=internal
+; EXPECT: unsat
+(set-logic LIA)
+(set-info :status unsat)
+
+(assert (or 
+(forall ((H Int) (G Int)) (= (= G 0) (= H 0)))
+
+(forall ((C Int) (D Int) (E Int)) (or 
+(= (= D 0) (= C 0)) 
+(and 
+(not (forall ((G Int)) (= (= E 0) (= G 0)))) 
+(not (forall ((A Int)) 
+  (not (= (ite (= A 0) 0 1) (ite (= C 0) 0 2)))
+))
+)))
+))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/delta-simp.smt2 b/test/regress/regress0/quantifiers/delta-simp.smt2
index f18a4fbd9..e5883134f 100644
--- a/test/regress/regress0/quantifiers/delta-simp.smt2
+++ b/test/regress/regress0/quantifiers/delta-simp.smt2
@@ -1,5 +1,7 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
 (set-logic LRA)
 (set-info :status sat)
 (declare-fun c () Real)
 (assert (forall ((x Real)) (or (<= x 0) (>= x (+ c 3)))))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/mix-coeff.smt2 b/test/regress/regress0/quantifiers/mix-coeff.smt2
index a20867b1c..23ecba49e 100644
--- a/test/regress/regress0/quantifiers/mix-coeff.smt2
+++ b/test/regress/regress0/quantifiers/mix-coeff.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic LIRA)
 (set-info :status unsat)
 (assert (forall ((x Int) (y Int) (a Real) (z Int)) (or (> x (+ a (* (/ 2 3) y) (* (/ 4 5) z))) (< x (+ 10 (* 3 a) (* (/ 2 5) y) (* (/ 4 7) z))))))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/mix-complete-strat.smt2 b/test/regress/regress0/quantifiers/mix-complete-strat.smt2
index c2209f697..e75591dec 100644
--- a/test/regress/regress0/quantifiers/mix-complete-strat.smt2
+++ b/test/regress/regress0/quantifiers/mix-complete-strat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --cbqi --finite-model-find --no-check-models
 ; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/mix-simp.smt2 b/test/regress/regress0/quantifiers/mix-simp.smt2
index 0b8c5067d..b7142c6e9 100644
--- a/test/regress/regress0/quantifiers/mix-simp.smt2
+++ b/test/regress/regress0/quantifiers/mix-simp.smt2
@@ -1,4 +1,6 @@
-(set-logic ALL_SUPPORTED)
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic LIRA)
 (set-info :status sat)
 (assert (forall ((x Real)) (exists ((y Int)) (and (>= y x) (< y (+ x 1))))))
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/psyco-196.smt2 b/test/regress/regress0/quantifiers/psyco-196.smt2
index 356e62752..fef1a24c6 100644
--- a/test/regress/regress0/quantifiers/psyco-196.smt2
+++ b/test/regress/regress0/quantifiers/psyco-196.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
 (set-logic LIA)
 (set-info :status sat)
 (declare-fun W_S1_V5 () Bool)
diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
index 5c11a57f5..0ce96285c 100644
--- a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
+++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --cbqi --no-check-models
+; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 (declare-datatypes () ((nat (Suc (pred nat)) (zero))))
diff --git a/test/regress/regress1/bug519.smt2 b/test/regress/regress1/bug519.smt2
index 72ec634a8..6cabbaa64 100644
--- a/test/regress/regress1/bug519.smt2
+++ b/test/regress/regress1/bug519.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -mi
+; COMMAND-LINE: --cbqi -mi --no-check-models
 ; EXPECT: sat
 ; EXPECT: unsat