diff options
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | Makefile.am | 8 | ||||
| -rw-r--r-- | Makefile.builds | 23 | ||||
| -rw-r--r-- | Makefile.builds.in | 39 | ||||
| -rw-r--r-- | configure.ac | 33 | ||||
| -rw-r--r-- | src/Makefile.am | 27 | ||||
| -rw-r--r-- | src/include/cvc4_config.h | 50 | ||||
| -rw-r--r-- | src/main/Makefile.am | 2 | ||||
| -rw-r--r-- | src/parser/Makefile.am | 33 | ||||
| -rw-r--r-- | src/parser/parser.cpp | 1 | ||||
| -rw-r--r-- | src/parser/smt/Makefile.am | 2 |
11 files changed, 145 insertions, 77 deletions
@@ -1,5 +1,5 @@ -.PHONY: default -default: all +.PHONY: _default_build_ +_default_build_: all %: @if test -e builds; then \ echo cd builds; \ diff --git a/Makefile.am b/Makefile.am index 02d9e1bea..76130be45 100644 --- a/Makefile.am +++ b/Makefile.am @@ -6,7 +6,7 @@ ACLOCAL_AMFLAGS = -I config SUBDIRS = src test doc contrib .PHONY: production debug default competition -production: ; @srcdir@/configure --with-build=production && $(MAKE) -debug: ; @srcdir@/configure --with-build=debug && $(MAKE) -default: ; @srcdir@/configure --with-build=default && $(MAKE) -competition:; @srcdir@/configure --with-build=competition && $(MAKE) +production: ; (cd @top_srcdir@ && ./configure --with-build=production && $(MAKE)) +debug: ; (cd @top_srcdir@ && ./configure --with-build=debug && $(MAKE)) +default: ; (cd @top_srcdir@ && ./configure --with-build=default && $(MAKE)) +competition:; (cd @top_srcdir@ && ./configure --with-build=competition && $(MAKE)) diff --git a/Makefile.builds b/Makefile.builds deleted file mode 100644 index 0fb07765b..000000000 --- a/Makefile.builds +++ /dev/null @@ -1,23 +0,0 @@ -include current - -.PHONY: default -default: all -all: - @if (cd $(CURRENT_BUILD) && $(MAKE) $@); then \ - mkdir -pv bin lib; \ - echo $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la `pwd`/lib; \ - $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la `pwd`/lib; \ - echo $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la `pwd`/lib; \ - $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la `pwd`/lib; \ - echo "libdir=`pwd`/lib; progdir=`pwd`/bin; file=cvc4"; \ - libdir=`pwd`/lib; progdir=`pwd`/bin; file=cvc4; \ - echo `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$libdir -Wl,-rpath:'`; \ - eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$libdir -Wl,-rpath:'`; \ - echo "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \ - eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \ - else \ - echo Build failure.; \ - fi - -%: - (cd $(CURRENT_BUILD) && $(MAKE) $@) diff --git a/Makefile.builds.in b/Makefile.builds.in new file mode 100644 index 000000000..f6e17b4ca --- /dev/null +++ b/Makefile.builds.in @@ -0,0 +1,39 @@ +# -*- makefile -*- + +include current + +@SET_MAKE@ + +install_sh = @install_sh@ +mkinstalldirs = $(install_sh) -d +exec_prefix = @exec_prefix@ +prefix = @prefix@ +bindir = @bindir@ +libdir = @libdir@ +abs_builddir = @abs_builddir@ + +.PHONY: _default_build_ +_default_build_: all +all: + (cd $(CURRENT_BUILD) && $(MAKE) $@) + # populate builds/$(CURRENT_BUILD)/bin and builds/$(CURRENT_BUILD)/lib + $(mkinstalldirs) "$(CURRENT_BUILD)$(bindir)" "$(CURRENT_BUILD)$(libdir)" + $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "$(abs_builddir)$(libdir)" + $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "$(abs_builddir)$(libdir)" + thelibdir="$(abs_builddir)$(libdir)"; progdir="$(abs_builddir)$(bindir)"; file=cvc4; \ + eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \ + eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)" + ln -sfv "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/lib + ln -sfv "$(abs_builddir)$(bindir)" $(CURRENT_BUILD)/bin + # populate builds/bin and builds/lib + mkdir -pv ".$(bindir)" ".$(libdir)" + $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)" + $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)" + thelibdir="`pwd`$(libdir)"; progdir="`pwd`$(bindir)"; file=cvc4; \ + eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \ + eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)" + ln -sfv ".$(libdir)" lib + ln -sfv ".$(bindir)" bin + +%: + (cd $(CURRENT_BUILD) && $(MAKE) $@) diff --git a/configure.ac b/configure.ac index c7f461128..f4320aeb4 100644 --- a/configure.ac +++ b/configure.ac @@ -7,6 +7,11 @@ AC_CONFIG_AUX_DIR([config]) #AC_CONFIG_LIBOBJ_DIR([lib]) AC_CONFIG_MACRO_DIR([config]) +CVC4_RELEASE=prerelease +CVC4_LIBRARY_RELEASE_CODE=0:0:0 +CVC4_LIBRARY_VERSION=0:0:0 +CVC4_PARSER_LIBRARY_VERSION=0:0:0 + # really irritating: AC_CANONICAL_* bash $@ config_cmdline="$@" @@ -92,11 +97,15 @@ if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then AC_MSG_RESULT([this one (in builds/)]) elif test -e src/include/cvc4.h; then AC_MSG_RESULT([builds/$target/$build_type]) - rm -f config.log config.status confdefs.h - mkdir -p "builds/$target/$build_type" - test -e builds/Makefile || ln -sf ../Makefile.builds builds/Makefile - echo "CURRENT_BUILD = $target/$build_type" > builds/current echo + echo Setting up "builds/$target/$build_type"... + rm -fv config.log config.status confdefs.h + mkdir -pv "builds/$target/$build_type" + test -e builds/Makefile || ln -sfv "$target/$build_type/Makefile.builds" builds/Makefile + echo Creating builds/current... + (echo "# This is the most-recently-configured CVC4 build"; \ + echo "# 'make' in the top-level source directory applies to this build"; \ + echo "CURRENT_BUILD = $target/$build_type") > builds/current echo cd "builds/$target/$build_type" cd "builds/$target/$build_type" CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS @@ -216,7 +225,7 @@ if test "$enable_profiling" = yes; then CVC4LDFLAGS="$CVC4LDFLAGS -pg" fi -AM_INIT_AUTOMAKE(cvc4, prerelease) +AM_INIT_AUTOMAKE(cvc4, $CVC4_RELEASE) AC_CONFIG_HEADERS([config.h]) # keep track of whether the user set these (check here, because @@ -301,8 +310,9 @@ fi # Checks for libraries. AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])]) # Check for antlr C++ runtime (defined in config/antlr.m4) -AC_LIB_ANTLR - +if test "$enable_antlr" = yes; then + AC_LIB_ANTLR +fi # Checks for header files. AC_CHECK_HEADERS([getopt.h unistd.h]) @@ -320,6 +330,9 @@ AC_TYPE_SIZE_T # Prepare configure output +AC_SUBST(CVC4_LIBRARY_RELEASE_CODE) +AC_SUBST(CVC4_LIBRARY_VERSION) +AC_SUBST(CVC4_PARSER_LIBRARY_VERSION) if test "$user_cppflags" = no; then CPPFLAGS="$CVC4CPPFLAGS" fi @@ -331,6 +344,7 @@ if test "$user_ldflags" = no; then fi AC_CONFIG_FILES([ + Makefile.builds Makefile contrib/Makefile doc/Makefile @@ -384,7 +398,10 @@ CPPFLAGS : $CPPFLAGS CXXFLAGS : $CXXFLAGS LDFLAGS : $LDFLAGS -Using ANTLR parsers: $enable_antlr +Using ANTLR parsers : $enable_antlr +Library releases : $CVC4_LIBRARY_RELEASE_CODE +libcvc4 version : $CVC4_LIBRARY_VERSION +libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION Now just type make, followed by make check or make install, as you like. diff --git a/src/Makefile.am b/src/Makefile.am index 128e47bd5..afbb587a8 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -1,3 +1,20 @@ +# LIBCVC4_VERSION (-version-info) is in the form current:revision:age +# +# current - +# increment if interfaces have been added, removed or changed +# revision - +# increment if source code has changed +# set to zero if current is incremented +# age - +# increment if interfaces have been added +# set to zero if interfaces have been removed +# or changed +# +# LIBCVC4_RELEASE (-release) should match the CVC4 release version +# +LIBCVC4_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@ +LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@ + INCLUDES = -I@srcdir@/include -I@srcdir@ AM_CXXFLAGS = -Wall -fvisibility=hidden AM_CPPFLAGS = -D__BUILDING_CVC4LIB @@ -6,6 +23,8 @@ SUBDIRS = util expr context prop smt theory . parser main lib_LTLIBRARIES = libcvc4.la +libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION) -release $(LIBCVC4_RELEASE) + libcvc4_la_SOURCES = libcvc4_la_LIBADD = \ @builddir@/util/libutil.la \ @@ -22,10 +41,10 @@ publicheaders = \ include/cvc4_expr.h install-data-local: $(publicheaders) - $(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4; \ - @for f in $(publicheaders); do - echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4" - $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4" + $(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4 + @for f in $(publicheaders); do \ + echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \ + $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \ done include/cvc4.h: smt/smt_engine.h diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h index ccc07b40a..95fac9aaa 100644 --- a/src/include/cvc4_config.h +++ b/src/include/cvc4_config.h @@ -10,35 +10,27 @@ ** [[ Add file-specific comments here ]] **/ -#ifdef __BUILDING_CVC4LIB - -# if defined _WIN32 || defined __CYGWIN__ -# ifdef BUILDING_DLL -# ifdef __GNUC__ -# define CVC4_PUBLIC __attribute__((dllexport)) -# else /* ! __GNUC__ */ -# define CVC4_PUBLIC __declspec(dllexport) -# endif /* __GNUC__ */ -# else /* BUILDING_DLL */ -# ifdef __GNUC__ -# define CVC4_PUBLIC __attribute__((dllimport)) -# else /* ! __GNUC__ */ -# define CVC4_PUBLIC __declspec(dllimport) -# endif /* __GNUC__ */ -# endif /* BUILDING_DLL */ -# else /* !( defined _WIN32 || defined __CYGWIN__ ) */ -# if __GNUC__ >= 4 -# define CVC4_PUBLIC __attribute__ ((visibility("default"))) -# else /* !( __GNUC__ >= 4 ) */ -# define CVC4_PUBLIC -# endif /* __GNUC__ >= 4 */ -# endif /* defined _WIN32 || defined __CYGWIN__ */ - -#else /* ! __BUILDING_CVC4LIB */ - -# define CVC4_PUBLIC - -#endif /* __BUILDING_CVC4LIB */ +#if defined _WIN32 || defined __CYGWIN__ +# ifdef BUILDING_DLL +# ifdef __GNUC__ +# define CVC4_PUBLIC __attribute__((dllexport)) +# else /* ! __GNUC__ */ +# define CVC4_PUBLIC __declspec(dllexport) +# endif /* __GNUC__ */ +# else /* BUILDING_DLL */ +# ifdef __GNUC__ +# define CVC4_PUBLIC __attribute__((dllimport)) +# else /* ! __GNUC__ */ +# define CVC4_PUBLIC __declspec(dllimport) +# endif /* __GNUC__ */ +# endif /* BUILDING_DLL */ +#else /* !( defined _WIN32 || defined __CYGWIN__ ) */ +# if __GNUC__ >= 4 +# define CVC4_PUBLIC __attribute__ ((visibility("default"))) +# else /* !( __GNUC__ >= 4 ) */ +# define CVC4_PUBLIC +# endif /* __GNUC__ >= 4 */ +#endif /* defined _WIN32 || defined __CYGWIN__ */ #define EXPECT_TRUE(x) __builtin_expect( (x), true) #define EXPECT_FALSE(x) __builtin_expect( (x), false) diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 36e4c0342..0992a434a 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -1,6 +1,6 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB +AM_CPPFLAGS = bin_PROGRAMS = cvc4 diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 7eb52d3e9..7e3cee751 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -1,14 +1,37 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES) +# LIBCVC4PARSER_VERSION (-version-info) is in the form current:revision:age +# +# current - +# increment if interfaces have been added, removed or changed +# revision - +# increment if source code has changed +# set to zero if current is incremented +# age - +# increment if interfaces have been added +# set to zero if interfaces have been removed +# or changed +# +# LIBCVC4PARSER_RELEASE (-release) should match the CVC4 release version +# +LIBCVC4PARSER_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@ +LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ + +INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB +AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB if USE_ANTLR SUBDIRS = smt + INCLUDES += $(ANTLR_INCLUDES) endif -nobase_lib_LTLIBRARIES = libcvc4parser.la +lib_LTLIBRARIES = libcvc4parser.la + +libcvc4parser_la_LDFLAGS = -version-info $(LIBCVC4PARSER_VERSION) -release $(LIBCVC4PARSER_RELEASE) + +if USE_ANTLR + libcvc4parser_la_LDFLAGS += $(ANTLR_LDFLAGS) +endif -libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) libcvc4parser_la_LIBADD = \ ../libcvc4.la @@ -22,7 +45,7 @@ libcvc4parser_la_SOURCES = \ smtlib.ypp if USE_ANTLR -libcvc4parser_la_SOURCES += \ + libcvc4parser_la_SOURCES += \ antlr_parser.cpp \ antlr_parser.h endif USE_ANTLR diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 89276872c..cd03f21f2 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -12,6 +12,7 @@ #include <iostream> +#include "cvc4_config.h" #include "parser/parser.h" #include "util/command.h" #include "util/assert.h" diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index bb2018e2e..acb95849f 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -1,6 +1,6 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB +AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB noinst_LTLIBRARIES = libparsersmt.la |