test infrastructure updated for multiple-level regressions

diff --git a/Makefile b/Makefile
index 061f3d8d1e9cc59de3e2c366656b32c760dbd2f2..7e0e0261b1c650cf416a263c61c8ecbcc8833736 100644 (file)
--- 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 1ac8357f6adaa0ffb41f9a9997c58325cf500717..5b151441eb57308e59f597c741657417469a6e58 100644 (file)
--- 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 1c170dbe6a275a10ab0cf2145812b429cf75a7fe..159f32a4e8c9e55fe83c8f991e2297510a4b2988 100644 (file)
--- 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 fa1dcec3aaa55daa9cff50c418ee136df2ab3635..45659ae1ea6f9e16529005c5d876a2a4c7c35dfb 100644 (file)
--- 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 13f12edf7837965c3cf327d2a4277f49607421ee..575d07b77afbe7359120761f3f5a04d229ba097d 100644 (file)
--- 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 06fe0f1fbd898188c9fc7b0dad6b7881fa8f8940..663fc1407a66a9f7df7a041302afd65444b03154 100644 (file)
--- 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 819a892bd6831c97f2027b874b77722f42e6cf99..bec1fce3e6a207e252da4a85593f33065ecd6f1c 100644 (file)
--- 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 (file)
index 0000000..894759a
--- /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 (file)
index 0000000..b0caacf
--- /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 (file)
index 0000000..b720980
--- /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 (file)
index 0000000..a99ed3f
--- /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 (file)
index 0000000..5a9aa63
--- /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 (file)
index 0000000..72742f2
--- /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 (file)
index 0000000..2235473
--- /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 (file)
index 0000000..202bc55
--- /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 (executable)
index 0000000..4cf9f07
--- /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 c1dc3ef2ff791735954692368340bf067d8e5d39..2ca4091cb0c79b4253ab1ba3b9a5a637787ce7c8 100644 (file)
--- 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 5e9cca17a51fdc4e83df1d1566af9ea90ae681ba..2aba75e1cfd380ef9b9e53ed9a8f61cee734236d 100644 (file)
--- 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 b8a801378e20b32b3517a1cbc34b298b777d09fe..94a9d1d9e320fa22ed3228afd9f0533f404c241c 100644 (file)
--- 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 eeed1f3931cce3d6176610a2a42587f29dcff230..1908f909dbc9ea418716272e9e415ff18eb7ac79 100644 (file)
--- 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