Flag to check invariance of entire values in sygus explain (#1908)

2 files changed, 135 insertions, 0 deletions

diff --git a/test/regress/regress2/sygus/sixfuncs.sy b/test/regress/regress2/sygus/sixfuncs.sy
new file mode 100644
index 000000000..5280ffb20
--- /dev/null
+++ b/test/regress/regress2/sygus/sixfuncs.sy
@@ -0,0 +1,81 @@
+(set-logic LIA)
+
+(synth-fun f1 ((p1 Int) (P1 Int)) Int
+	   ((Start Int (
+			p1
+			P1
+			(- Start Start)
+			(+ Start Start)
+                     )
+           )))
+
+(synth-fun f2 ((p1 Int) (P1 Int)) Int
+	   ((Start Int (
+			p1
+			P1
+			(+ Start Start)
+                     )
+           )))
+
+(synth-fun f3 ((p1 Int) (P1 Int)) Int
+	   ((Start Int (
+			p1
+			P1
+			(- Start Start)
+			(+ Start Start)
+                     )
+           )))
+
+(synth-fun f4 ((p1 Int) (P1 Int)) Int
+	   ((Start Int (
+			p1
+			P1
+			(- Start Start)
+			(+ Start Start)
+                     )
+           )))
+
+(synth-fun f5 ((p1 Int) (P1 Int)) Int
+	   ((Start Int (
+			p1
+			P1
+			(- Start Start)
+			(+ Start Start)
+                     )
+           )))
+
+(synth-fun g1 ((p1 Int) (P1 Int)) Int
+	   ((Start Int (
+			p1
+			P1
+			(- Start Start)
+			(+ Start Start)
+                     )
+           )))
+
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (+ (f1 x y) (f1 x y)) (f2 x y)))
+(constraint (= (- (+ (f1 x y) (f2 x y)) y) (f3 x y)))
+(constraint (= (+ (f2 x y) (f2 x y)) (f4 x y))) 
+(constraint (= (+ (f4 x y) (f1 x y)) (f5 x y))) 
+
+(constraint (= (- (f1 x y) y) (g1 x y)))
+
+
+(check-synth)
+
+;; possible solution
+;; f1: y+x+1
+;; f2: y+2x+2
+;; f3: y+3x+3
+;; f4: 4y+4x+4
+;; f5: 5y+5x+5
+;; g1: x+1
+;; g2: y+2
+;; g3: y+3
+;; g4: 2y+6
+;; g5: 3y+x+7
+
diff --git a/test/regress/regress2/sygus/vcb.sy b/test/regress/regress2/sygus/vcb.sy
new file mode 100644
index 000000000..9cc2389f3
--- /dev/null
+++ b/test/regress/regress2/sygus/vcb.sy
@@ -0,0 +1,54 @@
+(set-logic LIA)
+
+(synth-fun f1 ((x1 Int) (x2 Int)) Int)
+
+(synth-fun f2 ((x1 Int) (x2 Int)) Int)
+
+(define-fun vmin () Int 1)
+(define-fun vmax () Int 2)
+
+(define-fun AllZero ((v1 Int) (v2 Int)) Bool
+	    (and (= v1 0) (= v2 0)))
+
+(define-fun InV ((v1 Int) (v2 Int)) Bool
+	    (and (and (and (>= v1 vmin) (<= v1 vmax)) (>= v2 vmin)) (<= v2 vmax)))
+
+(define-fun InVorZero ((v1 Int) (v2 Int)) Bool
+	    (or (InV v1 v2) (AllZero v1 v2)))
+
+(define-fun UnsafeSame ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool
+	    (or (and (>= x1 x2) (>= (+ x2 v2) (+ x1 v1)))
+	    	(and (>= x2 x1) (>= (+ x1 v1) (+ x2 v2)))))
+
+(define-fun BadSame ((x1 Int) (x2 Int)) Bool
+	    (= x1 x2))
+
+(define-fun Bad ((x1 Int) (x2 Int)) Bool
+	    (BadSame x1 x2))
+
+(define-fun Unsafe ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool
+	    (UnsafeSame x1 x2 v1 v2))
+
+
+(declare-var x1 Int)
+(declare-var x2 Int)
+(declare-var v1 Int)
+(declare-var v2 Int)
+
+(constraint (InVorZero (f1 x1 x2) (f2 x1 x2)))
+
+(constraint (or (or (not (InV v1 v2))
+                    (AllZero (f1 x1 x2) (f2 x1 x2)))
+                (and (not (Unsafe x1 x2 (f1 x1 x2) (f2 x1 x2)))
+                     (not (AllZero (f1 (+ x1 (f1 x1 x2)) (+ x2 (f2 x1 x2)))
+                                   (f2 (+ x1 (f1 x1 x2)) (+ x2 (f2 x1 x2))))))))
+
+(constraint (or (or (or (not (InV v1 v2))
+	    	    	(Unsafe x1 x2 v1 v2))
+				   (AllZero (f1 (+ x1 v1) (+ x2 v2)) (f2 (+ x1 v1) (+ x2 v2))))
+                (not (AllZero (f1 x1 x2) (f2 x1 x2)))))
+
+
+(constraint (or (Bad x1 x2) (not (AllZero (f1 x1 x2) (f2 x1 x2)))))
+
+(check-synth)
\ No newline at end of file