make dist && make distcheck functional, other fixes

diff --git a/Makefile.am b/Makefile.am
index 4048b1b41d7ba284a9f82d5a2284faf38bd7341d..35744e381994adbaf304adf876cdf92d2f509c14 100644 (file)
--- a/Makefile.am
+++ b/Makefile.am
@@ -80,3 +80,21 @@ lcov lcov-all lcov18:
 
 endif
 
+# abs_srcdir is required here to get this Makefile instead of the
+# Makefile in the builddir (since $(srcdir) is stripped off of
+# EXTRA_DIST files)
+EXTRA_DIST = \
+       Makefile.builds.in \
+       Makefile.subdir \
+       config/build-type \
+       config/mkbuilddir \
+       contrib/addsourcedir \
+       contrib/code-checker \
+       contrib/configure-in-place \
+       contrib/cvc-devel.el \
+       contrib/cvc-mode.el \
+       contrib/dimacs_to_smt.pl \
+       contrib/editing-with-emacs \
+       contrib/switch-config
+dist-hook:
+       cp -p "$(srcdir)/Makefile" "$(distdir)/Makefile"

diff --git a/configure.ac b/configure.ac
index 49e35f71e53d3527b872b7b765e9b7bf4d63e4fa..4cdeb49552d81162a2ad472561b75883f6a09aef 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -244,6 +244,9 @@ AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
 
 # construct the build string
 AC_MSG_CHECKING([for appropriate build string])
+if test -z "$ac_confdir"; then
+  ac_confdir="$srcdir"
+fi
 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
 if test "$custom_build_profile" = yes; then
   if test "$with_build" = default; then

diff --git a/src/Makefile.am b/src/Makefile.am
index 97c66ac89409bf79e05e1ee676d2c49e1283f96f..e436971fa04c24baaa00ec9ce25b598054372b85 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -42,6 +42,12 @@ libcvc4_noinst_la_LIBADD = \
        @builddir@/smt/libsmt.la \
        @builddir@/theory/libtheory.la
 
+EXTRA_DIST = \
+       include/cvc4parser_private.h \
+       include/cvc4parser_public.h \
+       include/cvc4_private.h \
+       include/cvc4_public.h
+
 # empty.cpp hack; see above
 empty.cpp:; touch empty.cpp
 
@@ -55,3 +61,9 @@ install-data-local: $(publicheaders)
                echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
                $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
        done
+
+uninstall-local:
+       @for f in $(publicheaders); do \
+               rm -f "$(DESTDIR)/$(includedir)/cvc4/$$f"
+       done
+       rmdir "$(DESTDIR)/$(includedir)/cvc4"

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index db863440ca39eb5a554ae933a7c526cff44265e0..5f24538987f59ba4570e67ef9354bdfa248d748b 100644 (file)
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -10,47 +10,63 @@ libexpr_la_SOURCES = \
        node.cpp \
        type_node.h \
        type_node.cpp \
+       type_constant.h \
        node_builder.h \
        convenience_node_builders.h \
-       @srcdir@/expr.h \
        type.h \
        type.cpp \
        node_value.h \
        node_manager.h \
-       @srcdir@/expr_manager.h \
        attribute.h \
+       attribute_internals.h \
        attribute.cpp \
-       @srcdir@/kind.h \
-       @srcdir@/metakind.h \
        node_manager.cpp \
-       @srcdir@/expr_manager.cpp \
        node_value.cpp \
-       @srcdir@/expr.cpp \
        command.h \
        command.cpp \
        declaration_scope.h \
        declaration_scope.cpp \
        expr_manager_scope.h 
+nodist_libexpr_la_SOURCES = \
+       kind.h \
+       metakind.h \
+       expr.h \
+       expr.cpp \
+       expr_manager.h \
+       expr_manager.cpp
 
 EXTRA_DIST = \
