diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-23 20:58:08 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2015-01-14 06:33:49 -0500 |
commit | 0042f301908763cf1edb8a2d56b3f373a0055908 (patch) | |
tree | 4f2a66c39bf5511c3f00dca9f4d1bc475435359a /test | |
parent | ba1ae20edf3f4b2321a05b39cb218940e926d436 (diff) |
sygus input language and benchmark
Diffstat (limited to 'test')
-rw-r--r-- | test/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/parser/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/parser/constraint.smt2 | 5 | ||||
-rw-r--r-- | test/regress/regress0/sygus/Makefile | 8 | ||||
-rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 45 | ||||
-rw-r--r-- | test/regress/regress0/sygus/max.sl | 32 | ||||
-rw-r--r-- | test/regress/regress0/sygus/max.smt2 | 52 | ||||
-rw-r--r-- | test/regress/regress0/sygus/sygus-uf.sl | 20 | ||||
-rwxr-xr-x | test/regress/run_regression | 23 |
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" |