build system for multi-level regressions

11 files changed, 87 insertions, 6 deletions

diff --git a/Makefile.am b/Makefile.am
index 20d6298f4..bade9cd15 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -16,3 +16,7 @@ production debug default competition:
 	else \
 		./configure --with-build=$@ $(CONFARGS) && $(MAKE); \
 	fi
+
+.PHONY: regress0 regress1 regress2 regress3
+regress0 regress1 regress2 regress3:
+	(cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1
diff --git a/Makefile.subdir b/Makefile.subdir
index 5b151441e..9eec964e0 100644
--- a/Makefile.subdir
+++ b/Makefile.subdir
@@ -19,6 +19,21 @@ all %:
 	fi
 
 .PHONY: check
+ifeq ($(srcdir:test/%=test),test)
+# under the test/ directory, additional subtargets
+.PHONY: regress0 regress1 regress2 regress3
+check regress0 regress1 regress2 regress3:
+	@if test -e $(builddir); then \
+		echo cd $(builddir); \
+		cd $(builddir); \
+		echo $(MAKE) $@; \
+		$(MAKE) $@; \
+	else \
+		echo; \
+		echo "** ERROR: could not find testing dir \`$(builddir)'"; \
+		echo; \
+	fi
+else
 check:
 	@if test -e $(unittestdir); then \
 		echo cd $(unittestdir); \
@@ -31,6 +46,7 @@ check:
 		echo; \
 		exit 1; \
 	fi
+endif
 
 # synonyms for "check"
 .PHONY: regress test
diff --git a/configure b/configure
index bc1297ee5..dbd0a660d 100755
--- a/configure
+++ b/configure
@@ -16462,7 +16462,7 @@ LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 mk_include=include
 
 
-ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/Makefile src/expr/Makefile src/smt/Makefile src/main/Makefile src/prop/minisat/Makefile src/prop/Makefile src/util/Makefile src/context/Makefile src/parser/Makefile src/parser/cvc/Makefile src/parser/smt/Makefile src/theory/Makefile src/theory/bool/Makefile src/theory/uf/Makefile src/theory/arith/Makefile test/Makefile test/regress/Makefile test/system/Makefile test/unit/Makefile"
+ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/Makefile src/expr/Makefile src/smt/Makefile src/main/Makefile src/prop/minisat/Makefile src/prop/Makefile src/util/Makefile src/context/Makefile src/parser/Makefile src/parser/cvc/Makefile src/parser/smt/Makefile src/theory/Makefile src/theory/bool/Makefile src/theory/uf/Makefile 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"
 
 
 cat >confcache <<\_ACEOF
@@ -17563,6 +17563,10 @@ do
     "src/theory/arith/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/arith/Makefile" ;;
     "test/Makefile") CONFIG_FILES="$CONFIG_FILES test/Makefile" ;;
     "test/regress/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/Makefile" ;;
+    "test/regress/regress0/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress0/Makefile" ;;
+    "test/regress/regress1/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress1/Makefile" ;;
+    "test/regress/regress2/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress2/Makefile" ;;
+    "test/regress/regress3/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress3/Makefile" ;;
     "test/system/Makefile") CONFIG_FILES="$CONFIG_FILES test/system/Makefile" ;;
     "test/unit/Makefile") CONFIG_FILES="$CONFIG_FILES test/unit/Makefile" ;;
 
diff --git a/test/Makefile.am b/test/Makefile.am
index 575d07b77..316b2a140 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -1,5 +1,11 @@
 SUBDIRS = unit system regress
 
+.PHONY: regress0 regress1 regress2 regress3
+regress0 regress1 regress2 regress3:
+	for dir in $(SUBDIRS); do \
+		(cd $$dir && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1; \
+	done
+
 # synonyms for "check"
 .PHONY: regress test
 regress test: check
diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am
index bec1fce3e..6ed661de9 100644
--- a/test/regress/Makefile.am
+++ b/test/regress/Makefile.am
@@ -1,4 +1,12 @@
-SUBDIRS = regress0 regress1 regress2 regress3
+SUBDIRS = regress0
+DIST_SUBDIRS = regress1 regress2 regress3
+
+.PHONY: regress0 regress1 regress2 regress3
+regress1: regress0
+regress2: regress0 regress1
+regress3: regress0 regress1 regress2
+regress0 regress1 regress2 regress3:
+	cd $@ && $(MAKE) check
 
 # synonyms for "check"
 .PHONY: regress test
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index b0caacf1b..df0268f80 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,5 +1,19 @@
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
-TESTS =
+TESTS =	boolean.cvc \
+	bug1.cvc \
+	hole6.cvc \
+	logops.cvc \
+	queries0.cvc \
+	simple2.smt \
+	simple.cvc \
+	simple.smt \
+	simple-uf.smt \
+	smallcnf.cvc \
+	test11.cvc \
+	test12.cvc \
+	test9.cvc \
+	uf20-03.cvc \
+	wiki.cvc
 
 # synonyms for "check"
 .PHONY: regress regress0 test
diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
index a99ed3f70..8a41e99a3 100644
--- a/test/regress/regress1/Makefile.am
+++ b/test/regress/regress1/Makefile.am
@@ -1,5 +1,8 @@
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
-TESTS =
+TESTS =	friedman_n4_i5.smt \
+	hole7.cvc \
+	hole8.cvc \
+	instance_1444.smt
 
 # synonyms for "check"
 .PHONY: regress regress1 test
diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am
index 72742f201..2f72dd5e2 100644
--- a/test/regress/regress2/Makefile.am
+++ b/test/regress/regress2/Makefile.am
@@ -1,5 +1,20 @@
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
-TESTS =
+TESTS =	bmc-galileo-8.smt \
+	bmc-galileo-9.smt \
+	bmc-ibm-10.smt \
+	bmc-ibm-11.smt \
+	bmc-ibm-12.smt \
+	bmc-ibm-13.smt \
+	bmc-ibm-1.smt \
+	bmc-ibm-2.smt \
+	bmc-ibm-3.smt \
+	bmc-ibm-4.smt \
+	bmc-ibm-5.smt \
+	bmc-ibm-6.smt \
+	bmc-ibm-7.smt \
+	friedman_n6_i4.smt \
+	hole9.cvc \
+	qwh.35.405.shuffled-as.sat03-1651.smt
 
 # synonyms for "check"
 .PHONY: regress regress2 test
diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am
index 202bc553f..f0f46171c 100644
--- a/test/regress/regress3/Makefile.am
+++ b/test/regress/regress3/Makefile.am
@@ -1,5 +1,8 @@
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
-TESTS =
+TESTS =	C880mul.miter.shuffled-as.sat03-348.smt \
+	comb2.shuffled-as.sat03-420.smt \
+	hole10.cvc \
+	instance_1151.smt
 
 # synonyms for "check"
 .PHONY: regress regress3 test
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 2aba75e1c..15f781333 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -28,3 +28,7 @@ $(TESTS):: $(TEST_DEPS)
 # synonyms for "check"
 .PHONY: regress test
 regress test: check
+
+# in system test dir, regressN are also synonyms for check
+.PHONY: regress0 regress1 regress2 regress3
+regress0 regress1 regress2 regress3: check
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 1908f909d..7a1b75cbc 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -86,3 +86,7 @@ endif
 # synonyms for "check"
 .PHONY: regress test
 regress test: check
+
+# in unit test dir, regressN are also synonyms for check
+.PHONY: regress0 regress1 regress2 regress3
+regress0 regress1 regress2 regress3: check