build system for multi-level regressions

diff --git a/Makefile.am b/Makefile.am
index 20d6298f456ba17ff20edf52e364067fb3984c78..bade9cd15dfab67e5b05d09d522faf67b527b4f8 100644 (file)
--- 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 5b151441eb57308e59f597c741657417469a6e58..9eec964e016621ac780f6a524bd4ca03ebfdfcb2 100644 (file)
--- 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 bc1297ee5468772bfcb255a91a4c781301aafff3..dbd0a660d6becc47bb59c461c625602cf1d1fa33 100755 (executable)
--- 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 575d07b77afbe7359120761f3f5a04d229ba097d..316b2a140a6a4d8399d37aed81bfffbe158cb912 100644 (file)
--- 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 bec1fce3e6a207e252da4a85593f33065ecd6f1c..6ed661de9306b618674ad73376e1810a730a9abc 100644 (file)
--- 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 b0caacf1b259be6830a0432ccb8561fa39290f31..df0268f8033d81c9e7c5b045f3408bf8fd0f60d2 100644 (file)
--- 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 a99ed3f70b77e8248d1fb1e134275d4f1effcd43..8a41e99a3f7072f74761273fa2367a0568ba8f11 100644 (file)
--- 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 72742f2018bc4b28a18e68ed34f2fe7fac2b93b4..2f72dd5e283b684192bb92a3e41ea13de6706649 100644 (file)
--- 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 202bc553f49d8eb3935daed06fc7b2f9ae3cd08f..f0f46171cc8ef5c97ce1e1ed4cd7eb635cda0d0d 100644 (file)
--- 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 2aba75e1cfd380ef9b9e53ed9a8f61cee734236d..15f781333e87f3d54d2618e81e8ba00a297e0a05 100644 (file)
--- 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 1908f909dbc9ea418716272e9e415ff18eb7ac79..7a1b75cbcfe0d735503cf86a7a49ee10079e3276 100644 (file)
--- 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