diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-09-26 18:13:29 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-09-26 18:13:29 -0500 |
| commit | 672d1347c2daeddb8c434ea996f95ba555d22589 (patch) | |
| tree | ef2634cd546e10e14e30d44aadb557e020e278e2 /test/regress | |
| parent | bd866bbf75606663315c15ce4f28862e99b70cbd (diff) | |
Makes SyGuS parsing more robust in invariant problems (#2509)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/inv-different-var-order.sy | 22 |
3 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 35672d77a..5252954dc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -826,6 +826,7 @@ set(regress_0_tests regress0/sygus/check-generic-red.sy regress0/sygus/const-var-test.sy regress0/sygus/dt-no-syntax.sy + regress0/sygus/inv-different-var-order.sy regress0/sygus/let-ringer.sy regress0/sygus/let-simp.sy regress0/sygus/no-syntax-test-bool.sy diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index c79f42078..08d0ca5bb 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -839,6 +839,7 @@ REG0_TESTS = \ regress0/sygus/const-var-test.sy \ regress0/sygus/dt-no-syntax.sy \ regress0/sygus/hd-05-d1-prog-nogrammar.sy \ + regress0/sygus/inv-different-var-order.sy \ regress0/sygus/let-ringer.sy \ regress0/sygus/let-simp.sy \ regress0/sygus/no-syntax-test-bool.sy \ diff --git a/test/regress/regress0/sygus/inv-different-var-order.sy b/test/regress/regress0/sygus/inv-different-var-order.sy new file mode 100644 index 000000000..c3f43fc07 --- /dev/null +++ b/test/regress/regress0/sygus/inv-different-var-order.sy @@ -0,0 +1,22 @@ +; COMMAND-LINE: --sygus-out=status +;EXPECT: unsat +(set-logic LIA) +(synth-inv inv-f ((x Int) (y Int) (b Bool))) +(declare-primed-var b Bool) +(declare-primed-var x Int) +(declare-primed-var y Int) +(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool +(and +(and (>= x 5) (<= x 9)) +(and (>= y 1) (<= y 3)) +) +) +(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool +(and +(and (= b! b) (= y! x)) +(ite b (= x! (+ x 10)) (= x! (+ x 12))) +) +) +(define-fun post-f ((x Int) (y Int) (b Bool)) Bool true) +(inv-constraint inv-f pre-f trans-f post-f) +(check-synth)
\ No newline at end of file |