diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-27 01:44:55 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-27 06:44:55 +0000 |
commit | 437405dca0e1a393a8fa1eda900bc0bc469091c6 (patch) | |
tree | 4855b19b650818337aaad35ef9c4178e3645c5c0 /test | |
parent | 028d657dc41bbb908b7b9ad6ba707dc2216b15ac (diff) |
Enable new justification heuristic by default (#6613)
This enables the new implementation of justification heuristic by default.
Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.
Diffstat (limited to 'test')
20 files changed, 192 insertions, 5 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 01deeaede..a3244ff4a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1511,7 +1511,18 @@ set(regress_1_tests regress1/datatypes/tuple_projection.smt2 regress1/decision/bug374a.smtv1.smt2 regress1/decision/error3.smtv1.smt2 + regress1/decision/issue5454-2.smt2 + regress1/decision/issue5454-3.smt2 + regress1/decision/issue5454.smt2 + regress1/decision/issue5785.smt2 + regress1/decision/jh-test1.smt2 regress1/decision/quant-Arrays_Q1-noinfer.smt2 + regress1/decision/wishue114.smt2 + regress1/decision/wishue115.smt2 + regress1/decision/wishue116.smt2 + regress1/decision/wishue149-2.smt2 + regress1/decision/wishue149-3.smt2 + regress1/decision/wishue160.smt2 regress1/error.cvc regress1/errorcrash.smt2 regress1/fp/rti_3_5_bug_report.smt2 @@ -2635,6 +2646,8 @@ set(regression_disabled_tests regress1/sygus/issue3498.smt2 regress2/arith/miplib-opt1217--27.smt2 regress2/nl/dumortier-050317.smt2 + # timeout after refactoring justification heuristic + regress2/ho/SYO362^5.p # time out regress3/unifpi-solve-car_1.lus.sy regress3/issue4476-ext-rew.smt2 diff --git a/test/regress/regress0/arith/div.05.smt2 b/test/regress/regress0/arith/div.05.smt2 index 99e6b04d5..0342fc90c 100644 --- a/test/regress/regress0/arith/div.05.smt2 +++ b/test/regress/regress0/arith/div.05.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_NRA) (set-info :smt-lib-version 2.6) diff --git a/test/regress/regress0/fp/issue3619.smt2 b/test/regress/regress0/fp/issue3619.smt2 index 55269e123..3e0858035 100644 --- a/test/regress/regress0/fp/issue3619.smt2 +++ b/test/regress/regress0/fp/issue3619.smt2 @@ -1,5 +1,5 @@ ; REQUIRES: symfpu -; COMMAND-LINE: +; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_FPLRA) (set-info :status sat) diff --git a/test/regress/regress0/fp/issue4277-assign-func.smt2 b/test/regress/regress0/fp/issue4277-assign-func.smt2 index 5c39abc5f..6a516a3ca 100644 --- a/test/regress/regress0/fp/issue4277-assign-func.smt2 +++ b/test/regress/regress0/fp/issue4277-assign-func.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat ; REQUIRES: symfpu (set-logic ALL) (set-option :uf-ho true) diff --git a/test/regress/regress0/issue5099-model-2.smt2 b/test/regress/regress0/issue5099-model-2.smt2 index 2bd27093f..9feada280 100644 --- a/test/regress/regress0/issue5099-model-2.smt2 +++ b/test/regress/regress0/issue5099-model-2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -m +; COMMAND-LINE: -m -q ; EXPECT: sat ; EXPECT: ((IP true)) (set-logic QF_NRA) @@ -6,4 +6,4 @@ (declare-const r16 Real) (assert (! (distinct (/ 1 r16) r11) :named IP)) (check-sat) -(get-assignment)
\ No newline at end of file +(get-assignment) diff --git a/test/regress/regress1/decision/issue5454-2.smt2 b/test/regress/regress1/decision/issue5454-2.smt2 new file mode 100644 index 000000000..d943a0020 --- /dev/null +++ b/test/regress/regress1/decision/issue5454-2.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic ANIA) +(declare-fun i () Int) +(declare-fun a () (Array Int Bool)) +(declare-fun b () (Array Bool (Array Int Bool))) +(assert (= (store b (>= i 0) a) (store b false (store (store a 0 true) i true)))) +(check-sat) diff --git a/test/regress/regress1/decision/issue5454-3.smt2 b/test/regress/regress1/decision/issue5454-3.smt2 new file mode 100644 index 000000000..5c8c826f2 --- /dev/null +++ b/test/regress/regress1/decision/issue5454-3.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic AUFLIA) +(declare-fun v () Bool) +(declare-fun i () Int) +(declare-fun i8 () Int) +(declare-fun u (Int Int Int Int Int Int) Bool) +(declare-fun ar () (Array Bool Bool)) +(declare-fun a () (Array Int Int)) +(declare-fun arr-- () (Array Bool Int)) +(declare-fun arr () (Array Bool (Array Int Bool))) +(declare-fun arr- () (Array Bool (Array Bool (Array Int Bool)))) +(assert (= arr- (store (store arr- false arr) (or (u (- 1) (select a i8) i (- 1) (select arr-- (select ar (= ar (store ar v true)))) 0) (not (u (- 1) (select a i8) i (- 1) (select arr-- (select ar (= ar (store ar v true)))) 0))) arr))) +(check-sat) diff --git a/test/regress/regress1/decision/issue5454.smt2 b/test/regress/regress1/decision/issue5454.smt2 new file mode 100644 index 000000000..0eadf3412 --- /dev/null +++ b/test/regress/regress1/decision/issue5454.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic AUFNIA) +(declare-fun _substvar_298_ () (Array Int Bool)) +(declare-fun _substvar_379_ () (Array Bool (Array Int Bool))) +(declare-fun _substvar_400_ () (Array Bool (Array Int Bool))) +(declare-fun i0 () Int) +(declare-fun arr--325748303185799905_1467848600759014513-0 () (Array Int Bool)) +(declare-fun arr-1467848600759014513_3143370635870088364-0 () (Array Bool (Array Int Bool))) +(assert (= _substvar_400_ (store arr-1467848600759014513_3143370635870088364-0 false (store (store arr--325748303185799905_1467848600759014513-0 776 true) i0 true)) (store arr-1467848600759014513_3143370635870088364-0 (>= i0 776) _substvar_298_) _substvar_379_)) +(check-sat) diff --git a/test/regress/regress1/decision/issue5785.smt2 b/test/regress/regress1/decision/issue5785.smt2 new file mode 100644 index 000000000..1bf48a1b2 --- /dev/null +++ b/test/regress/regress1/decision/issue5785.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --fmf-fun -i --decision=justification +; EXPECT: sat +(set-logic ALRA) +(set-option :fmf-fun true) +(declare-fun v2 () Bool) +(declare-sort S0 0) +(declare-fun arr--1494941102250395870_2811598136228140380-0 () (Array Bool S0)) +(declare-fun arr-2811598136228140380_-1494941102250395870-0 () (Array S0 Bool)) +(push) +(assert (select arr-2811598136228140380_-1494941102250395870-0 (select arr--1494941102250395870_2811598136228140380-0 false))) +(push) +(pop) +(pop) +(assert (select arr-2811598136228140380_-1494941102250395870-0 (select (store arr--1494941102250395870_2811598136228140380-0 v2 (select arr--1494941102250395870_2811598136228140380-0 true)) true))) +(check-sat) diff --git a/test/regress/regress1/decision/jh-test1.smt2 b/test/regress/regress1/decision/jh-test1.smt2 new file mode 100644 index 000000000..31b72e787 --- /dev/null +++ b/test/regress/regress1/decision/jh-test1.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic ALL) +(declare-const size4 String) +(declare-const p2_size Int) +(assert (= 1 (+ 1 (ite (= 1 p2_size) (str.to_code size4) 0)))) +(check-sat) diff --git a/test/regress/regress1/decision/wishue114.smt2 b/test/regress/regress1/decision/wishue114.smt2 new file mode 100644 index 000000000..9bdcf562d --- /dev/null +++ b/test/regress/regress1/decision/wishue114.smt2 @@ -0,0 +1,33 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +(set-logic SAT) +(set-option :incremental true) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun v5 () Bool) +(declare-fun v6 () Bool) +(declare-fun v7 () Bool) +(declare-fun v8 () Bool) +(check-sat) +(assert (and (and v1 v2) (and (or true (and (or false v1) v1)) (or (and false v1) v3)))) +(assert true) +(assert (or (and (or (and (or v4 v4) false) v2) (and true (or (and v5 true) (and v6 v5)))) v2)) +(assert v3) +(check-sat) +(assert false) +(assert true) +(assert (and (or (and v7 (and (and v2 v6) (and false v8))) (and (or (and v8 false) true) (and v6 true))) (and true v3))) +(push) +(assert v7) +(check-sat) +(assert true) +(pop) +(push) +(check-sat) +(check-sat) diff --git a/test/regress/regress1/decision/wishue115.smt2 b/test/regress/regress1/decision/wishue115.smt2 new file mode 100644 index 000000000..d8335654a --- /dev/null +++ b/test/regress/regress1/decision/wishue115.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +(set-logic SAT) +(set-option :incremental true) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun v5 () Bool) +(check-sat) +(check-sat) +(assert (or (not (and (or v1 (and v1 true)) (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool)) (and v1 false)))) false)) +(assert (or (or (not true) (and (and (not v1) (or v1 v1)) v1)) (or (and (not (not v2)) (forall ((q0_1 Bool) (q0_2 Bool)) (and q0_2 q0_2))) (and (not (and true v3)) (or (not v1) v2))))) +(check-sat) +(check-sat) +(assert (not (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool) (q0_4 Bool)) (and (not (forall ((q1_1 Bool) (q1_2 Bool) (q1_3 Bool) (q1_4 Bool)) false)) (not (forall ((q1_1 Bool)) q0_2)))))) +(assert (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool) (q0_4 Bool) (q0_5 Bool)) (not v1))) +(push) +(check-sat) +(assert (and (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool)) (forall ((q1_1 Bool) (q1_2 Bool) (q1_3 Bool) (q1_4 Bool)) (not (forall ((q2_1 Bool)) true)))) (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool)) (not (or q0_3 (forall ((q1_1 Bool)) v4)))))) +(assert (or (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool) (q0_4 Bool)) (forall ((q1_1 Bool) (q1_2 Bool) (q1_3 Bool)) (not q1_1))) v1)) +(assert v5) +(check-sat) +(assert (not (forall ((q0_1 Bool)) (and (or (or true q0_1) (and false q0_1)) (not true))))) +(pop) diff --git a/test/regress/regress1/decision/wishue116.smt2 b/test/regress/regress1/decision/wishue116.smt2 new file mode 100644 index 000000000..3cfb1540b --- /dev/null +++ b/test/regress/regress1/decision/wishue116.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic SAT) +(set-option :incremental true) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun v5 () Bool) +(check-sat) +(assert (and (or (or (and (or false v1) v2) (not (not v3))) (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool)) (forall ((q1_1 Bool)) q1_1))) true)) +(check-sat) +(assert (or (not v2) (or (and (or (and v4 true) v2) (forall ((q0_1 Bool)) (not true))) (not (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool) (q0_4 Bool)) (forall ((q1_1 Bool) (q1_2 Bool)) v1)))))) +(push) +(assert (not v5)) +(assert (not true)) +(pop) +(push) +(check-sat) +(pop) +(assert true) diff --git a/test/regress/regress1/decision/wishue149-2.smt2 b/test/regress/regress1/decision/wishue149-2.smt2 new file mode 100644 index 000000000..6095a4940 --- /dev/null +++ b/test/regress/regress1/decision/wishue149-2.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic AUFLIA) +(declare-const v4 Bool) +(declare-const v6 Bool) +(declare-const arr0 (Array Bool Int)) +(declare-const arr1 (Array Bool (Array Bool Int))) +(assert (= (store arr1 v6 (store arr0 true 0)) (store arr1 true (store (store (store arr0 true 0) v4 0) true 96)) arr1 arr1)) +(check-sat) diff --git a/test/regress/regress1/decision/wishue149-3.smt2 b/test/regress/regress1/decision/wishue149-3.smt2 new file mode 100644 index 000000000..fbd200f66 --- /dev/null +++ b/test/regress/regress1/decision/wishue149-3.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic AUFLRA) +(declare-fun _substvar_323_ () Bool) +(declare-sort S0 0) +(declare-const arr-8825057447867329665_7821057345541224443-0 (Array Bool S0)) +(declare-const arr--3985848114402943554_-2673408464765268945-0 (Array Real (Array Bool S0))) +(assert (not (= (select arr--3985848114402943554_-2673408464765268945-0 0.0) (store (store arr-8825057447867329665_7821057345541224443-0 _substvar_323_ (select arr-8825057447867329665_7821057345541224443-0 true)) false (select arr-8825057447867329665_7821057345541224443-0 false)) arr-8825057447867329665_7821057345541224443-0 arr-8825057447867329665_7821057345541224443-0))) +(check-sat) diff --git a/test/regress/regress1/decision/wishue160.smt2 b/test/regress/regress1/decision/wishue160.smt2 new file mode 100644 index 000000000..8497a66fc --- /dev/null +++ b/test/regress/regress1/decision/wishue160.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic ALIA) +(set-option :repeat-simp true) +(set-option :sygus-rr-synth-check true) +(declare-fun v6 () Bool) +(declare-const arr-7579056739068271278_-8074447279386590332-0 (Array Bool Int)) +(assert (= false false false (= arr-7579056739068271278_-8074447279386590332-0 (store arr-7579056739068271278_-8074447279386590332-0 v6 746)) false false false)) +(check-sat) diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 index 61f0f207b..21405dfdb 100644 --- a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 +++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --uf-ho --finite-model-find -q +; COMMAND-LINE: --uf-ho --finite-model-find -q --decision=justification-old ; EXPECT: sat (set-logic ALL) diff --git a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 index 45727743f..796d7e753 100644 --- a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 +++ b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --no-jh-rlv-order ; REQUIRES: symfpu ; EXPECT: unsat (set-logic AUFBVFPDTNIRA) diff --git a/test/regress/regress2/strings/issue6483.smt2 b/test/regress/regress2/strings/issue6483.smt2 index 3ee748d27..a86ce1fe5 100644 --- a/test/regress/regress2/strings/issue6483.smt2 +++ b/test/regress/regress2/strings/issue6483.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: unsat (set-logic QF_SLIA) (declare-fun a () String) (assert diff --git a/test/regress/regress3/ho/SYO362^5.p b/test/regress/regress3/ho/SYO362^5.p index c01d3f235..b9537fd0e 100644 --- a/test/regress/regress3/ho/SYO362^5.p +++ b/test/regress/regress3/ho/SYO362^5.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim +% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim --decision=justification-old % EXPECT: % SZS status Theorem for SYO362^5 thf(cK,type,( |