Squashed merge of SygusComp 2015 branch.

6 files changed, 59 insertions, 1 deletions

diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index dbef0494a..9d7155f78 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -38,7 +38,12 @@ TESTS = commutative.sy \
         let-simp.sy \
         tl-type.sy \
         dup-op.sy \
-        nflat-fwd.sy
+        nflat-fwd.sy \
+        nflat-fwd-3.sy \
+        enum-test.sy \
+        no-syntax-test-bool.sy \
+        inv-example.sy \
+        uminus_one.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy
new file mode 100644
index 000000000..52a72c07d
--- /dev/null
+++ b/test/regress/regress0/sygus/enum-test.sy
@@ -0,0 +1,8 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(define-sort D (Enum (a b)))
+(define-fun f ((x D)) Int (ite (= x D::a) 3 7))
+(synth-fun g () D ((Start D (D::a D::b))))
+(constraint (= (f g) 7))
+(check-synth)
\ No newline at end of file
diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy
new file mode 100644
index 000000000..dda8e0ed5
--- /dev/null
+++ b/test/regress/regress0/sygus/inv-example.sy
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-inv inv-f ((x Int) (y Int) (b Bool)))
+(declare-primed-var x Int)
+(declare-primed-var y Int)
+(declare-primed-var b Bool)
+(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (and (>= x 5) (<= x 9)) (and (>= y 1) (<= y 3))))
+(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (and (and (= b! b) (= y! x)) (ite b (= x! (+ x 10)) (= x! (+ x 12)))))
+(define-fun post-f ((x Int) (y Int) (b Bool)) Bool (<= y x))
+(inv-constraint inv-f pre-f trans-f post-f)
+(check-synth)
\ No newline at end of file
diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy
new file mode 100644
index 000000000..bd7c79e3e
--- /dev/null
+++ b/test/regress/regress0/sygus/nflat-fwd-3.sy
@@ -0,0 +1,11 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-fun f ((x Int)) Int
+    ((Start Int ((+ (+ Con Con) Con) x))
+     (Con Int (0 1))))
+
+(declare-var x Int)
+(constraint (= (f x) 2))
+(check-synth)
+
diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy
new file mode 100644
index 000000000..cc3855ad1
--- /dev/null
+++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy
@@ -0,0 +1,15 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Bool)
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (f x y) (>= (+ x y) 500)))
+
+
+(check-synth)
+
diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy
new file mode 100644
index 000000000..b020c0bee
--- /dev/null
+++ b/test/regress/regress0/sygus/uminus_one.sy
@@ -0,0 +1,7 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+(set-logic LIA)
+(synth-fun f ((x Int)) Int ((Start Int ((- 1)))))
+(declare-var x Int)
+(constraint (= (f x) (- 1)))
+(check-synth)
\ No newline at end of file