From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 15 May 2018 19:48:43 +0000 (-0500)
Subject: adding regressions (#1925)
X-Git-Tag: cvc5-1.0.0~5048
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=35c2868435b8333113e7d1932a8f21b5f84fe69e;p=cvc5.git

adding regressions (#1925)
---

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 7784a6825..c0f1cf315 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1470,6 +1470,7 @@ REG1_TESTS = \
 	regress1/sygus/array_search_2.sy \
 	regress1/sygus/array_sum_2_5.sy \
 	regress1/sygus/cegar1.sy \
+	regress1/sygus/cegisunif-depth1.sy \
 	regress1/sygus/cggmp.sy \
 	regress1/sygus/clock-inc-tuple.sy \
 	regress1/sygus/commutative.sy \
@@ -1590,6 +1591,7 @@ REG2_TESTS = \
 	regress2/strings/norn-dis-0707-3.smt2 \
 	regress2/sygus/MPwL_d1s3.sy \
 	regress2/sygus/array_sum_dd.sy \
+	regress2/sygus/cegisunif-depth1-bv.sy \
 	regress2/sygus/ex23.sy \
 	regress2/sygus/icfp_easy_mt_ite.sy \
 	regress2/sygus/inv_gen_n_c11.sy \
diff --git a/test/regress/regress1/sygus/cegisunif-depth1.sy b/test/regress/regress1/sygus/cegisunif-depth1.sy
new file mode 100644
index 000000000..1e810fea3
--- /dev/null
+++ b/test/regress/regress1/sygus/cegisunif-depth1.sy
@@ -0,0 +1,34 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-unif --sygus-out=status
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Int
+  (
+    (Start Int
+      (0 1 x y
+        (+ Start Start)
+        (- Start Start)
+        (ite CBool Start Start)
+        )
+      )
+    (CBool Bool
+      (true false
+        (and CBool CBool)
+        (or CBool CBool)
+        (not CBool)
+        (<= Start Start)
+        ; Having equality makes the problem easy to CEGIS
+        ; (= Start Start)
+        )
+      )
+    )
+  )
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (f 0 1) 0))
+(constraint (= (f 1 y) y))
+(constraint (= (f 2 1) 0))
+
+(check-synth)
diff --git a/test/regress/regress2/sygus/cegisunif-depth1-bv.sy b/test/regress/regress2/sygus/cegisunif-depth1-bv.sy
new file mode 100644
index 000000000..4b0cefcda
--- /dev/null
+++ b/test/regress/regress2/sygus/cegisunif-depth1-bv.sy
@@ -0,0 +1,37 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-unif --sygus-out=status
+(set-logic BV)
+
+(synth-fun f ((x (BitVec 64)) (y (BitVec 64))) (BitVec 64)
+  (
+    (Start (BitVec 64)
+      (#x0000000000000000 #x0000000000000001 x y
+        (bvnot Start)
+        (bvand Start Start)
+        (bvor Start Start)
+        (bvxor Start Start)
+        (bvadd Start Start)
+        (ite CBool Start Start)
+        )
+      )
+    (CBool Bool
+      (true false
+        (and CBool CBool)
+        (or CBool CBool)
+        (not CBool)
+        (bvule Start Start)
+        (= Start Start)
+        )
+      )
+    )
+  )
+
+(declare-var x (BitVec 64))
+(declare-var y (BitVec 64))
+
+(constraint (= (f #x0000000000000000 #x0000000000000001) #x0000000000000000))
+(constraint (= (f #x0000000000000000 #x0000000000000000) #x0000000000000001))
+(constraint (= (f #x0000000000000001 y) y))
+(constraint (= (f #x0000000000000002 #x0000000000000001) #x0000000000000000))
+
+(check-synth)