diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-01 12:25:11 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-01 12:25:11 +0200 |
| commit | 8f4e966ae0c0f42e595e1c603cb7c3f779b713ef (patch) | |
| tree | f3a46b20e752a2fb34e310ca477d4fb90bd7138e /test/regress/regress0/sygus | |
| parent | 91f40dee752910fca5d749656c0b6ee1bc1281aa (diff) | |
Support for default grammar for datatypes in sygus. Support vts for infinity.
Diffstat (limited to 'test/regress/regress0/sygus')
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 27 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/dt-no-syntax.sy | 12 |
2 files changed, 26 insertions, 13 deletions
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 82ff67d41..cf0f005b9 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -9,8 +9,8 @@ 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) + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) endif MAKEFLAGS = -k @@ -22,12 +22,12 @@ TESTS = commutative.sy \ constant.sy \ multi-fun-polynomial2.sy \ unbdd_inv_gen_winf1.sy \ - max.sy \ - array_sum_2_5.sy \ - parity-AIG-d0.sy \ - twolets1.sy \ - array_search_2.sy \ - hd-01-d1-prog.sy \ + max.sy \ + array_sum_2_5.sy \ + parity-AIG-d0.sy \ + twolets1.sy \ + array_search_2.sy \ + hd-01-d1-prog.sy \ icfp_28_10.sy \ const-var-test.sy \ no-syntax-test.sy \ @@ -44,23 +44,24 @@ TESTS = commutative.sy \ no-syntax-test-bool.sy \ inv-example.sy \ uminus_one.sy \ - sygus-dt.sy + sygus-dt.sy \ + dt-no-syntax.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ - max.smt2 \ - sygus-uf.sl + max.smt2 \ + sygus-uf.sl #if CVC4_BUILD_PROFILE_COMPETITION #else #TESTS += \ -# error.cvc +# error.cvc #endif # disabled tests, yet distribute #EXTRA_DIST += \ -# setofsets-disequal.smt2 +# setofsets-disequal.smt2 # synonyms for "check" .PHONY: regress regress0 test diff --git a/test/regress/regress0/sygus/dt-no-syntax.sy b/test/regress/regress0/sygus/dt-no-syntax.sy new file mode 100644 index 000000000..e0f8112ce --- /dev/null +++ b/test/regress/regress0/sygus/dt-no-syntax.sy @@ -0,0 +1,12 @@ +; COMMAND-LINE: --cegqi --no-dump-synth +; EXPECT: unsat +(set-logic LIA) + +(declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) + +(synth-fun f ((x Int)) List) + +(declare-var x Int) + +(constraint (= (f x) (cons (+ x 1) nil))) +(check-synth) |