test infrastructure updated for multiple-level regressions

11 files changed, 154 insertions, 48 deletions

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
+