build system for multi-level regressions

8 files changed, 62 insertions, 5 deletions

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