more build system work

diff --git a/Makefile b/Makefile
index efc532a23d690f5bcb4ca8968edabca65643a54c..707f3cda3f21a114bc0be1e511f63f05a4ff587d 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -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 f7390bb05c563f0947ac2445829eef6f07a9c2c5..0fb07765bddef0e8e58cb0e38965b674681dd272 100644 (file)
--- 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 c9e4200da5f8928321c4904f68ae2e47fc3a3170..5f2611c91642e1358178aea6df50af6ec17cbb02 100755 (executable)
--- 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 e19f3c42df2bca57a51b2cb39480a4d88d8cd1ab..fbc4dbe566ad3b883dc6f8169cd8dd36fdd5b67e 100644 (file)
--- 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 068eea929a88bf41a9e17cf24eeab830c5c71ee8..c7f4611281e815bc78592ed6d409f70d4cf7374b 100644 (file)
--- 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 b79eddf8bd67565c5d3bc7ad32467c61143137a4..128e47bd5c59db48d1a45d64d2929c80c1a9f576 100644 (file)
--- 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 (file)
index 0000000..005c3bd
--- /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 d44c970d251fc3caee770c3cab1d5c2e4a46cd58..7eb52d3e9845055f98f8be19865d151ac6869ef9 100644 (file)
--- 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 54e3e9bf961a65e19dd84bf5a49eeec8b12398c4..bb2018e2e7429c186332a94244f3c6699f123ba3 100644 (file)
--- 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