Support for printing solutions involving LetGTerm sygus. Bug fix define-fun within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions.

4 files changed, 61 insertions, 1 deletions

diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 40f3fa4aa..dc6a1e0d1 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -32,7 +32,10 @@ TESTS = commutative.sy \
         const-var-test.sy \
         no-syntax-test.sy \
         no-syntax-test-no-si.sy \
-        no-flat-simp.sy
+        no-flat-simp.sy \
+        twolets2-orig.sy \
+        let-ringer.sy \
+        let-simp.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy
new file mode 100644
index 000000000..046d074d9
--- /dev/null
+++ b/test/regress/regress0/sygus/let-ringer.sy
@@ -0,0 +1,14 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(define-fun g ((x Int)) Int (ite (= x 1) 15 19))
+(synth-fun f ((x Int)) Int
+    ((Start Int (x
+                 0
+                 1
+                 (- Start Start)
+                 (let ((z Int Start) (w Int Start)) (+ z (+ x (+ x (+ Start (+ 1 (+ (g w) z)))))))))))
+                 
+(declare-var x Int)
+(constraint (= (f x) (+ (* 4 x) 15)))
+(check-synth)
diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy
new file mode 100644
index 000000000..daca906a2
--- /dev/null
+++ b/test/regress/regress0/sygus/let-simp.sy
@@ -0,0 +1,15 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-fun f ((x Int) (y Int)) Int
+    ((Start Int (x
+                 y
+                 0
+                 (- Start Start)
+                 (let ((z Int Start)) (+ z z))))))
+
+(declare-var x Int)
+(declare-var y Int)
+(constraint (= (f x y) (* 3 x)))
+(check-synth)
+
diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy
new file mode 100644
index 000000000..c1066277e
--- /dev/null
+++ b/test/regress/regress0/sygus/twolets2-orig.sy
@@ -0,0 +1,28 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-fun f1 ((x Int)) Int
+	   (
+	   (Start Int (
+	   	      (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z))
+	   	      )
+ 	   )
+	   (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+
+	   )
+)
+(synth-fun f2 ((x Int)) Int
+	   (
+	   (Start Int (x
+	   	      (let ((y Int Start) (z Int CInt)) (+ (+ y x) z))
+	   	      )
+ 	   )
+	   (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+
+	   )
+)
+(declare-var x1 Int)
+(declare-var x2 Int)
+(constraint (= (+ (f1 x1)(f2 x2)) (+ (+ x2 x2) (+ x1 8))))
+(check-synth)
+