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

4 files changed, 181 insertions, 0 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 52eb63789..5cb24d072 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1475,6 +1475,7 @@ REG1_TESTS = \
 	regress1/sygus/commutative.sy \
 	regress1/sygus/constant.sy \
 	regress1/sygus/constant-ite-bv.sy \
+	regress1/sygus/crci-ssb-unk.sy \
 	regress1/sygus/dt-test-ns.sy \
 	regress1/sygus/dup-op.sy \
 	regress1/sygus/fg_polynomial3.sy \
@@ -1598,7 +1599,9 @@ REG2_TESTS = \
 	regress2/sygus/process-10-vars-2fun.sy \
 	regress2/sygus/process-arg-invariance.sy \
 	regress2/sygus/real-grammar-neg.sy \
+	regress2/sygus/sixfuncs.sy \
 	regress2/sygus/three.sy \
+	regress2/sygus/vcb.sy \
 	regress2/typed_v1l50016-simp.cvc \
 	regress2/uflia-error0.smt2 \
 	regress2/xs-09-16-3-4-1-5.decn.smt \
diff --git a/test/regress/regress1/sygus/crci-ssb-unk.sy b/test/regress/regress1/sygus/crci-ssb-unk.sy
new file mode 100644
index 000000000..f2b28db9c
--- /dev/null
+++ b/test/regress/regress1/sygus/crci-ssb-unk.sy
@@ -0,0 +1,43 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic BV)
+
+
+(define-fun origCir ( (LN4 Bool) (LN91 Bool)  )  Bool    
+          (and  LN91 LN4 )
+)
+
+
+(synth-fun skel ( (LN4 Bool) (LN91 Bool)  )  Bool    
+          ((Start Bool (
+                                  (and depth1 depth1)
+                                  (xor depth1 depth1)
+          ))
+          (depth1 Bool (
+                                  (not depth2)
+                                  LN91
+          ))
+          (depth2 Bool (
+                                  (and depth3 depth3)
+                                  (not depth3)
+                                  (or depth3 depth3)
+          ))
+          (depth3 Bool (
+                                  (and depth4 depth4)
+                                  (not depth4)
+                                  (or depth4 depth4)
+                                  (xor depth4 depth4)
+          ))
+          (depth4 Bool (
+                                  LN4
+          )))
+)
+
+
+(declare-var LN4 Bool)
+(declare-var LN91 Bool)
+
+(constraint (= (origCir LN4 LN91 ) (skel LN4 LN91 )))
+
+(check-synth)
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