Robust strategy for single invocation LIA synthesis conjectures. Add regressions.

6 files changed, 97 insertions, 3 deletions

diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index b5ea8b476..ef65ead1f 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -23,11 +23,15 @@ TESTS = hd-01-d1-prog.sy \
         commutative.sy \
         constant.sy \
         multi-fun-polynomial2.sy \
-        unbdd_inv_gen_winf1.sy
+        unbdd_inv_gen_winf1.sy \
+	max.sy \
+	array_sum_2_5.sy \
+	parity-AIG-d0.sy \
+	twolets1.sy \
+	array_search_2.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
-	max.sl \
 	max.smt2 \
 	sygus-uf.sl
 
diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy
new file mode 100644
index 000000000..5d8cd8752
--- /dev/null
+++ b/test/regress/regress0/sygus/array_search_2.sy
@@ -0,0 +1,11 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
+(declare-var x1 Int)
+(declare-var x2 Int)
+(declare-var k Int)
+(constraint (=> (< x1 x2) (=> (< k x1) (= (findIdx x1 x2 k) 0))))
+(constraint (=> (< x1 x2) (=> (> k x2) (= (findIdx x1 x2 k) 2))))
+(constraint (=> (< x1 x2) (=> (and (> k x1) (< k x2)) (= (findIdx x1 x2 k) 1))))
+(check-synth)
diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy
new file mode 100644
index 000000000..48b5c8a4d
--- /dev/null
+++ b/test/regress/regress0/sygus/array_sum_2_5.sy
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start)    (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
+(declare-var x1 Int)
+(declare-var x2 Int)
+(constraint (=> (> (+ x1 x2) 5) (= (findSum x1 x2 ) (+ x1 x2))))
+(constraint (=> (<= (+ x1 x2) 5) (= (findSum x1 x2 ) 0)))
+(check-synth)
diff --git a/test/regress/regress0/sygus/max.sl b/test/regress/regress0/sygus/max.sy
index fdd925196..4fc515353 100644
--- a/test/regress/regress0/sygus/max.sl
+++ b/test/regress/regress0/sygus/max.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi-si
 (set-logic LIA)
 
 (synth-fun max ((x Int) (y Int)) Int
diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy
new file mode 100644
index 000000000..c4fbd1c17
--- /dev/null
+++ b/test/regress/regress0/sygus/parity-AIG-d0.sy
@@ -0,0 +1,30 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic BV)
+
+(define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+  (xor (not (xor a b)) (not (xor c d))))
+
+(synth-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+           ((Start Bool ((and Start Start) (not Start) a b c d))))
+
+(declare-var a Bool)
+(declare-var b Bool)
+(declare-var c Bool)
+(declare-var d Bool)
+
+(constraint
+ (= (parity a b c d) 
+    (and (AIG a b c d)
+        (not (and (and (not (and a b)) (not (and (not a) (not b))))
+               (and (not (and (not c) (not d))) (not (and c d))))))))
+
+
+(check-synth)
+
+; Solution:
+;(define-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+;(not
+;  (and
+;   (and (not (and (not a) b)) (not (and d (not c))))
+;   (and (not (and (not b) a)) (not (and (not d) c)))))) 
\ No newline at end of file
diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy
new file mode 100644
index 000000000..24b0f2c09
--- /dev/null
+++ b/test/regress/regress0/sygus/twolets1.sy
@@ -0,0 +1,40 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+
+;; f1 is x plus 2 ;; f2 is 2x plus 5
+
+(define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))
+
+(synth-fun f1 ((x Int)) Int
+	   (
+	   (Start Int (
+	   	      (let0 Intx CInt CInt)
+	   	      )
+ 	   )
+ 	   (Intx Int (x))
+	   (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
+	   	      (let0 Intx Start CInt)
+	   	      )
+ 	   )
+     (Intx Int (x))
+	   (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+
+	   )
+)
+
+
+(declare-var x Int)
+
+(constraint (= (+ (f1 x)(f2 x)) (+ (+ x x) (+ x 8))))
+(constraint (= (- (f2 x)(f1 x)) (+ x 2)))
+
+(check-synth)
+