sygus input language and benchmark

5 files changed, 157 insertions, 0 deletions

diff --git a/test/regress/regress0/sygus/Makefile b/test/regress/regress0/sygus/Makefile
new file mode 100644
index 000000000..cc09c6091
--- /dev/null
+++ b/test/regress/regress0/sygus/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/sygus
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
new file mode 100644
index 000000000..ad1296af0
--- /dev/null
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -0,0 +1,45 @@
+# don't override a BINARY imported from a personal.mk
+@mk_if@eq ($(BINARY),)
+@mk_empty@BINARY = cvc4
+end@mk_if@
+
+LOG_COMPILER = @srcdir@/../../run_regression
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
+
+if AUTOMAKE_1_11
+# old-style (pre-automake 1.12) test harness
+TESTS_ENVIRONMENT = \
+	$(LOG_COMPILER) \
+	$(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =
+
+# sygus tests currently taking too long for make regress
+EXTRA_DIST = $(TESTS) \
+	max.sl \
+	max.smt2 \
+	sygus-uf.sl
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#	error.cvc
+#endif
+
+# disabled tests, yet distribute
+#EXTRA_DIST += \
+#	setofsets-disequal.smt2
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/sygus/max.sl b/test/regress/regress0/sygus/max.sl
new file mode 100644
index 000000000..aea8e8186
--- /dev/null
+++ b/test/regress/regress0/sygus/max.sl
@@ -0,0 +1,32 @@
+; EXPECT: unsat
+(set-logic LIA)
+
+(synth-fun max ((x Int) (y Int)) Int
+  ((Start Int (0 1 x y
+               (+ Start Start)
+               (- Start Start)
+               (ite StartBool Start Start)))
+   (StartBool Bool ((and StartBool StartBool)
+                    (not StartBool)
+                    (<= Start Start)))))
+
+;(synth-fun min ((x Int) (y Int)) Int
+;  ((Start Int ((Constant Int) (Variable Int)
+;               (+ Start Start)
+;               (- Start Start)
+;               (ite StartBool Start Start)))
+;   (StartBool Bool ((and StartBool StartBool)
+;                    (not StartBool)
+;                    (<= Start Start)))))
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (>= (max x y) x))
+(constraint (>= (max x y) y))
+(constraint (or (= x (max x y))
+                (= y (max x y))))
+;(constraint (= (+ (max x y) (min x y))
+;               (+ x y)))
+
+(check-synth)
diff --git a/test/regress/regress0/sygus/max.smt2 b/test/regress/regress0/sygus/max.smt2
new file mode 100644
index 000000000..97c223e16
--- /dev/null
+++ b/test/regress/regress0/sygus/max.smt2
@@ -0,0 +1,52 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic UFDTLIA)
+
+(declare-datatypes () ((start (startx)
+                              (starty)
+                              (start1)
+                              (start0)
+                              (startplus (startplus1 start) (startplus2 start))
+                              (startminus (startminus1 start) (startminus2 start))
+                              (startite (startite1 startbool) (startite2 start) (startite3 start)))
+                       (startbool (startand (startand1 startbool) (startand2 startbool))
+                                  (startor (startor1 startbool) (startor2 startbool))
+                                  (startnot (startnot1 startbool))
+                                  (startleq (startleq1 start) (startleq2 start))
+                                  (starteq (starteq1 start) (starteq2 start))
+                                  (startgeq (startgeq1 start) (startgeq2 start))
+                                  )))
+
+(declare-fun eval (start Int Int) Int)
+(declare-fun evalbool (startbool Int Int) Bool)
+
+(assert (forall ((x Int) (y Int)) (! (= (eval startx x y) x) :pattern ((eval startx x y)))))
+(assert (forall ((x Int) (y Int)) (! (= (eval starty x y) y) :pattern ((eval starty x y)))))
+(assert (forall ((x Int) (y Int)) (! (= (eval start0 x y) 0) :pattern ((eval start0 x y)))))
+(assert (forall ((x Int) (y Int)) (! (= (eval start1 x y) 1) :pattern ((eval start1 x y)))))
+(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (eval (startplus s1 s2) x y) (+ (eval s1 x y) (eval s2 x y))) :pattern ((eval (startplus s1 s2) x y)))))
+(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (eval (startminus s1 s2) x y) (- (eval s1 x y) (eval s2 x y))) :pattern ((eval (startminus s1 s2) x y)))))
+(assert (forall ((s1 startbool) (s2 start) (s3 start) (x Int) (y Int)) (! (= (eval (startite s1 s2 s3) x y) (ite (evalbool s1 x y) (eval s2 x y) (eval s3 x y)))
+                                                                          :pattern ((eval (startite s1 s2 s3) x y)))))
+
+(assert (forall ((s1 startbool) (s2 startbool) (x Int) (y Int)) (! (= (evalbool (startand s1 s2) x y) (and (evalbool s1 x y) (evalbool s2 x y)))
+                                                                   :pattern ((evalbool (startand s1 s2) x y)))))
+(assert (forall ((s1 startbool) (s2 startbool) (x Int) (y Int)) (! (= (evalbool (startor s1 s2) x y) (or (evalbool s1 x y) (evalbool s2 x y)))
+                                                                   :pattern ((evalbool (startor s1 s2) x y)))))
+(assert (forall ((s1 startbool) (x Int) (y Int)) (! (= (evalbool (startnot s1) x y) (not (evalbool s1 x y)))
+                                                    :pattern ((evalbool (startnot s1) x y)))))
+(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (evalbool (startleq s1 s2) x y) (<= (eval s1 x y) (eval s2 x y)))
+                                                           :pattern ((evalbool (startleq s1 s2) x y)))))
+(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (evalbool (starteq s1 s2) x y) (= (eval s1 x y) (eval s2 x y)))
+                                                           :pattern ((evalbool (starteq s1 s2) x y)))))
+(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (evalbool (startgeq s1 s2) x y) (>= (eval s1 x y) (eval s2 x y)))
+                                                           :pattern ((evalbool (startgeq s1 s2) x y)))))
+
+
+(define-fun P ((fmax start) (x Int) (y Int)) Bool (and (>= (eval fmax x y) x) (>= (eval fmax x y) y) (or (= (eval fmax x y) x) (= (eval fmax x y) y))))
+
+(assert (forall ((fmax start)) (! (exists ((x Int) (y Int)) (not (P fmax x y))) :sygus)))
+
+
+(check-sat)
diff --git a/test/regress/regress0/sygus/sygus-uf.sl b/test/regress/regress0/sygus/sygus-uf.sl
new file mode 100644
index 000000000..95cd8771e
--- /dev/null
+++ b/test/regress/regress0/sygus/sygus-uf.sl
@@ -0,0 +1,20 @@
+(set-logic LIA)
+
+(declare-fun uf (Int) Int)
+
+(synth-fun f ((x Int) (y Int)) Bool
+  ((Start Bool (true false
+                (<= IntExpr IntExpr)
+                (= IntExpr IntExpr)
+                (and Start Start)
+                (or Start Start)
+                (not Start)))
+   (IntExpr Int (0 1 x y
+                 (+ IntExpr IntExpr)
+                 (- IntExpr IntExpr)))))
+
+(declare-var x Int)
+
+(constraint (f (uf x) (uf x)))
+
+(check-synth)