diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-14 11:33:14 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-14 11:33:14 -0500 |
| commit | c308c094548bcd9bee59e33334d147a9afe97018 (patch) | |
| tree | 0191612aa290c1f3bcf915f140e0494cbb12d1e9 /test | |
| parent | 33420e77e9f7ee7a429708db3a7f6c28aef7d0ec (diff) | |
Add regressions, change defaults. (#1911)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/large-const-simp.sy | 13 | ||||
| -rw-r--r-- | test/regress/regress2/sygus/ex23.sy | 23 |
3 files changed, 38 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 5cb24d072..7784a6825 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1488,6 +1488,7 @@ REG1_TESTS = \ regress1/sygus/icfp_easy-ite.sy \ regress1/sygus/inv-example.sy \ regress1/sygus/inv-unused.sy \ + regress1/sygus/large-const-simp.sy \ regress1/sygus/list-head-x.sy \ regress1/sygus/max.sy \ regress1/sygus/multi-fun-polynomial2.sy \ @@ -1589,6 +1590,7 @@ REG2_TESTS = \ regress2/strings/norn-dis-0707-3.smt2 \ regress2/sygus/MPwL_d1s3.sy \ regress2/sygus/array_sum_dd.sy \ + regress2/sygus/ex23.sy \ regress2/sygus/icfp_easy_mt_ite.sy \ regress2/sygus/inv_gen_n_c11.sy \ regress2/sygus/lustre-real.sy \ diff --git a/test/regress/regress1/sygus/large-const-simp.sy b/test/regress/regress1/sygus/large-const-simp.sy new file mode 100644 index 000000000..31f660b2a --- /dev/null +++ b/test/regress/regress1/sygus/large-const-simp.sy @@ -0,0 +1,13 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-add-const-grammar +(set-logic LIA) + +(synth-fun lc ((x Int)) Int) + +(declare-var x Int) +(declare-var y Int) + +(constraint (> (lc x) 1500)) +(constraint (< (lc x) 1600)) + +(check-synth) diff --git a/test/regress/regress2/sygus/ex23.sy b/test/regress/regress2/sygus/ex23.sy new file mode 100644 index 000000000..61b08a838 --- /dev/null +++ b/test/regress/regress2/sygus/ex23.sy @@ -0,0 +1,23 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) + +(synth-inv inv-f ((y Int) (z Int) (c Int))) + +(declare-primed-var y Int) +(declare-primed-var z Int) +(declare-primed-var c Int) + +(define-fun pre-f ((y Int) (z Int) (c Int)) Bool +(and (and (= c 0) (>= y 0)) (and (>= 127 y) (= z (* 36 y))))) + + +(define-fun trans-f ((y Int) (z Int) (c Int) (y! Int) (z! Int) (c! Int)) Bool +(and (and (and (< c 36) (= z! (+ z 1))) (= c! (+ c 1))) (= y! y))) + +(define-fun post-f ((y Int) (z Int) (c Int)) Bool +(not (and (< c 36) (or (< z 0) (>= z 4608))))) + +(inv-constraint inv-f pre-f trans-f post-f) + +(check-synth) |