summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/Makefile.am6
-rw-r--r--test/regress/regress0/Makefile.am6
-rw-r--r--test/regress/regress0/precedence/Makefile.am17
-rw-r--r--test/regress/regress0/uf/Makefile.am24
-rw-r--r--test/regress/regress1/Makefile.am6
-rw-r--r--test/regress/regress2/Makefile.am6
-rw-r--r--test/regress/regress3/Makefile.am6
-rw-r--r--test/unit/Makefile.am47
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
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback