fix some things with the build system (make dist, make install, make check)

diff --git a/Makefile.am b/Makefile.am
index e482638d3e03edff0ca4befd7c412924f61ad769..288cfb2cc1b1b059bfe4509732479c6201603eeb 100644 (file)
--- a/Makefile.am
+++ b/Makefile.am
@@ -89,6 +89,7 @@ EXTRA_DIST = \
        Makefile.builds.in \
        Makefile.subdir \
        config/build-type \
-       config/mkbuilddir
+       config/mkbuilddir \
+       config/doxygen.cfg
 dist-hook:
        cp -p "$(srcdir)/Makefile" "$(distdir)/Makefile"

diff --git a/src/Makefile.am b/src/Makefile.am
index a46f56598b8015efb2f98eb1441f1ef84dc51594..069a446e688cc3b18afb7a5cceec4d0ae2f36cbe 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -17,7 +17,7 @@ AM_CPPFLAGS = \
        -I@srcdir@/include -I@srcdir@ -I@builddir@
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
-SUBDIRS = lib expr util context theory prop smt . parser main
+SUBDIRS = lib expr util context theory prop smt printer . parser main
 
 lib_LTLIBRARIES = libcvc4.la
 noinst_LTLIBRARIES = libcvc4_noinst.la
@@ -62,15 +62,15 @@ publicheaders = \
        include/cvc4parser_public.h
 
 install-data-local: $(publicheaders)
-       $(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4
+       $(mkinstalldirs) $(DESTDIR)$(prefix)$(includedir)/cvc4
        @for f in $(publicheaders); do \
-               echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
-               $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
+               echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)$(prefix)$(includedir)/cvc4"; \
+               $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)$(prefix)$(includedir)/cvc4"; \
        done
 
 uninstall-local:
        @for f in $(publicheaders); do \
                f=`echo "$$f" | sed 's,.*/,,'`; \
-               rm -f "$(DESTDIR)$(includedir)/cvc4/$$f"; \
+               rm -f "$(DESTDIR)$(prefix)$(includedir)/cvc4/$$f"; \
        done
-       @rmdir "$(DESTDIR)$(includedir)/cvc4"
+       @rmdir "$(DESTDIR)$(prefix)$(includedir)/cvc4"

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index c82968ef682c21298515907b887716066e362011..639e9eb4c78c3c12e584a62d12b8af326cf4dc6f 100644 (file)
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -3,6 +3,8 @@ AM_CPPFLAGS = \
        -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
+SUBDIRS = builtin booleans uf arith arrays bv
+
 noinst_LTLIBRARIES = libtheory.la
 
 libtheory_la_SOURCES = \
@@ -48,5 +50,3 @@ theoryof_table.h: theoryof_table_template.h mktheoryof @top_builddir@/src/theory
                $< \
                `cat @top_builddir@/src/theory/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
-
-SUBDIRS = builtin booleans uf arith arrays bv

diff --git a/test/Makefile.am b/test/Makefile.am
index 2ff1c497425b4cc30ac5d36e65e99cbb68f4ff73..e370752b68bbb473611cbe1d78275cdf240949dd 100644 (file)
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -26,7 +26,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \
   blu='\e[1;34m'; \
   std='\e[m'; \
 }
-subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
+subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/lemmas regress/regress0/push-pop regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
 check-recursive: check-pre
 .PHONY: check-pre
 check-pre:

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index d50633a19190ad2d9000192a4a1845aa06b26970..9f4fdce898b10215b74f002640c5f5850b402b83 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . arith precedence uf bv lemmas
+SUBDIRS = . arith precedence uf bv lemmas push-pop
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 MAKEFLAGS = -k

diff --git a/test/regress/regress0/bv/Makefile b/test/regress/regress0/bv/Makefile
new file mode 100644 (file)
index 0000000..c9ec320
--- /dev/null
+++ b/test/regress/regress0/bv/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/bv
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check

diff --git a/test/regress/regress0/bv/core/Makefile b/test/regress/regress0/bv/core/Makefile
new file mode 100644 (file)
index 0000000..15e8e62
--- /dev/null
+++ b/test/regress/regress0/bv/core/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../../..
+srcdir = test/regress/regress0/bv/core
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check

diff --git a/test/regress/regress0/lemmas/Makefile b/test/regress/regress0/lemmas/Makefile
new file mode 100644 (file)
index 0000000..96e2422
--- /dev/null
+++ b/test/regress/regress0/lemmas/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/lemmas
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check

diff --git a/test/regress/regress0/push-pop/Makefile b/test/regress/regress0/push-pop/Makefile
new file mode 100644 (file)
index 0000000..cd5bcd3
--- /dev/null
+++ b/test/regress/regress0/push-pop/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../push-pop
+srcdir = test/regress/regress0/push-pop
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check

diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
new file mode 100644 (file)
index 0000000..ee365e7
--- /dev/null
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -0,0 +1,25 @@
+SUBDIRS = . 
+
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+
+# Regression tests for SMT inputs
+CVC_TESTS = \
+       test.00.cvc \
+       test.01.cvc
+
+TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
+
+EXTRA_DIST = $(TESTS)
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3: