diff options
| -rw-r--r-- | src/Makefile.am | 40 | ||||
| -rw-r--r-- | src/Makefile.theories | 3 | ||||
| -rw-r--r-- | src/expr/Makefile.am | 49 | ||||
| -rwxr-xr-x | src/mksubdirs | 16 | ||||
| -rw-r--r-- | src/theory/Makefile.subdirs | 7 |
5 files changed, 75 insertions, 40 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 95ca44e63..9502afa9c 100644 --- 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 index 000000000..8b5cef4d5 --- /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 13358d294..c5a032abc 100644 --- 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 index 000000000..c96437caa --- /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 index 42582c67f..000000000 --- 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 |