Add sygus stream regressions (#2330)

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 9db34bca22236a1845364348d75225b24139a93a..d27988d70b5199ee20737bc68211803fe8869abd 100644 (file)
--- 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 (file)
index 0000000..b07051d
--- /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 (file)
index 0000000..42965ff
--- /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)