diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-17 13:29:15 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-17 11:29:15 -0700 |
| commit | 58ee4bc13c37bf25ddafd07bc09c8d975dc6d62d (patch) | |
| tree | a0003640718152afbca7fb5718753e2ff4d9e521 | |
| parent | 55050d2a3dff2d0428171c51d0ac54626d579d3a (diff) | |
Add sygus stream regressions (#2330)
| -rw-r--r-- | test/regress/Makefile.tests | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/commutative-stream.sy | 24 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/trivial-stream.sy | 18 |
3 files changed, 44 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 9db34bca2..d27988d70 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1517,6 +1517,7 @@ REG1_TESTS = \ regress1/sygus/cggmp.sy \ regress1/sygus/clock-inc-tuple.sy \ regress1/sygus/commutative.sy \ + regress1/sygus/commutative-stream.sy \ regress1/sygus/constant.sy \ regress1/sygus/constant-bool-si-all.sy \ regress1/sygus/constant-dec-tree-bug.sy \ @@ -1571,6 +1572,7 @@ REG1_TESTS = \ regress1/sygus/tl-type-0.sy \ regress1/sygus/tl-type-4x.sy \ regress1/sygus/tl-type.sy \ + regress1/sygus/trivial-stream.sy \ regress1/sygus/triv-type-mismatch-si.sy \ regress1/sygus/twolets1.sy \ regress1/sygus/twolets2-orig.sy \ diff --git a/test/regress/regress1/sygus/commutative-stream.sy b/test/regress/regress1/sygus/commutative-stream.sy new file mode 100644 index 000000000..b07051d37 --- /dev/null +++ b/test/regress/regress1/sygus/commutative-stream.sy @@ -0,0 +1,24 @@ +; EXPECT: (define-fun comm ((x Int) (y Int)) Int (+ x y)) +; EXPECT: (define-fun comm ((x Int) (y Int)) Int (- x x)) +; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded. +; EXPECT: ") +; EXIT: 1 + +; COMMAND-LINE: --sygus-stream --sygus-abort-size=2 + +(set-logic LIA) + +(synth-fun comm ((x Int) (y Int)) Int + ((Start Int (x + y + (+ Start Start) + (- Start Start) + )) + )) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (comm x y) (comm y x))) + +(check-synth) diff --git a/test/regress/regress1/sygus/trivial-stream.sy b/test/regress/regress1/sygus/trivial-stream.sy new file mode 100644 index 000000000..42965ff32 --- /dev/null +++ b/test/regress/regress1/sygus/trivial-stream.sy @@ -0,0 +1,18 @@ +; EXPECT: (define-fun triv ((x Int) (y Int)) Int x) +; EXPECT: (define-fun triv ((x Int) (y Int)) Int y) +; EXPECT: (error "Maximum term size (0) for enumerative SyGuS exceeded. +; EXPECT: ") +; EXIT: 1 + +; COMMAND-LINE: --sygus-stream --sygus-abort-size=0 + +(set-logic LIA) + +(synth-fun triv ((x Int) (y Int)) Int + ((Start Int (x + y + (+ Start Start) + )) + )) + +(check-synth) |