From 3203c9bf8ec818b287c8b4030bb4b71d48ede9f1 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 4 Feb 2010 19:01:55 +0000
Subject: [PATCH] test infrastructure updated for multiple-level regressions

---
 Makefile                          |  4 +-
 Makefile.subdir                   |  4 +-
 configure.ac                      |  4 ++
 test/Makefile                     |  4 +-
 test/Makefile.am                  |  4 +-
 test/regress/Makefile             |  4 +-
 test/regress/Makefile.am          | 49 ++------------------
 test/regress/regress0/Makefile    |  8 ++++
 test/regress/regress0/Makefile.am | 10 ++++
 test/regress/regress1/Makefile    |  8 ++++
 test/regress/regress1/Makefile.am | 10 ++++
 test/regress/regress2/Makefile    |  8 ++++
 test/regress/regress2/Makefile.am | 10 ++++
 test/regress/regress3/Makefile    |  8 ++++
 test/regress/regress3/Makefile.am | 10 ++++
 test/regress/run_regression       | 77 +++++++++++++++++++++++++++++++
 test/system/Makefile              |  4 +-
 test/system/Makefile.am           |  4 +-
 test/unit/Makefile                |  4 +-
 test/unit/Makefile.am             |  4 +-
 20 files changed, 174 insertions(+), 64 deletions(-)
 create mode 100644 test/regress/regress0/Makefile
 create mode 100644 test/regress/regress0/Makefile.am
 create mode 100644 test/regress/regress1/Makefile
 create mode 100644 test/regress/regress1/Makefile.am
 create mode 100644 test/regress/regress2/Makefile
 create mode 100644 test/regress/regress2/Makefile.am
 create mode 100644 test/regress/regress3/Makefile
 create mode 100644 test/regress/regress3/Makefile.am
 create mode 100755 test/regress/run_regression

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
-- 
2.30.2