From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 17 Aug 2018 18:29:15 +0000 (-0500)
Subject:  Add sygus stream regressions (#2330)
X-Git-Tag: cvc5-1.0.0~4762
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=58ee4bc13c37bf25ddafd07bc09c8d975dc6d62d;p=cvc5.git

 Add sygus stream regressions (#2330)
---

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)