Adding regression test scrubbing.

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 )
+    ).