This commit removes using absolute paths in the generation of the .subdirs file....

diff --git a/src/Makefile.am b/src/Makefile.am
index 95ca44e635ea7e1c19e829210295731d596a7788..9502afa9c354fe25b9aedc7a6f61960e0047d467 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -20,7 +20,8 @@ AM_CPPFLAGS = \
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN)
 
 SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main
-THEORIES = builtin booleans uf arith bv fp arrays datatypes sets strings quantifiers idl
+# The THEORIES list has been moved to Makefile.theories
+include @top_srcdir@/src/Makefile.theories
 
 lib_LTLIBRARIES = libcvc4.la
 
@@ -232,7 +233,7 @@ libcvc4_la_SOURCES = \
        theory/builtin/theory_builtin.cpp \
        theory/datatypes/theory_datatypes_type_rules.h \
        theory/datatypes/type_enumerator.h \
-        theory/datatypes/type_enumerator.cpp \
+       theory/datatypes/type_enumerator.cpp \
        theory/datatypes/theory_datatypes.h \
        theory/datatypes/datatypes_rewriter.h \
        theory/datatypes/theory_datatypes.cpp \
@@ -465,7 +466,8 @@ endif
 BUILT_SOURCES = \
        theory/rewriter_tables.h \
        theory/theory_traits.h \
-       theory/type_enumerator.cpp
+       theory/type_enumerator.cpp \
+       $(top_builddir)/src/.subdirs
 
 CLEANFILES = \
        svn_versioninfo.cpp \
@@ -476,7 +478,8 @@ CLEANFILES = \
        gitinfo \
        theory/rewriter_tables.h \
        theory/theory_traits.h \
-       theory/type_enumerator.cpp
+       theory/type_enumerator.cpp \
+       $(top_builddir)/src/.subdirs
 
 EXTRA_DIST = \
        include/cvc4_private_library.h \
@@ -486,6 +489,7 @@ EXTRA_DIST = \
        include/cvc4_public.h \
        include/cvc4.h \
        cvc4.i \
+       Makefile.theories \
        smt/smt_options_template.cpp \
        smt/modal_exception.i \
        smt/logic_exception.i \
@@ -496,7 +500,6 @@ EXTRA_DIST = \
        theory/type_enumerator_template.cpp \
        theory/mktheorytraits \
        theory/mkrewriter \
-       theory/Makefile.subdirs \
        theory/uf/kinds \
        theory/bv/kinds \
        theory/idl/kinds \
@@ -633,28 +636,41 @@ uninstall-local:
 # fails.
 %.Plo:; $(MKDIR_P) "$(dir $@)" && : > "$@"
 
-include @top_srcdir@/src/theory/Makefile.subdirs
+#include @top_srcdir@/src/theory/Makefile.subdirs
+$(top_builddir)/src/.subdirs: $(top_srcdir)/src/Makefile.theories  @top_srcdir@/src/mksubdirs
+       $(AM_V_at)test -d $(top_builddir)/src || mkdir $(top_builddir)/src
+       $(AM_V_at)chmod +x @top_srcdir@/src/mksubdirs
+       $(AM_V_at)( @top_srcdir@/src/mksubdirs "$(top_srcdir)" ) > $(top_builddir)/src/.subdirs.tmp
+       @if ! diff -q $(top_builddir)/src/.subdirs $(top_builddir)/src/.subdirs.tmp &>/dev/null; then \
+               echo "  GEN   " $@; \
+               $(am__mv) $(top_builddir)/src/.subdirs.tmp $(top_builddir)/src/.subdirs; \
+       fi
+
+#      $(AM_V_at)(\
+#        grep '^THEORIES = ' $(top_srcdir)/src/Makefile.theories | \
+#        cut -d' ' -f3- | tr ' ' "\n" | \
+#        xargs -I__D__ echo $(top_srcdir)/src/theory/__D__/kinds ) >$(top_builddir)/src/.subdirs.tmp
 
