diff options
author | Tim King <taking@google.com> | 2017-01-10 17:51:14 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2017-01-10 18:21:15 -0800 |
commit | 1e7807069e07a710bafa83fc7412c3ac164249b8 (patch) | |
tree | 3301a132c17645a33abe8e5bb331fa3d721af33d /test/regress/regress0/expect | |
parent | ff498bb43b3d3785bdb894974678e65926de62ab (diff) |
Adding regression test scrubbing.
Diffstat (limited to 'test/regress/regress0/expect')
-rw-r--r-- | test/regress/regress0/expect/Makefile.am | 44 | ||||
-rw-r--r-- | test/regress/regress0/expect/README | 1 | ||||
-rw-r--r-- | test/regress/regress0/expect/scrub.01.smt | 7 | ||||
-rw-r--r-- | test/regress/regress0/expect/scrub.01.smt.expect | 6 | ||||
-rw-r--r-- | test/regress/regress0/expect/scrub.02.smt | 13 | ||||
-rw-r--r-- | test/regress/regress0/expect/scrub.03.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/expect/scrub.03.smt2.expect | 6 | ||||
-rw-r--r-- | test/regress/regress0/expect/scrub.04.smt2 | 15 | ||||
-rw-r--r-- | test/regress/regress0/expect/scrub.06.cvc | 9 | ||||
-rw-r--r-- | test/regress/regress0/expect/scrub.07.sy | 7 | ||||
-rw-r--r-- | test/regress/regress0/expect/scrub.07.sy.expect | 6 | ||||
-rw-r--r-- | test/regress/regress0/expect/scrub.08.sy | 13 | ||||
-rw-r--r-- | test/regress/regress0/expect/scrub.09.p | 11 |
13 files changed, 147 insertions, 0 deletions
diff --git a/test/regress/regress0/expect/Makefile.am b/test/regress/regress0/expect/Makefile.am new file mode 100644 index 000000000..e1518d84d --- /dev/null +++ b/test/regress/regress0/expect/Makefile.am @@ -0,0 +1,44 @@ +SUBDIRS = . + +# 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) @abs_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 = \ + scrub.01.smt \ + scrub.02.smt \ + scrub.03.smt2 \ + scrub.04.smt2 \ + scrub.06.cvc \ + scrub.07.sy \ + scrub.08.sy \ + scrub.09.p + +EXTRA_DIST = $(TESTS) \ + scrub.01.smt.expect \ + scrub.03.smt2.expect \ + scrub.07.sy.expect + +# synonyms for "check" in this directory +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/expect/README b/test/regress/regress0/expect/README new file mode 100644 index 000000000..756982408 --- /dev/null +++ b/test/regress/regress0/expect/README @@ -0,0 +1 @@ +This directory contains integration tests for the test/regress/run_regression script.
\ No newline at end of file diff --git a/test/regress/regress0/expect/scrub.01.smt b/test/regress/regress0/expect/scrub.01.smt new file mode 100644 index 000000000..592a3501f --- /dev/null +++ b/test/regress/regress0/expect/scrub.01.smt @@ -0,0 +1,7 @@ +(benchmark reject_nonlinear +:logic QF_LRA +:extrafuns ((n Real)) +:status unknown +:formula +(= (/ n n) 1) +) diff --git a/test/regress/regress0/expect/scrub.01.smt.expect b/test/regress/regress0/expect/scrub.01.smt.expect new file mode 100644 index 000000000..b21f2d965 --- /dev/null +++ b/test/regress/regress0/expect/scrub.01.smt.expect @@ -0,0 +1,6 @@ +% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' +% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) +% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: The fact in question: TERM +% EXPECT: ") +% EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.02.smt b/test/regress/regress0/expect/scrub.02.smt new file mode 100644 index 000000000..f2e6554b7 --- /dev/null +++ b/test/regress/regress0/expect/scrub.02.smt @@ -0,0 +1,13 @@ +% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' +% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) +% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: The fact in question: TERM +% EXPECT: ") +% EXIT: 1 +(benchmark reject_nonlinear +:logic QF_LRA +:extrafuns ((n Real)) +:status unknown +:formula +(= (/ n n) 1) +) diff --git a/test/regress/regress0/expect/scrub.03.smt2 b/test/regress/regress0/expect/scrub.03.smt2 new file mode 100644 index 000000000..a5a2c9be1 --- /dev/null +++ b/test/regress/regress0/expect/scrub.03.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_LRA) +(set-info :status unknown) +(declare-fun n () Real) + +; This example is test that LRA rejects multiplication terms + +(assert (= (/ n n) 1)) + +(check-sat) diff --git a/test/regress/regress0/expect/scrub.03.smt2.expect b/test/regress/regress0/expect/scrub.03.smt2.expect new file mode 100644 index 000000000..b21f2d965 --- /dev/null +++ b/test/regress/regress0/expect/scrub.03.smt2.expect @@ -0,0 +1,6 @@ +% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' +% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) +% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: The fact in question: TERM +% EXPECT: ") +% EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.04.smt2 b/test/regress/regress0/expect/scrub.04.smt2 new file mode 100644 index 000000000..e457734eb --- /dev/null +++ b/test/regress/regress0/expect/scrub.04.smt2 @@ -0,0 +1,15 @@ +; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' +; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) +; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +; EXPECT: The fact in question: TERM +; EXPECT: ") +; EXIT: 1 +(set-logic QF_LRA) +(set-info :status unknown) +(declare-fun n () Real) + +; This example is test that LRA rejects multiplication terms + +(assert (= (/ n n) 1)) + +(check-sat) diff --git a/test/regress/regress0/expect/scrub.06.cvc b/test/regress/regress0/expect/scrub.06.cvc new file mode 100644 index 000000000..b9cb1cd8a --- /dev/null +++ b/test/regress/regress0/expect/scrub.06.cvc @@ -0,0 +1,9 @@ +% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -e '/^$/d' +% EXPECT: A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM +% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: The fact in question: TERM +% EXIT: 1 + +n : REAL; + +QUERY (n/n) = 1;
\ No newline at end of file diff --git a/test/regress/regress0/expect/scrub.07.sy b/test/regress/regress0/expect/scrub.07.sy new file mode 100644 index 000000000..cf0e37c9f --- /dev/null +++ b/test/regress/regress0/expect/scrub.07.sy @@ -0,0 +1,7 @@ +; COMMAND-LINE: --cegqi-si=all --no-dump-synth +(set-logic LIA) +(declare-var n Int) + +(synth-fun f ((n Int)) Int) +(constraint (= (/ n n) 1)) +(check-synth) diff --git a/test/regress/regress0/expect/scrub.07.sy.expect b/test/regress/regress0/expect/scrub.07.sy.expect new file mode 100644 index 000000000..dfcd45a8a --- /dev/null +++ b/test/regress/regress0/expect/scrub.07.sy.expect @@ -0,0 +1,6 @@ +% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' +% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM +% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: The fact in question: TERM +% EXPECT: ") +% EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy new file mode 100644 index 000000000..3b9574cdf --- /dev/null +++ b/test/regress/regress0/expect/scrub.08.sy @@ -0,0 +1,13 @@ +; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' +; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM +; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +; EXPECT: The fact in question: TERM +; EXPECT: ") +; EXIT: 1 +(set-logic LIA) +(declare-var n Int) + +(synth-fun f ((n Int)) Int) +(constraint (= (/ n n) 1)) +(check-synth)
\ No newline at end of file diff --git a/test/regress/regress0/expect/scrub.09.p b/test/regress/regress0/expect/scrub.09.p new file mode 100644 index 000000000..17eef44fe --- /dev/null +++ b/test/regress/regress0/expect/scrub.09.p @@ -0,0 +1,11 @@ +% COMMAND-LINE: --cegqi-si=all --no-dump-synth +% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' +% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM +% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: The fact in question: TERM +% EXPECT: ") +% EXIT: 1 +tff(reject_division,conjecture, + ! [X: $int] : + ( $quotient(X,X) = 1 ) + ). |