-       @srcdir@/kind.h \
-       @srcdir@/metakind.h \
-       @srcdir@/expr_manager.h \
-       @srcdir@/expr.h \
-       @srcdir@/expr_manager.cpp \
-       @srcdir@/expr.cpp \
-       @srcdir@/type.h \
-       @srcdir@/type.cpp \
        kind_template.h \
        metakind_template.h \
        expr_manager_template.h \
        expr_manager_template.cpp \
        expr_template.h \
-       expr_template.cpp
+       expr_template.cpp \
+       mkkind \
+       mkmetakind \
+       mkexpr
+
+BUILT_SOURCES = \
+       kind.h \
+       metakind.h \
+       expr.h \
+       expr.cpp \
+       expr_manager.h \
+       expr_manager.cpp \
+       $(top_builddir)/src/theory/.subdirs
+
+CLEANFILES = \
+       kind.h \
+       metakind.h \
+       expr.h \
+       expr.cpp \
+       expr_manager.h \
+       expr_manager.cpp \
+       $(top_builddir)/src/theory/.subdirs
 
 include @top_srcdir@/src/theory/Makefile.subdirs
 
-@srcdir@/kind.h: kind_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+kind.h: kind_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
        $(AM_V_at)chmod +x @srcdir@/mkkind
        $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
        $(AM_V_GEN)(@srcdir@/mkkind \
@@ -58,7 +74,7 @@ include @top_srcdir@/src/theory/Makefile.subdirs
                `cat @top_builddir@/src/theory/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-@srcdir@/metakind.h: metakind_template.h mkmetakind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+metakind.h: metakind_template.h mkmetakind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
        $(AM_V_at)chmod +x @srcdir@/mkmetakind
        $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
        $(AM_V_GEN)(@srcdir@/mkmetakind \
@@ -66,7 +82,7 @@ include @top_srcdir@/src/theory/Makefile.subdirs
                `cat @top_builddir@/src/theory/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-@srcdir@/expr.h: expr_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+expr.h: expr_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
        $(AM_V_at)chmod +x @srcdir@/mkexpr
        $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
        $(AM_V_GEN)(@srcdir@/mkexpr \
@@ -74,7 +90,7 @@ include @top_srcdir@/src/theory/Makefile.subdirs
                `cat @top_builddir@/src/theory/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-@srcdir@/expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
        $(AM_V_at)chmod +x @srcdir@/mkexpr
        $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
        $(AM_V_GEN)(@srcdir@/mkexpr \
@@ -82,7 +98,7 @@ include @top_srcdir@/src/theory/Makefile.subdirs
                `cat @top_builddir@/src/theory/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-@srcdir@/expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
        $(AM_V_at)chmod +x @srcdir@/mkexpr
        $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
        $(AM_V_GEN)(@srcdir@/mkexpr \
@@ -90,34 +106,10 @@ include @top_srcdir@/src/theory/Makefile.subdirs
                `cat @top_builddir@/src/theory/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-@srcdir@/expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
        $(AM_V_at)chmod +x @srcdir@/mkexpr
        $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
        $(AM_V_GEN)(@srcdir@/mkexpr \
                $< \
                `cat @top_builddir@/src/theory/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
-
-BUILT_SOURCES = \
-       @srcdir@/kind.h \
-       @srcdir@/metakind.h \
-       @srcdir@/expr.h \
-       @srcdir@/expr.cpp \
-       @srcdir@/expr_manager.h \
-       @srcdir@/expr_manager.cpp
-
-dist-hook: \
-       @srcdir@/kind.h \
-       @srcdir@/metakind.h \
-       @srcdir@/expr.h \
-       @srcdir@/expr.cpp \
-       @srcdir@/expr_manager.h \
-       @srcdir@/expr_manager.cpp
-
-MAINTAINERCLEANFILES = \
-       @srcdir@/kind.h \
-       @srcdir@/metakind.h \
-       @srcdir@/expr.h \
-       @srcdir@/expr.cpp \
-       @srcdir@/expr_manager.h \
-       @srcdir@/expr_manager.cpp

diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 2318699e73e80aed08517b49ad18d199f87204a3..83462c355a651b51b26a1f33532cc9da94bb4db8 100644 (file)
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -19,7 +19,7 @@
 #ifndef DECLARATION_SCOPE_H_
 #define DECLARATION_SCOPE_H_
 
-#include "expr.h"
+#include "expr/expr.h"
 #include "util/hash.h"
 
 #include <ext/hash_map>

diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index cfe983727f81f837d7e3a9df1d0e387bdbcdc34a..ea67ef35629ba7eae9c06fcdd02363f99fb132f8 100644 (file)
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -28,8 +28,10 @@ libparsercvc_la_SOURCES = \
     cvc_input.cpp \
     $(ANTLR_STUFF)
 
-BUILT_SOURCES = $(ANTLR_STUFF)
-dist-hook: $(ANTLR_STUFF)
+BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
+
+EXTRA_DIST = @srcdir@/stamp-generated
+
 MAINTAINERCLEANFILES = $(ANTLR_STUFF)
 maintainer-clean-local:
        -$(AM_V_at)rmdir @srcdir@/generated

diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index f5ea3aae3f9bc1580a37432fa1dddeb1a7ce13bf..19665b0f79f274a06bdb0e311896e417535ed276 100644 (file)
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -30,8 +30,10 @@ libparsersmt_la_SOURCES = \
        smt_input.cpp \
        $(ANTLR_STUFF)
 
-BUILT_SOURCES = $(ANTLR_STUFF)
-dist-hook: $(ANTLR_STUFF)
+BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
+
+EXTRA_DIST = @srcdir@/stamp-generated
+
 MAINTAINERCLEANFILES = $(ANTLR_STUFF)
 maintainer-clean-local:
        -$(AM_V_at)rmdir @srcdir@/generated

diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am
index aabae53526119313ce0646a6c815fbf5da956681..99ff0dabaf38bba6a442e769b1edcbaebef62436 100644 (file)
--- a/src/parser/smt2/Makefile.am
+++ b/src/parser/smt2/Makefile.am
@@ -25,13 +25,15 @@ ANTLR_STUFF = \
 libparsersmt2_la_SOURCES = \
        Smt2.g \
        smt2.h \
-    smt2.cpp \
+       smt2.cpp \
        smt2_input.h \
        smt2_input.cpp \
        $(ANTLR_STUFF)
 
-BUILT_SOURCES = $(ANTLR_STUFF)
-dist-hook: $(ANTLR_STUFF)
+BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
+
+EXTRA_DIST = @srcdir@/stamp-generated
+
 MAINTAINERCLEANFILES = $(ANTLR_STUFF)
 maintainer-clean-local:
        -$(AM_V_at)rmdir @srcdir@/generated

diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 06504e73c6bcb6e0529f0d045edd441efdb5838e..dbd32c0626a88daa0b6c02644a2d312d7fce0460 100644 (file)
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -11,7 +11,6 @@ libprop_la_SOURCES = \
        sat.h \
         sat.cpp \
        cnf_stream.h \
-       cnf_stream.cpp \
-       cnf_conversion.h
+       cnf_stream.cpp
 
 SUBDIRS = minisat

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index a2a206d405b9884af3d2c0f42fa866b1537a4eed..ce15b86d4a81da6835fec67af5e89293cf4014b0 100644 (file)
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -6,12 +6,15 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 noinst_LTLIBRARIES = libtheory.la
 
 libtheory_la_SOURCES = \
-       @srcdir@/theoryof_table.h \
+       output_channel.h \
+       interrupted.h \
        theory_engine.h \
        theory_engine.cpp \
        theory_test_utils.h \
        theory.h \
        theory.cpp
+nodist_libtheory_la_SOURCES = \
+       theoryof_table.h
 
 libtheory_la_LIBADD = \
        @builddir@/builtin/libbuiltin.la \
@@ -22,12 +25,19 @@ libtheory_la_LIBADD = \
        @builddir@/bv/libbv.la
 
 EXTRA_DIST = \
-       @srcdir@/theoryof_table.h \
-       theoryof_table_template.h
+       theoryof_table_template.h \
+       mktheoryof \
+       Makefile.subdirs
+
+BUILT_SOURCES = \
+       theoryof_table.h
+
+CLEANFILES = \
+       theoryof_table.h
 
 include @top_srcdir@/src/theory/Makefile.subdirs
 
-@srcdir@/theoryof_table.h: theoryof_table_template.h mktheoryof @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+theoryof_table.h: theoryof_table_template.h mktheoryof @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
        $(AM_V_at)chmod +x @srcdir@/mktheoryof
        $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
        $(AM_V_GEN)(@srcdir@/mktheoryof \
@@ -35,8 +45,4 @@ include @top_srcdir@/src/theory/Makefile.subdirs
                `cat @top_builddir@/src/theory/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-BUILT_SOURCES = @srcdir@/theoryof_table.h
-dist-hook: @srcdir@/theoryof_table.h
-MAINTAINERCLEANFILES = @srcdir@/theoryof_table.h
-
 SUBDIRS = builtin booleans uf arith arrays bv

diff --git a/src/theory/Makefile.subdirs b/src/theory/Makefile.subdirs
index 0dfba2449d16c368d426b7a1a574835033019c72..eafb350ae35ecb1a2cc5211a929d2c24b0040583 100644 (file)
--- a/src/theory/Makefile.subdirs
+++ b/src/theory/Makefile.subdirs
@@ -4,3 +4,4 @@ $(top_builddir)/src/theory/.subdirs: $(top_srcdir)/src/theory/Makefile.am
                echo "  GEN   " $@; \
                $(am__mv) $(top_builddir)/src/theory/.subdirs.tmp $(top_builddir)/src/theory/.subdirs; \
        fi
+

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 4d299e8afe4d9689263f02c466a1df7bee3c3bad..e500f5cf81776b62270d61395a7169980b249b79 100644 (file)
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -18,7 +18,6 @@ libarith_la_SOURCES = \
        partial_model.cpp \
        ordered_bounds_list.h \
        basic.h \
-       normal.h \
        slack.h \
        tableau.h \
        arith_propagator.h \
@@ -26,4 +25,6 @@ libarith_la_SOURCES = \
        theory_arith.h \
        theory_arith.cpp
 
-EXTRA_DIST = kinds
+EXTRA_DIST = \
+       kinds \
+       normal_form_notes.txt

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index b6ca5bcc66fdfb8c766a71e44ea80e318ebc0fa9..a690f743278f825b184779ce817a1fdee6d5a62d 100644 (file)
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -16,6 +16,7 @@ libutil_la_SOURCES = \
        decision_engine.h \
        exception.h \
        hash.h \
+       bool.h \
        model.h \
        options.h \
        output.cpp \

diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am
index de06dd4d2850f7b63bc86ab2a7bff940230c6fe3..a3808b7519d8f6173d0dd173555c77b705cd3cc6 100644 (file)
--- 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 4744cc0fe0a1411932c1204379a0b2fcac339894..47ff97d616a5a5b1915abb1d3243565c4034e3e0 100644 (file)
--- 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 362ec70b6439f8ad60827ec3fdfde2789d772cf0..4cf18f17dbb93608bc47b59c80d27c9cc43330a3 100644 (file)
--- 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 802189f2b54ee752a01159762de9e50989b5ba15..bf516107e8f451c3dba2fb0c6496cde1a6811d0c 100644 (file)
--- 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 f133a272d652aadfa1df8eb278ec66488a76a580..981ab80129c60b6105b105f4e86bd810619d4a32 100644 (file)
--- 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 9dd4934ac156ebf0533938aaaf8cf8e6cd2c81c2..51d1458597a9c3d41ccd31841dc908c34035156b 100644 (file)
--- 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 5d34df14d0aae557d147b3d914166ac64e111103..8d3ebb137f5a9e7238fcfa6cf4db27adcdec0e85 100644 (file)
--- 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 e427e35067bd503834f87618bf7289785463df02..c96fbccb603240a583a14df63c8b39f00dc1573a 100644 (file)
--- 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
+