Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.

1 files changed, 60 insertions, 0 deletions

diff --git a/test/regress/regress1/sygus/VC22_a.sy b/test/regress/regress1/sygus/VC22_a.sy
new file mode 100644
index 000000000..75bed6a28
--- /dev/null
+++ b/test/regress/regress1/sygus/VC22_a.sy
@@ -0,0 +1,60 @@
+; EXPECT: unsat
+; COMMAND-LINE: --no-dump-synth
+(set-logic LIA)
+
+(synth-fun f ((x1 Int) (x2 Int)) Int
+	((Start Int (0 1 x1 x2
+				(ite StartBool Start Start)))
+		(StartBool Bool ((= Start Start)))))
+
+(define-fun vmin () Int 1)
+(define-fun vmax () Int 2)
+
+(define-fun Zero ((v Int)) Bool
+	(= v 0))
+
+(define-fun InV1 ((v Int)) Bool
+	(and (>= v vmin) (<= v vmax)))
+
+(define-fun InV2 ((v1 Int) (v2 Int)) Bool
+	(and (and (and (>= v1 vmin) (<= v1 vmax))
+			(>= v2 vmin)) (<= v2 vmax)))
+
+(define-fun InVorZero ((v Int)) Bool
+	(or (InV1 v) (Zero v)))
+
+
+(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 Unsafe ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool
+	(UnsafeSame x1 x2 v1 v2))
+
+(define-fun BadSame ((x1 Int) (x2 Int)) Bool
+	(= x1 x2))
+
+(define-fun Bad ((x1 Int) (x2 Int)) Bool
+	(BadSame x1 x2))
+
+(declare-var x1 Int)
+(declare-var x2 Int)
+(declare-var v1 Int)
+(declare-var v2 Int)
+
+(constraint (InVorZero (f x1 x2)))
+
+(constraint (or (or (not (InV2 v1 v2))
+			(Zero (f x1 x2)))
+		(and (not (Unsafe x1 x2 (f x1 x2) (f x1 x2)))
+			(not (Zero (f (+ x1 (f x1 x2)) (+ x2 (f x1 x2))))))))
+
+(constraint (or (or (not (InV2 v1 v2))
+			(or (Unsafe x1 x2 v1 v2)
+				(Zero (f (+ x1 v1) (+ x2 v2)))))
+		(not (Zero (f x1 x2)))))
+
+(constraint (or (Bad x1 x2) (not (Zero (f x1 x2)))))
+
+(check-synth)
+