sygus input language and benchmark

10 files changed, 188 insertions, 3 deletions

diff --git a/test/Makefile.am b/test/Makefile.am
index 236443eb9..dcb58b591 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -58,6 +58,7 @@ subdirs_to_check = \
 	regress/regress0/strings \
 	regress/regress0/sets \
 	regress/regress0/parser \
+	regress/regress0/sygus \
 	regress/regress1 \
 	regress/regress1/arith \
 	regress/regress2 \
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 68d002367..128072f24 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,5 +1,5 @@
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser
-DIST_SUBDIRS = $(SUBDIRS) #. arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser sygus
+DIST_SUBDIRS = $(SUBDIRS)
 
 # don't override a BINARY imported from a personal.mk
 @mk_if@eq ($(BINARY),)
diff --git a/test/regress/regress0/parser/Makefile.am b/test/regress/regress0/parser/Makefile.am
index eb27e797b..44318d492 100644
--- a/test/regress/regress0/parser/Makefile.am
+++ b/test/regress/regress0/parser/Makefile.am
@@ -20,6 +20,7 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 TESTS =	\
 	declarefun-emptyset-uf.smt2 \
+	constraint.smt2 \
 	strings20.smt2 \
 	strings25.smt2
 
diff --git a/test/regress/regress0/parser/constraint.smt2 b/test/regress/regress0/parser/constraint.smt2
new file mode 100644
index 000000000..ffd56625e
--- /dev/null
+++ b/test/regress/regress0/parser/constraint.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_UF)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-fun Constraint () U)
+(check-sat)
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)
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 062458055..7b215dc2a 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -179,8 +179,29 @@ elif expr "$benchmark" : '.*\.p$' &>/dev/null; then
   if grep -q '^% COMMAND-LINE: ' "$benchmark"; then
     command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
   fi
+elif expr "$benchmark" : '.*\.sy$' &>/dev/null; then
+  lang=sygus
+  if test -e "$benchmark.expect"; then
+    expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
+    expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
+    expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
+    command_line=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'`
+    if [ -z "$expected_exit_status" ]; then
+      expected_exit_status=0
+    fi
+  elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then
+    expected_output=`grep '^; EXPECT: ' "$benchmark" | sed 's,^; EXPECT: ,,'`
+    expected_error=`grep '^; EXPECT-ERROR: ' "$benchmark" | sed 's,^; EXPECT-ERROR: ,,'`
+    expected_exit_status=`grep -m 1 '^; EXIT: ' "$benchmark" | perl -pe 's,^; EXIT: ,,;s,\r,,'`
+    command_line=`grep '^; COMMAND-LINE: ' "$benchmark" | sed 's,^; COMMAND-LINE: ,,'`
+    if [ -z "$expected_exit_status" ]; then
+      expected_exit_status=0
+    fi
+  else
+    error "cannot determine expected output of \`$benchmark'"
+  fi
 else
-  error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2 or *.p"
+  error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2 or *.p or *.sy"
 fi
 
 command_line="${command_line:+$command_line }--lang=$lang"