From 8fdc49e1bc53fb99050c3c46b9a8ba8541cf851b Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 31 May 2017 11:11:02 -0500 Subject: [PATCH] Minor change to defaults, update smt comp script, minor changes to options in regressions. --- contrib/run-script-smtcomp2017 | 25 ++++++++++--------- src/smt/smt_engine.cpp | 13 +++++++--- .../regress0/bv/bv-int-collapse2-sat.smt2 | 2 +- test/regress/regress0/bv/cmu-rdk-3.smt2 | 2 ++ .../fmf/fmf-fun-no-elim-ext-arith.smt2 | 2 +- .../fmf/fmf-fun-no-elim-ext-arith2.smt2 | 2 +- test/regress/regress0/quantifiers/Makefile.am | 3 ++- .../regress0/quantifiers/RND-small.smt2 | 2 +- .../regress0/quantifiers/anti-sk-simp.smt2 | 2 +- test/regress/regress0/quantifiers/ari056.smt2 | 2 ++ .../quantifiers/cbqi-lia-dt-simp.smt2 | 2 +- .../quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 | 19 ++++++++++++++ .../regress0/quantifiers/delta-simp.smt2 | 4 ++- .../regress0/quantifiers/mix-coeff.smt2 | 4 +-- .../quantifiers/mix-complete-strat.smt2 | 2 +- .../regress0/quantifiers/mix-simp.smt2 | 4 ++- .../regress0/quantifiers/psyco-196.smt2 | 2 ++ .../regress0/quantifiers/pure_dt_cbqi.smt2 | 2 ++ test/regress/regress1/bug519.smt2 | 2 +- 19 files changed, 67 insertions(+), 29 deletions(-) create mode 100644 test/regress/regress0/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 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 -- 2.30.2