From: Morgan Deters Date: Thu, 4 Feb 2010 23:29:47 +0000 (+0000) Subject: build system for multi-level regressions X-Git-Tag: cvc5-1.0.0~9284 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8e71a972b206c19c08ed284f4be7e9b96921ad5f;p=cvc5.git build system for multi-level regressions --- 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