diff options
| -rw-r--r-- | Makefile | 7 | ||||
| -rw-r--r-- | Makefile.builds | 21 | ||||
| -rwxr-xr-x | autogen.sh | 1 | ||||
| -rw-r--r-- | config/antlr.m4 | 4 | ||||
| -rw-r--r-- | configure.ac | 19 | ||||
| -rw-r--r-- | src/Makefile.am | 14 | ||||
| -rw-r--r-- | src/context/context.cpp | 13 | ||||
| -rw-r--r-- | src/parser/Makefile.am | 14 | ||||
| -rw-r--r-- | src/parser/smt/Makefile.am | 14 |
9 files changed, 82 insertions, 25 deletions
@@ -1,10 +1,11 @@ .PHONY: default -default: +default: all +%: @if test -e builds; then \ echo cd builds; \ cd builds; \ - echo $(MAKE); \ - $(MAKE); \ + echo $(MAKE) $@; \ + $(MAKE) $@; \ else \ echo; \ echo 'Run configure first, or type "make" in a configured build directory.'; \ diff --git a/Makefile.builds b/Makefile.builds index f7390bb05..0fb07765b 100644 --- a/Makefile.builds +++ b/Makefile.builds @@ -1,4 +1,23 @@ include current .PHONY: default -default:; cd "$(CURRENT_BUILD)" && $(MAKE) +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/autogen.sh b/autogen.sh index c9e4200da..5f2611c91 100755 --- a/autogen.sh +++ b/autogen.sh @@ -1,7 +1,6 @@ #!/bin/sh -ex cd "$(dirname "$0")" -mkdir -p config libtoolize --copy autoheader -I config touch NEWS README AUTHORS ChangeLog diff --git a/config/antlr.m4 b/config/antlr.m4 index e19f3c42d..fbc4dbe56 100644 --- a/config/antlr.m4 +++ b/config/antlr.m4 @@ -75,7 +75,7 @@ AC_DEFUN([AC_LIB_ANTLR],[ [ AC_MSG_RESULT(found in $antlr_prefix) ANTLR_INCLUDES="-I$antlr_prefix/include" - ANTLR_LDFLAGS="-L$antlr_prefix/lib -lantlr" + ANTLR_LDFLAGS="-L$antlr_prefix/lib -lantlr-pic" break ], [ @@ -93,4 +93,4 @@ AC_DEFUN([AC_LIB_ANTLR],[ # Define the ANTLR include/libs variables AC_SUBST(ANTLR_INCLUDES) AC_SUBST(ANTLR_LDFLAGS) -])
\ No newline at end of file +]) diff --git a/configure.ac b/configure.ac index 068eea929..c7f461128 100644 --- a/configure.ac +++ b/configure.ac @@ -94,7 +94,7 @@ 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 || cp Makefile.builds builds/Makefile + test -e builds/Makefile || ln -sf ../Makefile.builds builds/Makefile echo "CURRENT_BUILD = $target/$build_type" > builds/current echo echo cd "builds/$target/$build_type" @@ -242,14 +242,23 @@ AC_LIBTOOL_WIN32_DLL # Checks for programs. AC_PROG_CC AC_PROG_CXX - AC_PROG_INSTALL AC_PROG_LIBTOOL AM_PROG_LEX AC_PROG_YACC # Check for ANTLR runantlr script (defined in config/antlr.m4) -AC_PROG_ANTLR +AC_ARG_ENABLE(antlr, AS_HELP_STRING([--enable-antlr],[use Dejan's ANTLR parsers])) +AC_MSG_CHECKING([whether you want to use the ANTLR parsers]) +if test -z "${enable_antlr+set}"; then + enable_antlr=no +fi +AC_MSG_RESULT([$enable_antlr]) +AM_CONDITIONAL(USE_ANTLR, test "$enable_antlr" = yes) +if test "$enable_antlr" = yes; then + AC_PROG_ANTLR + AC_DEFINE(ANTLR_PARSERS, [], [whether we're using ANTLR parsers]) +fi AC_CHECK_PROG(DOXYGEN, doxygen, doxygen, []) if test -z "$DOXYGEN"; then @@ -291,7 +300,7 @@ fi # Checks for libraries. AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])]) -# Chcek for antlr C++ runtime (defined in config/antlr.m4) +# Check for antlr C++ runtime (defined in config/antlr.m4) AC_LIB_ANTLR @@ -375,6 +384,8 @@ CPPFLAGS : $CPPFLAGS CXXFLAGS : $CXXFLAGS LDFLAGS : $LDFLAGS +Using ANTLR parsers: $enable_antlr + Now just type make, followed by make check or make install, as you like. You can use 'make <build_profile>' to reconfig/build a different profile. diff --git a/src/Makefile.am b/src/Makefile.am index b79eddf8b..128e47bd5 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -8,13 +8,13 @@ lib_LTLIBRARIES = libcvc4.la libcvc4_la_SOURCES = libcvc4_la_LIBADD = \ - util/libutil.la \ - expr/libexpr.la \ - context/libcontext.la \ - prop/libprop.la \ - prop/minisat/libminisat.la \ - smt/libsmt.la \ - theory/libtheory.la + @builddir@/util/libutil.la \ + @builddir@/expr/libexpr.la \ + @builddir@/context/libcontext.la \ + @builddir@/prop/libprop.la \ + @builddir@/prop/minisat/libminisat.la \ + @builddir@/smt/libsmt.la \ + @builddir@/theory/libtheory.la publicheaders = \ include/cvc4.h \ diff --git a/src/context/context.cpp b/src/context/context.cpp new file mode 100644 index 000000000..005c3bd6a --- /dev/null +++ b/src/context/context.cpp @@ -0,0 +1,13 @@ +/********************* -*- C++ -*- */ +/** context.cpp + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + **/ + +#include "context/context.h" + diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index d44c970d2..7eb52d3e9 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -1,12 +1,16 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@ $(ANTLR_INCLUDES) +INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -fvisibility=hidden AM_CPPFLAGS = -D__BUILDING_CVC4LIB -SUBDIRS = smt . +if USE_ANTLR + SUBDIRS = smt +endif nobase_lib_LTLIBRARIES = libcvc4parser.la libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) +libcvc4parser_la_LIBADD = \ + ../libcvc4.la libcvc4parser_la_SOURCES = \ parser.cpp \ @@ -15,9 +19,13 @@ libcvc4parser_la_SOURCES = \ pl_scanner.lpp \ pl.ypp \ smtlib_scanner.lpp \ - smtlib.ypp \ + smtlib.ypp + +if USE_ANTLR +libcvc4parser_la_SOURCES += \ antlr_parser.cpp \ antlr_parser.h +endif USE_ANTLR BUILT_SOURCES = \ pl_scanner.cpp \ diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index 54e3e9bf9..bb2018e2e 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -1,6 +1,12 @@ -SOURCES = \ +INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CPPFLAGS = -D__BUILDING_CVC4LIB + +noinst_LTLIBRARIES = libparsersmt.la + +libparsersmt_la_SOURCES = \ SmtLexer.g \ - SmtParser.g + SmtParser.g \ SmtLexer.hpp \ SmtLexer.cpp \ SmtParser.hpp \ @@ -13,7 +19,7 @@ BUILT_SOURCES = \ SmtParser.cpp SmtLexer.cpp SmtLexer.hpp: SmtLexer.g - $(ANTLR) SmtLexer.g + $(ANTLR) @srcdir@/SmtLexer.g SmtParser.cpp SmtParser.hpp: SmtParser.g - $(ANTLR) SmtParser.g + $(ANTLR) @srcdir@/SmtParser.g |