-theory/rewriter_tables.h: theory/rewriter_tables_template.h theory/mkrewriter @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+theory/rewriter_tables.h: theory/rewriter_tables_template.h theory/mkrewriter @top_builddir@/src/.subdirs @top_srcdir@/src/theory/*/kinds
        $(AM_V_at)chmod +x @srcdir@/theory/mkrewriter
        $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
        $(AM_V_GEN)(@srcdir@/theory/mkrewriter \
                $< \
-               `cat @top_builddir@/src/theory/.subdirs` \
+               `cat @top_builddir@/src/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-theory/theory_traits.h: theory/theory_traits_template.h theory/mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+theory/theory_traits.h: theory/theory_traits_template.h theory/mktheorytraits @top_builddir@/src/.subdirs @top_srcdir@/src/theory/*/kinds
        $(AM_V_at)chmod +x @srcdir@/theory/mktheorytraits
        $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
        $(AM_V_GEN)(@srcdir@/theory/mktheorytraits \
                $< \
-               `cat @top_builddir@/src/theory/.subdirs` \
+               `cat @top_builddir@/src/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-theory/type_enumerator.cpp: theory/type_enumerator_template.cpp theory/mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+theory/type_enumerator.cpp: theory/type_enumerator_template.cpp theory/mktheorytraits @top_builddir@/src/.subdirs @top_srcdir@/src/theory/*/kinds
        $(AM_V_at)chmod +x @srcdir@/theory/mktheorytraits
        $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
        $(AM_V_GEN)(@srcdir@/theory/mktheorytraits \
                $< \
-               `cat @top_builddir@/src/theory/.subdirs` \
+               `cat @top_builddir@/src/.subdirs` \
        > $@) || (rm -f $@ && exit 1)

diff --git a/src/Makefile.theories b/src/Makefile.theories
new file mode 100644 (file)
index 0000000..8b5cef4
--- /dev/null
+++ b/src/Makefile.theories
@@ -0,0 +1,3 @@
+
+
+THEORIES = builtin booleans uf arith bv fp arrays datatypes sets strings quantifiers idl

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 13358d294f748fcbd2843539aa70530297177e23..c5a032abcc6e51c663f13a2ee152e438dfd001a7 100644 (file)
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -80,7 +80,7 @@ BUILT_SOURCES = \
        expr_manager.h \
        expr_manager.cpp \
        type_checker.cpp \
-       $(top_builddir)/src/theory/.subdirs
+       $(top_builddir)/src/expr/.subdirs
 
 CLEANFILES = \
        kind.h \
@@ -91,72 +91,79 @@ CLEANFILES = \
        expr_manager.cpp \
        type_checker.cpp \
        type_properties.h \
-       $(top_builddir)/src/theory/.subdirs
-
-include @top_srcdir@/src/theory/Makefile.subdirs
-
-kind.h: kind_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+       $(top_builddir)/src/expr/.subdirs
+
+$(top_builddir)/src/expr/.subdirs: $(top_srcdir)/src/Makefile.theories  @top_srcdir@/src/mksubdirs
+       $(AM_V_at)test -d $(top_builddir)/src/expr || mkdir $(top_builddir)/src/expr
+       $(AM_V_at)chmod +x @top_srcdir@/src/mksubdirs
+       $(AM_V_at)( @top_srcdir@/src/mksubdirs "$(top_srcdir)" ) > $(top_builddir)/src/expr/.subdirs.tmp
+       @if ! diff -q $(top_builddir)/src/expr/.subdirs $(top_builddir)/src/expr/.subdirs.tmp &>/dev/null; then \
+               echo "  GEN   " $@; \
+               $(am__mv) $(top_builddir)/src/expr/.subdirs.tmp $(top_builddir)/src/expr/.subdirs; \
+       fi
+
+kind.h: kind_template.h mkkind @top_builddir@/src/expr/.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 \
                $< \
-               `cat @top_builddir@/src/theory/.subdirs` \
+               `cat @top_builddir@/src/expr/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-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/expr/.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 \
                $< \
-               `cat @top_builddir@/src/theory/.subdirs` \
+               `cat @top_builddir@/src/expr/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-type_properties.h: type_properties_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+type_properties.h: type_properties_template.h mkkind @top_builddir@/src/expr/.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 \
                $< \
-               `cat @top_builddir@/src/theory/.subdirs` \
+               `cat @top_builddir@/src/expr/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-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/expr/.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` \
+               `cat @top_builddir@/src/expr/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-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/expr/.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` \
+               `cat @top_builddir@/src/expr/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-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/expr/.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` \
+               `cat @top_builddir@/src/expr/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-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/expr/.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` \
+               `cat @top_builddir@/src/expr/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
-type_checker.cpp: type_checker_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+type_checker.cpp: type_checker_template.cpp mkexpr @top_builddir@/src/expr/.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` \
+               `cat @top_builddir@/src/expr/.subdirs` \
        > $@) || (rm -f $@ && exit 1)
 
 .PHONY: builts

diff --git a/src/mksubdirs b/src/mksubdirs
new file mode 100755 (executable)
index 0000000..c96437c
--- /dev/null
+++ b/src/mksubdirs
@@ -0,0 +1,16 @@
+#!/bin/bash
+#
+# The purpose of this file is to generate a .subdirs file in the build process.
+# This file contains a file of relative paths to all of the theories relative
+# to the current directory. Each Makefile.am should thus build its own .subdirs file.
+# This assumes it is passed the equivalent of the $top_srcdir configure variable.
+#
+# Invocation:
+#
+#    mksubdirs <top_srcdir>
+
+TOP_SRCDIR=$1
+
+grep '^THEORIES = ' $TOP_SRCDIR/src/Makefile.theories | \
+  cut -d' ' -f3- | tr ' ' "\n" | \
+  xargs -I__D__ echo "$TOP_SRCDIR/src/theory/__D__/kinds"

diff --git a/src/theory/Makefile.subdirs b/src/theory/Makefile.subdirs
deleted file mode 100644 (file)
index 42582c6..0000000
--- a/src/theory/Makefile.subdirs
+++ /dev/null
@@ -1,7 +0,0 @@
-$(top_builddir)/src/theory/.subdirs: $(top_srcdir)/src/Makefile.am
-       $(AM_V_at)test -d $(top_builddir)/src/theory || mkdir $(top_builddir)/src/theory
-       $(AM_V_at)grep '^THEORIES = ' $(abs_top_srcdir)/src/Makefile.am | cut -d' ' -f3- | tr ' ' "\n" | xargs -I__D__ echo $(abs_top_srcdir)/src/theory/__D__/kinds >$(abs_top_builddir)/src/theory/.subdirs.tmp
-       @if ! diff -q $(abs_top_builddir)/src/theory/.subdirs $(abs_top_builddir)/src/theory/.subdirs.tmp &>/dev/null; then \
-               echo "  GEN   " $@; \
-               $(am__mv) $(abs_top_builddir)/src/theory/.subdirs.tmp $(abs_top_builddir)/src/theory/.subdirs; \
-       fi