diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/Makefile.am | 6 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 6 | ||||
-rw-r--r-- | test/regress/regress0/precedence/Makefile.am | 17 | ||||
-rw-r--r-- | test/regress/regress0/uf/Makefile.am | 24 | ||||
-rw-r--r-- | test/regress/regress1/Makefile.am | 6 | ||||
-rw-r--r-- | test/regress/regress2/Makefile.am | 6 | ||||
-rw-r--r-- | test/regress/regress3/Makefile.am | 6 | ||||
-rw-r--r-- | test/unit/Makefile.am | 47 |
8 files changed, 108 insertions, 10 deletions
diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index de06dd4d2..a3808b751 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -1,5 +1,5 @@ SUBDIRS = regress0 -DIST_SUBDIRS = regress1 regress2 regress3 +DIST_SUBDIRS = regress0 regress1 regress2 regress3 export VERBOSE = 1 @@ -13,3 +13,7 @@ regress0 regress1 regress2 regress3: # synonyms for "check" .PHONY: regress test regress test: check + +EXTRA_DIST = \ + run_regression \ + README diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 4744cc0fe..47ff97d61 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -63,12 +63,18 @@ TESTS = \ wiki.21.cvc \ fuzz_3.smt +EXTRA_DIST = $(TESTS) + if CVC4_BUILD_PROFILE_COMPETITION else TESTS += \ error.cvc endif +# and make sure to distribute it +EXTRA_DIST += \ + error.cvc + # synonyms for "check" .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am index 362ec70b6..4cf18f17d 100644 --- a/test/regress/regress0/precedence/Makefile.am +++ b/test/regress/regress0/precedence/Makefile.am @@ -1,6 +1,10 @@ TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" TESTS = \ - iff-implies.cvc \ + iff-implies.cvc \ implies-iff.cvc \ implies-or.cvc \ or-implies.cvc \ @@ -16,6 +20,17 @@ TESTS = \ implies-assoc.cvc \ xor-assoc.cvc +EXTRA_DIST = $(TESTS) + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc # synonyms for "check" .PHONY: regress regress0 test diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 802189f2b..bf516107e 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -1,4 +1,8 @@ TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" TESTS = \ euf_simp01.smt \ euf_simp02.smt \ @@ -15,10 +19,22 @@ TESTS = \ dead_dnd002.smt \ iso_brn001.smt \ SEQ032_size2.smt \ - simple.01.cvc \ - simple.02.cvc \ - simple.03.cvc \ - simple.04.cvc + simple.01.cvc \ + simple.02.cvc \ + simple.03.cvc \ + simple.04.cvc + +EXTRA_DIST = $(TESTS) + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc # synonyms for "check" .PHONY: regress regress0 test diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index f133a272d..981ab8012 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -12,11 +12,17 @@ TESTS = friedman_n4_i5.smt \ fuzz_1.smt \ fuzz_2.smt +EXTRA_DIST = $(TESTS) + #if CVC4_BUILD_PROFILE_COMPETITION #else #TESTS += \ # error.cvc #endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc # synonyms for "check" .PHONY: regress regress1 test diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am index 9dd4934ac..51d145859 100644 --- a/test/regress/regress2/Makefile.am +++ b/test/regress/regress2/Makefile.am @@ -22,11 +22,17 @@ TESTS = bmc-galileo-8.smt \ hole9.cvc \ qwh.35.405.shuffled-as.sat03-1651.smt +EXTRA_DIST = $(TESTS) + #if CVC4_BUILD_PROFILE_COMPETITION #else #TESTS += \ # error.cvc #endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc # synonyms for "check" .PHONY: regress regress2 test diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am index 5d34df14d..8d3ebb137 100644 --- a/test/regress/regress3/Makefile.am +++ b/test/regress/regress3/Makefile.am @@ -10,11 +10,17 @@ TESTS = C880mul.miter.shuffled-as.sat03-348.smt \ hole10.cvc \ instance_1151.smt +EXTRA_DIST = $(TESTS) + #if CVC4_BUILD_PROFILE_COMPETITION #else #TESTS += \ # error.cvc #endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc # synonyms for "check" .PHONY: regress regress3 test diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index e427e3506..c96fbccb6 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -40,7 +40,8 @@ export VERBOSE = 1 # Things that aren't tests but that tests rely on and need to # go into the distribution TEST_DEPS_DIST = \ - memory.h + memory.h \ + Makefile.tests if HAVE_CXXTESTGEN @@ -68,6 +69,8 @@ AM_LIBADD_PUBLIC = \ EXTRA_DIST = \ no_cxxtest \ + $(UNIT_TESTS:%=%.cpp) \ + $(UNIT_TESTS:%=%.h) \ $(TEST_DEPS_DIST) MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp) @@ -133,15 +136,19 @@ else TESTS = no_cxxtest EXTRA_DIST = \ - $(UNIT_TESTS:%=%.cpp) \ - $(TEST_DEPS_DIST) + no_cxxtest \ + $(UNIT_TESTS:%=%.h) \ + $(TEST_DEPS_DIST) \ + no-cxxtest-available endif +$(UNIT_TESTS:%=%.cpp): $(UNIT_TESTS:%=$(abs_builddir)/%.cpp) + # trick automake into setting LTCXXCOMPILE, CXXLINK, etc. if CVC4_FALSE noinst_LTLIBRARIES = libdummy.la -libdummy_la_SOURCES = expr/node_black.cpp +nodist_libdummy_la_SOURCES = expr/node_black.cpp libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la endif @@ -152,3 +159,35 @@ regress test: check # in unit test dir, regressN are also synonyms for check .PHONY: regress0 regress1 regress2 regress3 regress0 regress1 regress2 regress3: check + +if HAVE_CXXTESTGEN +# all is fine with the world +else +# all is not ! +no-cxxtest-available: + @if test "$(I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS)" = 1; then \ + echo; \ + echo "WARNING:"; \ + echo "WARNING: No CxxTest to build unit tests, but, then, you know that;"; \ + echo "WARNING: I hope you know what you're doing."; \ + echo "WARNING:"; \ + echo; \ + ( echo "CxxTest was not available at the time this distribution was built,"; \ + echo "so the tests could not be built. You'll need CxxTest to test this"; \ + echo "distribution." ) >no-cxxtest-available; \ + else \ + echo; \ + echo "ERROR:"; \ + echo "ERROR: You cannot make dist in this build directory, you do not have CxxTest."; \ + echo "ERROR: The tests should be generated for the user and included in the tarball,"; \ + echo "ERROR: otherwise they'll be required to have CxxTest just to test the standard"; \ + echo "ERROR: distribution built correctly."; \ + echo "ERROR: If you really want to do this, append the following to your make command."; \ + echo "ERROR:"; \ + echo "ERROR: I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS=1"; \ + echo "ERROR:"; \ + echo; \ + exit 1; \ + fi >&2 +endif + |