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

diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017
index bb3425d91d432ec2705fb2db00e4fa1016013b9b..8a0ff92eab6c56cf31e66c4e0c26374f7f07ee58 100644 (file)
--- 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 b5fbecf7d5df7ac2378ea24de6d2593b14d0ef90..ace33a164913b0cad8b90bff2f8e512e46e5918b 100644 (file)
--- 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 1a355a4953de7d0341d94a3a727fdd1e83af57d5..4b97a3de9d6e2bc0c23a7a03557d3eecacb43efe 100644 (file)
--- 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 742dd593badfb3f9d2b081880443f18d334e97a5..9e773388963b6f3f6c02f56c4bc92b10b2a4c5ef 100644 (file)
--- 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 dd9cb68863a4dd40d97edace39cc0d001207dfdf..0618e28cb94c0a3eb8bea4527576d311c1aee031 100644 (file)
--- 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 ea5a5e4b74807bc4ad0568272e3b5e01a29a393c..07f1e66740c4966080aff0684247b2063f5c721f 100644 (file)
--- 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 faa2abe9a089f23a8b3635e2ee1e08e82c4d2925..9c31204e85e7df963c95a66bebb05d741c66f0d8 100644 (file)
--- 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 1401e5de84b258ffdda40b103e6221f2a0944c75..cf5c3bc7ed45a8e79b6c8258b72d4c3d061c0fbc 100644 (file)
--- 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 ba4f9cbb979e077aa396b8fbc99e22beb9cea72f..2ae54a075c07dcba21572b4317aaa4d3f8d36c77 100644 (file)
--- 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 ed4d2bf4a8921dffdca1bbd652b8066edbbff240..a1f4aef04ef92308648e01ed866143f3f6aa66eb 100644 (file)
--- 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 bd7ca19cd66de39413eb2d5f981fb70267040b01..b8b1683a95e2588668e8f14d4152223a1bbced6a 100644 (file)
--- 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 (file)
index 0000000..4d5cf4e
--- /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 f18a4fbd9b14732d84096875beb3f600b65095b4..e5883134f74514ab286e9328832728741dd2afda 100644 (file)
--- 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 a20867b1c298ad9e2887650fa27c3e391e15e01b..23ecba49e75355265135dc3d84eec63085a7d588 100644 (file)
--- 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 c2209f6978bdeb5f7bae927baf161b108f2764d2..e75591decfa04e1d1769bda18d878a82d112c285 100644 (file)
--- 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 0b8c5067d162912cfa4e4abb30ea2e044bc3b45d..b7142c6e9c20635c01dd1302cbd763d7fcfd4bab 100644 (file)
--- 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 356e62752229019098bfaaa5e431e642a4006cac..fef1a24c63c6bbb03b5a9102882b8a71d602a1a0 100644 (file)
--- 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 5c11a57f521cd46bfc4811b6d1a949c47d5be4f9..0ce96285c45de17b0621ab17d7f1a65f8e7d537b 100644 (file)
--- 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 72ec634a8db4c77d6c038340cab5eaac41953641..6cabbaa642deb435e1b8312cf4c9f45a1409fdda 100644 (file)
--- 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