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 /test/regress/regress1/sygus | |
parent | 55050d2a3dff2d0428171c51d0ac54626d579d3a (diff) |
Add sygus stream regressions (#2330)
Diffstat (limited to 'test/regress/regress1/sygus')
-rw-r--r-- | test/regress/regress1/sygus/commutative-stream.sy | 24 | ||||
-rw-r--r-- | test/regress/regress1/sygus/trivial-stream.sy | 18 |
2 files changed, 42 insertions, 0 deletions
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) |