summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile4
-rw-r--r--Makefile.subdir4
-rw-r--r--configure.ac4
-rw-r--r--test/Makefile4
-rw-r--r--test/Makefile.am4
-rw-r--r--test/regress/Makefile4
-rw-r--r--test/regress/Makefile.am49
-rw-r--r--test/regress/regress0/Makefile8
-rw-r--r--test/regress/regress0/Makefile.am10
-rw-r--r--test/regress/regress1/Makefile8
-rw-r--r--test/regress/regress1/Makefile.am10
-rw-r--r--test/regress/regress2/Makefile8
-rw-r--r--test/regress/regress2/Makefile.am10
-rw-r--r--test/regress/regress3/Makefile8
-rw-r--r--test/regress/regress3/Makefile.am10
-rwxr-xr-xtest/regress/run_regression77
-rw-r--r--test/system/Makefile4
-rw-r--r--test/system/Makefile.am4
-rw-r--r--test/unit/Makefile4
-rw-r--r--test/unit/Makefile.am4
20 files changed, 174 insertions, 64 deletions
diff --git a/Makefile b/Makefile
index 061f3d8d1..7e0e0261b 100644
--- a/Makefile
+++ b/Makefile
@@ -15,5 +15,5 @@ all %:
fi
# synonyms for "check"
-.PHONY: regress regress0 regress1 regress2 regress3 test
-regress regress0 regress1 regress2 regress3 test: check
+.PHONY: regress test
+regress test: check
diff --git a/Makefile.subdir b/Makefile.subdir
index 1ac8357f6..5b151441e 100644
--- a/Makefile.subdir
+++ b/Makefile.subdir
@@ -33,5 +33,5 @@ check:
fi
# synonyms for "check"
-.PHONY: regress regress0 regress1 regress2 regress3 test
-regress regress0 regress1 regress2 regress3 test: check
+.PHONY: regress test
+regress test: check
diff --git a/configure.ac b/configure.ac
index 1c170dbe6..159f32a4e 100644
--- a/configure.ac
+++ b/configure.ac
@@ -443,6 +443,10 @@ AC_CONFIG_FILES([
src/theory/arith/Makefile
test/Makefile
test/regress/Makefile
+ test/regress/regress0/Makefile
+ test/regress/regress1/Makefile
+ test/regress/regress2/Makefile
+ test/regress/regress3/Makefile
test/system/Makefile
test/unit/Makefile
])
diff --git a/test/Makefile b/test/Makefile
index fa1dcec3a..45659ae1e 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -4,5 +4,5 @@ srcdir = test
include $(topdir)/Makefile.subdir
# synonyms for "check"
-.PHONY: regress regress0 regress1 regress2 regress3 test
-regress regress0 regress1 regress2 regress3 test: check
+.PHONY: regress test
+regress test: check
diff --git a/test/Makefile.am b/test/Makefile.am
index 13f12edf7..575d07b77 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -1,5 +1,5 @@
SUBDIRS = unit system regress
# synonyms for "check"
-.PHONY: regress regress0 regress1 regress2 regress3 test
-regress regress0 regress1 regress2 regress3 test: check
+.PHONY: regress test
+regress test: check
diff --git a/test/regress/Makefile b/test/regress/Makefile
index 06fe0f1fb..663fc1407 100644
--- a/test/regress/Makefile
+++ b/test/regress/Makefile
@@ -4,5 +4,5 @@ srcdir = test/regress
include $(topdir)/Makefile.subdir
# synonyms for "check"
-.PHONY: regress regress0 regress1 regress2 regress3 test
-regress regress0 regress1 regress2 regress3 test: check
+.PHONY: test
+test: check
diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am
index 819a892bd..bec1fce3e 100644
--- a/test/regress/Makefile.am
+++ b/test/regress/Makefile.am
@@ -1,48 +1,5 @@
-TESTS_ENVIRONMENT = @top_builddir@/../../bin/cvc4
-TESTS = \
- simple.cvc \
- simple.smt \
- hole6.cvc \
- hole7.cvc \
- hole8.cvc \
- hole9.cvc \
- hole10.cvc \
- wiki.cvc \
- test9.cvc \
- test11.cvc \
- bmc-ibm-1.smt \
- bmc-ibm-2.smt \
- bmc-ibm-3.smt \
- bmc-ibm-4.smt \
- bmc-ibm-5.smt \
- uf20-03.cvc \
- qwh.35.405.shuffled-as.sat03-1651.smt \
- C880mul.miter.shuffled-as.sat03-348.smt \
- instance_1151.smt \
- instance_1444.smt
-
-#Tests that currently do not work
-FUTURETESTS = \
- logops.cvc \
- test12.cvc \
- bug1.cvc \
- boolean.cvc
-
-#Tests that take too long to be put in the default regress level
-#TODO Make multiple regression levels. Some of which are off by default.
-LONGTESTS = \
- friedman_n4_i5.smt \
- friedman_n6_i4.smt \
- bmc-galileo-8.smt \
- bmc-galileo-9.smt \
- bmc-ibm-6.smt \
- bmc-ibm-7.smt \
- bmc-ibm-10.smt \
- bmc-ibm-11.smt \
- bmc-ibm-12.smt \
- bmc-ibm-13.smt \
- comb2.shuffled-as.sat03-420.smt
+SUBDIRS = regress0 regress1 regress2 regress3
# synonyms for "check"
-.PHONY: regress regress0 regress1 regress2 regress3 test
-regress regress0 regress1 regress2 regress3 test: check
+.PHONY: regress test
+regress test: check
diff --git a/test/regress/regress0/Makefile b/test/regress/regress0/Makefile
new file mode 100644
index 000000000..894759aa3
--- /dev/null
+++ b/test/regress/regress0/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../..
+srcdir = test/regress/regress0
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
new file mode 100644
index 000000000..b0caacf1b
--- /dev/null
+++ b/test/regress/regress0/Makefile.am
@@ -0,0 +1,10 @@
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
+TESTS =
+
+# 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/regress1/Makefile b/test/regress/regress1/Makefile
new file mode 100644
index 000000000..b720980f1
--- /dev/null
+++ b/test/regress/regress1/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../..
+srcdir = test/regress/regress1
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
new file mode 100644
index 000000000..a99ed3f70
--- /dev/null
+++ b/test/regress/regress1/Makefile.am
@@ -0,0 +1,10 @@
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
+TESTS =
+
+# synonyms for "check"
+.PHONY: regress regress1 test
+regress regress1 test: check
+
+# do nothing in this subdir
+.PHONY: regress0 regress2 regress3
+regress0 regress2 regress3:
diff --git a/test/regress/regress2/Makefile b/test/regress/regress2/Makefile
new file mode 100644
index 000000000..5a9aa63be
--- /dev/null
+++ b/test/regress/regress2/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../..
+srcdir = test/regress/regress2
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am
new file mode 100644
index 000000000..72742f201
--- /dev/null
+++ b/test/regress/regress2/Makefile.am
@@ -0,0 +1,10 @@
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
+TESTS =
+
+# synonyms for "check"
+.PHONY: regress regress2 test
+regress regress2 test: check
+
+# do nothing in this subdir
+.PHONY: regress0 regress1 regress3
+regress0 regress1 regress3:
diff --git a/test/regress/regress3/Makefile b/test/regress/regress3/Makefile
new file mode 100644
index 000000000..223547305
--- /dev/null
+++ b/test/regress/regress3/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../..
+srcdir = test/regress/regress3
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am
new file mode 100644
index 000000000..202bc553f
--- /dev/null
+++ b/test/regress/regress3/Makefile.am
@@ -0,0 +1,10 @@
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
+TESTS =
+
+# synonyms for "check"
+.PHONY: regress regress3 test
+regress regress3 test: check
+
+# do nothing in this subdir
+.PHONY: regress0 regress1 regress2
+regress0 regress1 regress2:
diff --git a/test/regress/run_regression b/test/regress/run_regression
new file mode 100755
index 000000000..4cf9f07cf
--- /dev/null
+++ b/test/regress/run_regression
@@ -0,0 +1,77 @@
+#!/bin/bash
+#
+# Morgan Deters <mdeters@cs.nyu.edu>
+# for the CVC4 project
+#
+# usage:
+#
+# run_regression cvc4-binary [ benchmark.cvc | benchmark.smt ]
+#
+# Runs benchmark and checks for correct exit status and output.
+#
+
+prog=`basename "$0"`
+
+if [ $# != 2 ]; then
+ echo "usage: $prog cvc4-binary [ benchmark.cvc | benchmark.smt ]" >&2
+ exit 1
+fi
+
+cvc4=$1
+benchmark=$2
+
+function error {
+ echo "$prog: error: $*"
+ exit 1
+}
+
+if ! [ -x "$cvc4" ]; then
+ error "\`$cvc4' doesn't exist or isn't executable" >&2
+fi
+if ! [ -r "$benchmark" ]; then
+ error "\`$benchmark' doesn't exist or isn't readable" >&2
+fi
+
+if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
+ if grep '^ *:status *sat' &>/dev/null; then
+ expected_output=sat
+ expected_exit_status=10
+ elif grep '^ *:status *unsat' &>/dev/null; then
+ expected_output=unsat
+ expected_exit_status=20
+ else
+ error "cannot determine status of \`$benchmark'"
+ fi
+elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
+ expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
+ if [ -z "$expected_output" ]; then
+ error "cannot determine status of \`$benchmark'"
+ fi
+ expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'`
+else
+ error "benchmark \`$benchmark' must be *.cvc or *.smt"
+fi
+
+expfile=`mktemp -t cvc4test.exp.XXXXXXXXXX`
+outfile=`mktemp -t cvc4test.out.XXXXXXXXXX`
+echo "$expected_output" >"$expfile"
+
+echo "$cvc4" --segv-nospin "$benchmark"
+"$cvc4" --segv-nospin "$benchmark" | tee "$outfile"
+exit_status=$?
+
+diffs=`diff -u "$expfile" "$outfile"`
+rm -f "$expfile"
+rm -f "$outfile"
+if [ $? -ne 0 ]; then
+ echo "$prog: error: differences between expected and actual output"
+ echo "$diffs"
+ exit 1
+fi
+
+if [ -n "$expected_exit_status" ]; then
+ if [ $exit_status != "$expected_exit_status" ]; then
+ error "expected exit status \`$expected_exit_status' but got \`$exit_status'"
+ fi
+fi
+
diff --git a/test/system/Makefile b/test/system/Makefile
index c1dc3ef2f..2ca4091cb 100644
--- a/test/system/Makefile
+++ b/test/system/Makefile
@@ -4,5 +4,5 @@ srcdir = test/system
include $(topdir)/Makefile.subdir
# synonyms for "check"
-.PHONY: regress regress0 regress1 regress2 regress3 test
-regress regress0 regress1 regress2 regress3 test: check
+.PHONY: regress test
+regress test: check
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 5e9cca17a..2aba75e1c 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -26,5 +26,5 @@ EXTRA_DIST = \
$(TESTS):: $(TEST_DEPS)
# synonyms for "check"
-.PHONY: regress regress0 regress1 regress2 regress3 test
-regress regress0 regress1 regress2 regress3 test: check
+.PHONY: regress test
+regress test: check
diff --git a/test/unit/Makefile b/test/unit/Makefile
index b8a801378..94a9d1d9e 100644
--- a/test/unit/Makefile
+++ b/test/unit/Makefile
@@ -4,5 +4,5 @@ srcdir = test/unit
include $(topdir)/Makefile.subdir
# synonyms for "check"
-.PHONY: regress regress0 regress1 regress2 regress3 test
-regress regress0 regress1 regress2 regress3 test: check
+.PHONY: regress test
+regress test: check
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index eeed1f393..1908f909d 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -84,5 +84,5 @@ EXTRA_DIST = \
endif
# synonyms for "check"
-.PHONY: regress regress0 regress1 regress2 regress3 test
-regress regress0 regress1 regress2 regress3 test: check
+.PHONY: regress test
+regress test: check
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback