diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-22 15:48:25 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-22 20:48:25 +0000 |
commit | 4929b5dcfaba1e051309a0debfeaf9f8bf8e2d8b (patch) | |
tree | 467f72854fdc931f1d2ffc9124ab2fa841874d93 /test | |
parent | b3774c9758b6a23c8ef5d98eaa0879a814114674 (diff) |
Add more abduction regressions (#7461)
Fixes #5848.
This also fixes an issue leftover from #6605 where a spurious assertion failure was thrown.
Also introduces subfolder regress/regress1/abduction.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 27 | ||||
-rw-r--r-- | test/regress/regress1/abduction/abd-simple-conj-4.smt2 (renamed from test/regress/regress1/sygus/abd-simple-conj-4.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/abduct-dt.smt2 (renamed from test/regress/regress1/abduct-dt.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2 (renamed from test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2 (renamed from test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/abduction_streq.readable.smt2 (renamed from test/regress/regress1/sygus/abduction_streq.readable.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/issue5848-2.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2 (renamed from test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/issue5848-4.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress1/abduction/issue5848.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress1/abduction/issue6605-1.smt2 | 11 | ||||
-rw-r--r-- | test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2 (renamed from test/regress/regress1/sygus-abduct-ex1-grammar.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2 (renamed from test/regress/regress1/sygus-abduct-test-ccore.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/sygus-abduct-test-user.smt2 (renamed from test/regress/regress1/sygus-abduct-test-user.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/sygus-abduct-test.smt2 (renamed from test/regress/regress1/sygus-abduct-test.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/uf-abduct.smt2 (renamed from test/regress/regress1/sygus/uf-abduct.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/yoni-true-sol.smt2 (renamed from test/regress/regress1/sygus/yoni-true-sol.smt2) | 0 |
17 files changed, 48 insertions, 11 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b80fd890b..1c81316c3 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1489,7 +1489,22 @@ set(regress_0_tests # Regression level 1 tests set(regress_1_tests - regress1/abduct-dt.smt2 + regress1/abduction/sygus-abduct-test-user.smt2 + regress1/abduction/issue5848-4.smt2 + regress1/abduction/issue5848-2.smt2 + regress1/abduction/issue5848.smt2 + regress1/abduction/issue6605-1.smt2 + regress1/abduction/abduct-dt.smt2 + regress1/abduction/sygus-abduct-test-ccore.smt2 + regress1/abduction/sygus-abduct-test.smt2 + regress1/abduction/abd-simple-conj-4.smt2 + regress1/abduction/abduction_streq.readable.smt2 + regress1/abduction/yoni-true-sol.smt2 + regress1/abduction/uf-abduct.smt2 + regress1/abduction/abduction_1255.corecstrs.readable.smt2 + regress1/abduction/abduction-no-pbe-sym-break.smt2 + regress1/abduction/issue5848-3-trivial-no-abduct.smt2 + regress1/abduction/sygus-abduct-ex1-grammar.smt2 regress1/arith/arith-brab-test.smt2 regress1/arith/arith-int-004.cvc.smt2 regress1/arith/arith-int-011.cvc.smt2 @@ -2322,15 +2337,7 @@ set(regress_1_tests regress1/strings/update-ex1.smt2 regress1/strings/update-ex2.smt2 regress1/strings/username_checker_min.smt2 - regress1/sygus-abduct-ex1-grammar.smt2 - regress1/sygus-abduct-test.smt2 - regress1/sygus-abduct-test-ccore.smt2 - regress1/sygus-abduct-test-user.smt2 regress1/sygus/VC22_a.sy - regress1/sygus/abd-simple-conj-4.smt2 - regress1/sygus/abduction_1255.corecstrs.readable.smt2 - regress1/sygus/abduction_streq.readable.smt2 - regress1/sygus/abduction-no-pbe-sym-break.smt2 regress1/sygus/abv.sy regress1/sygus/array-grammar-store.sy regress1/sygus/array_search_5-Q-easy.sy @@ -2476,10 +2483,8 @@ set(regress_1_tests regress1/sygus/trivial-stream.sy regress1/sygus/twolets1.sy regress1/sygus/twolets2-orig.sy - regress1/sygus/uf-abduct.smt2 regress1/sygus/unbdd_inv_gen_winf1.sy regress1/sygus/univ_2-long-repeat.sy - regress1/sygus/yoni-true-sol.smt2 regress1/sym/q-constant.smt2 regress1/sym/q-function.smt2 regress1/sym/qf-function.smt2 diff --git a/test/regress/regress1/sygus/abd-simple-conj-4.smt2 b/test/regress/regress1/abduction/abd-simple-conj-4.smt2 index 98bf70fd7..98bf70fd7 100644 --- a/test/regress/regress1/sygus/abd-simple-conj-4.smt2 +++ b/test/regress/regress1/abduction/abd-simple-conj-4.smt2 diff --git a/test/regress/regress1/abduct-dt.smt2 b/test/regress/regress1/abduction/abduct-dt.smt2 index d72d15a21..d72d15a21 100644 --- a/test/regress/regress1/abduct-dt.smt2 +++ b/test/regress/regress1/abduction/abduct-dt.smt2 diff --git a/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2 b/test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2 index 79fa4f230..79fa4f230 100644 --- a/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2 +++ b/test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2 diff --git a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 b/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2 index 1595b0865..1595b0865 100644 --- a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 +++ b/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2 diff --git a/test/regress/regress1/sygus/abduction_streq.readable.smt2 b/test/regress/regress1/abduction/abduction_streq.readable.smt2 index b466ab33e..b466ab33e 100644 --- a/test/regress/regress1/sygus/abduction_streq.readable.smt2 +++ b/test/regress/regress1/abduction/abduction_streq.readable.smt2 diff --git a/test/regress/regress1/abduction/issue5848-2.smt2 b/test/regress/regress1/abduction/issue5848-2.smt2 new file mode 100644 index 000000000..36716c4c7 --- /dev/null +++ b/test/regress/regress1/abduction/issue5848-2.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --produce-abducts +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun v9 () Bool) +(get-abduct A (or true v9)) diff --git a/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2 b/test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2 index b64e27b45..b64e27b45 100644 --- a/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2 +++ b/test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2 diff --git a/test/regress/regress1/abduction/issue5848-4.smt2 b/test/regress/regress1/abduction/issue5848-4.smt2 new file mode 100644 index 000000000..93cd8f52b --- /dev/null +++ b/test/regress/regress1/abduction/issue5848-4.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --produce-abducts +; EXPECT: none +(set-logic UFLRA) +(declare-sort S0 0) +(declare-fun S0-0 () S0) +(declare-fun S0-1 () S0) +(declare-fun v87 () Bool) +(get-abduct A (and false (exists ((q117 S0)) (or v87 (and (= S0-1 q117) (= q117 S0-0)))))) diff --git a/test/regress/regress1/abduction/issue5848.smt2 b/test/regress/regress1/abduction/issue5848.smt2 new file mode 100644 index 000000000..7b8761235 --- /dev/null +++ b/test/regress/regress1/abduction/issue5848.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --produce-abducts +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun a () Int) +(assert (= (mod 0 a) 0)) +(get-abduct A (= a 1)) diff --git a/test/regress/regress1/abduction/issue6605-1.smt2 b/test/regress/regress1/abduction/issue6605-1.smt2 new file mode 100644 index 000000000..a33fdd905 --- /dev/null +++ b/test/regress/regress1/abduction/issue6605-1.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --produce-abducts +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(set-option :produce-abducts true) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(assert (= (>= b c) (>= 0 a))) +(assert (= c a)) +(get-abduct d (<= a b)) diff --git a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 b/test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2 index bda237676..bda237676 100644 --- a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 +++ b/test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2 diff --git a/test/regress/regress1/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2 index 86f5fe133..86f5fe133 100644 --- a/test/regress/regress1/sygus-abduct-test-ccore.smt2 +++ b/test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2 diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/abduction/sygus-abduct-test-user.smt2 index bb02ebce2..bb02ebce2 100644 --- a/test/regress/regress1/sygus-abduct-test-user.smt2 +++ b/test/regress/regress1/abduction/sygus-abduct-test-user.smt2 diff --git a/test/regress/regress1/sygus-abduct-test.smt2 b/test/regress/regress1/abduction/sygus-abduct-test.smt2 index ed1ea6ddf..ed1ea6ddf 100644 --- a/test/regress/regress1/sygus-abduct-test.smt2 +++ b/test/regress/regress1/abduction/sygus-abduct-test.smt2 diff --git a/test/regress/regress1/sygus/uf-abduct.smt2 b/test/regress/regress1/abduction/uf-abduct.smt2 index bfcfe39fd..bfcfe39fd 100644 --- a/test/regress/regress1/sygus/uf-abduct.smt2 +++ b/test/regress/regress1/abduction/uf-abduct.smt2 diff --git a/test/regress/regress1/sygus/yoni-true-sol.smt2 b/test/regress/regress1/abduction/yoni-true-sol.smt2 index 464f7c729..464f7c729 100644 --- a/test/regress/regress1/sygus/yoni-true-sol.smt2 +++ b/test/regress/regress1/abduction/yoni-true-sol.smt2 |