Includes many fixes to build system for Solaris (thanks Tim!), and also
authorMorgan Deters <mdeters@gmail.com>
Wed, 24 Oct 2012 22:24:34 +0000 (22:24 +0000)
committerMorgan Deters <mdeters@gmail.com>
Wed, 24 Oct 2012 22:24:34 +0000 (22:24 +0000)
just in general, and some documentation adjustments.

INSTALL
Makefile.builds.in
config/boost.m4
config/readline.m4
configure.ac
contrib/get-antlr-3.4
src/Makefile.am
src/main/Makefile.am
src/options/Makefile.am
src/options/mkoptions
src/parser/memory_mapped_input_buffer.cpp

diff --git a/INSTALL b/INSTALL
index a9986a073c39144ac6db1715829ccbc42c1fc1c0..d1e3d53a373c9f5a9c02125f60410a3883c0ca1e 100644 (file)
--- a/INSTALL
+++ b/INSTALL
@@ -2,33 +2,6 @@ CVC4 release version 1.0.
 
 *** Quick-start instructions
 
-    ./configure
-    make
-    make check   [optional but a good idea!]
-
-(To build from a repository checkout, see below.)
-
-You can then "make install" to install in the prefix you gave to
-the configure script (/usr/local by default).  ** You should run
-"make check" ** before installation to ensure that CVC4 has been
-built correctly.  In particular, GCC version 4.5.1 seems to have a
-bug in the optimizer that results in incorrect behavior (and wrong
-results) in many builds.  This is a known problem for Minisat, and
-since Minisat is at the core of CVC4, a problem for CVC4.  "make check"
-easily detects this problem (by showing a number of FAILed test cases).
-It is ok if the unit tests aren't run as part of "make check", but all
-system tests and regression tests should pass without incident.
-
-To build API documentation, use "make doc".  Documentation is produced
-under doc/ but is not installed by "make install".
-
-Examples and tutorials are not installed with "make install."  See
-below.
-
-For more information about the build system itself (probably not
-necessary for casual users), see the Appendix at the bottom of this
-file.
-
 *** Build dependences
 
 The following tools and libraries are required to run CVC4. Versions
@@ -69,6 +42,43 @@ may need to remove the --enable-64bit part in the script.  (If you're
 curious, the manual instructions are at
 http://church.cims.nyu.edu/wiki/Developer%27s_Guide#ANTLR3 .)
 
+*** Building CVC4
+
+The hardest build dependence to satisfy is libantlr3c; that's why it
+is explained above.  Problems in satisfying other build dependences are
+explained below.
+
+Once the build dependences are satisfied, you should be able to
+configure, make, make check, and make install without incident:
+
+    ./configure   [use --prefix to specify a prefix; default /usr/local]
+    make
+    make check    [optional but a good idea!]
+
+To build from a repository checkout (rather than a distributed CVC4
+tarball), there are additional dependences; see below.
+
+You can then "make install" to install in the prefix you gave to
+the configure script (/usr/local by default).  ** You should run
+"make check" ** before installation to ensure that CVC4 has been
+built correctly.  In particular, GCC version 4.5.1 seems to have a
+bug in the optimizer that results in incorrect behavior (and wrong
+results) in many builds.  This is a known problem for Minisat, and
+since Minisat is at the core of CVC4, a problem for CVC4.  "make check"
+easily detects this problem (by showing a number of FAILed test cases).
+It is ok if the unit tests aren't run as part of "make check", but all
+system tests and regression tests should pass without incident.
+
+To build API documentation, use "make doc".  Documentation is produced
+under doc/ but is not installed by "make install".
+
+Examples and tutorials are not installed with "make install."  You may
+want to "make install-examples".  See below.
+
+For more information about the build system itself (probably not
+necessary for casual users), see the Appendix at the bottom of this
+file.
+
 *** Installing the Boost C++ base libraries
 
 A Boost package is available on most Linux distributions; check yours
index baf9237b21d08d330547b35a4ddd9c58c4870cd9..274e2c9e77d4731ca512ac082026ae675699b0a4 100644 (file)
@@ -60,11 +60,11 @@ AM_V_mkdir = $(am__v_mkdir_$(V))
 am__v_mkdir_ = $(am__v_mkdir_$(AM_DEFAULT_VERBOSITY))
 am__v_mkdir_0 = @$(am__v_mkdir_noat_0)
 am__v_mkdir_1 = $(am__v_mkdir_noat_1)
-# libtool --mode=install install
+# libtool --mode=install $(install_sh)
 AM_V_ltinstall = $(am__v_ltinstall_$(V))
 am__v_ltinstall_ = $(am__v_ltinstall_$(AM_DEFAULT_VERBOSITY))
-am__v_ltinstall_0 = @$(SHELL) -c 'echo "   LTINS $$1"; $(LIBTOOL) --silent --mode=install install "$$@"' bash
-am__v_ltinstall_1 = $(LIBTOOL) --mode=install install
+am__v_ltinstall_0 = @$(SHELL) -c 'echo "   LTINS $$1"; $(LIBTOOL) --silent --mode=install $(install_sh) "$$@"' bash
+am__v_ltinstall_1 = $(LIBTOOL) --mode=install $(install_sh)
 # install_sh (never prefix with @)
 AM_V_install_sh_noat = $(am__v_install_sh_noat_$(V))
 am__v_install_sh_noat_ = $(am__v_install_sh_noat_$(AM_DEFAULT_VERBOSITY))
@@ -98,7 +98,7 @@ all:
                "$(abs_builddir)$(libdir)"
 ifeq ($(CVC4_BUILD_LIBCOMPAT),yes)
 #      install libcvc4compat
-       $(CURRENT_BUILD)/libtool --mode=install install -v \
+       $(CURRENT_BUILD)/libtool --mode=install $(install_sh) \
                $(CURRENT_BUILD)/src/compat/libcvc4compat.la \
                "$(abs_builddir)$(libdir)"
 endif
@@ -148,7 +148,7 @@ endif
        $(AM_V_ltinstall) $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)"
 ifeq ($(CVC4_BUILD_LIBCOMPAT),yes)
 #      install libcvc4compat
-       $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/compat/libcvc4compat.la "`pwd`$(libdir)"
+       $(CURRENT_BUILD)/libtool --mode=install $(install_sh) $(CURRENT_BUILD)/src/compat/libcvc4compat.la "`pwd`$(libdir)"
 endif
 ifeq ($(BUILDING_SHARED)$(STATIC_BINARY),10)
 #      if we're building shared libs and the binary is not static, relink
index 118abb7ebdead0a1a07f3bd3daa3910f3868481b..6252f966c5a0f46bb656eeafa894511fe3c9a289 100644 (file)
@@ -1,5 +1,5 @@
 # boost.m4: Locate Boost headers and libraries for autoconf-based projects.
-# Copyright (C) 2007, 2008, 2009, 2010  Benoit Sigoure <tsuna@lrde.epita.fr>
+# Copyright (C) 2007, 2008, 2009, 2010, 2011  Benoit Sigoure <tsuna@lrde.epita.fr>
 #
 # This program is free software: you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -22,7 +22,7 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 m4_define([_BOOST_SERIAL], [m4_translit([
-# serial 13
+# serial 16
 ], [#
 ], [])])
 
@@ -45,15 +45,19 @@ m4_define([_BOOST_SERIAL], [m4_translit([
 # Note: THESE MACROS ASSUME THAT YOU USE LIBTOOL.  If you don't, don't worry,
 # simply read the README, it will show you what to do step by step.
 
-m4_pattern_forbid([^_?BOOST_])
+m4_pattern_forbid([^_?(BOOST|Boost)_])
 
 
 # _BOOST_SED_CPP(SED-PROGRAM, PROGRAM,
 #                [ACTION-IF-FOUND], [ACTION-IF-NOT-FOUND])
 # --------------------------------------------------------
 # Same as AC_EGREP_CPP, but leave the result in conftest.i.
-# PATTERN is *not* overquoted, as in AC_EGREP_CPP.  It could be useful
-# to turn this into a macro which extracts the value of any macro.
+#
+# SED-PROGRAM is *not* overquoted, as in AC_EGREP_CPP.  It is expanded
+# in double-quotes, so escape your double quotes.
+#
+# It could be useful to turn this into a macro which extracts the
+# value of any macro.
 m4_define([_BOOST_SED_CPP],
 [AC_LANG_PREPROC_REQUIRE()dnl
 AC_REQUIRE([AC_PROG_SED])dnl
@@ -114,7 +118,7 @@ if test x"$BOOST_ROOT" != x; then
   fi
 fi
 AC_SUBST([DISTCHECK_CONFIGURE_FLAGS],
-         ["$DISTCHECK_CONFIGURE_FLAGS '--with-boost=$with_boost'"])
+         ["$DISTCHECK_CONFIGURE_FLAGS '--with-boost=$with_boost'"])dnl
 boost_save_CPPFLAGS=$CPPFLAGS
   AC_CACHE_CHECK([for Boost headers version >= $boost_version_req_string],
     [boost_cv_inc_path],
@@ -193,7 +197,7 @@ AC_LANG_POP([C++])dnl
         BOOST_CPPFLAGS=
         ;;#(
       *)
-        AC_SUBST([BOOST_CPPFLAGS], ["-I$boost_cv_inc_path"])
+        AC_SUBST([BOOST_CPPFLAGS], ["-I$boost_cv_inc_path"])dnl
         ;;
     esac
   if test x"$boost_cv_inc_path" != xno; then
@@ -202,7 +206,7 @@ AC_LANG_POP([C++])dnl
   AC_CACHE_CHECK([for Boost's header version],
     [boost_cv_lib_version],
     [m4_pattern_allow([^BOOST_LIB_VERSION$])dnl
-     _BOOST_SED_CPP([/^boost-lib-version = /{s///;s/\"//g;p;g;}],
+     _BOOST_SED_CPP([/^boost-lib-version = /{s///;s/\"//g;p;q;}],
                     [#include <boost/version.hpp>
 boost-lib-version = BOOST_LIB_VERSION],
     [boost_cv_lib_version=`cat conftest.i`])])
@@ -296,7 +300,7 @@ AS_VAR_PUSHDEF([Boost_lib], [boost_cv_lib_$1])dnl
 AS_VAR_PUSHDEF([Boost_lib_LDFLAGS], [boost_cv_lib_$1_LDFLAGS])dnl
 AS_VAR_PUSHDEF([Boost_lib_LDPATH], [boost_cv_lib_$1_LDPATH])dnl
 AS_VAR_PUSHDEF([Boost_lib_LIBS], [boost_cv_lib_$1_LIBS])dnl
-BOOST_FIND_HEADER([$3])
+BOOST_FIND_HEADER([$3], [$6])
 boost_save_CPPFLAGS=$CPPFLAGS
 CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS"
 # Now let's try to find the library.  The algorithm is as follows: first look
@@ -378,8 +382,8 @@ for boost_rtopt_ in $boost_rtopt '' -d; do
     boost_tmp_lib=$with_boost
     test x"$with_boost" = x && boost_tmp_lib=${boost_cv_inc_path%/include}
     for boost_ldpath in "$boost_tmp_lib/lib" '' \
-             /opt/local/lib /usr/local/lib /opt/lib /usr/lib \
-             "$with_boost" C:/Boost/lib /lib /usr/lib64 /lib64
+             /opt/local/lib* /usr/local/lib* /opt/lib* /usr/lib* \
+             "$with_boost" C:/Boost/lib /lib*
     do
       test -e "$boost_ldpath" || continue
       boost_save_LDFLAGS=$LDFLAGS
@@ -402,7 +406,7 @@ dnl generated only once above (before we start the for loops).
       LDFLAGS=$boost_save_LDFLAGS
       LIBS=$boost_save_LIBS
       if test x"$Boost_lib" = xyes; then
-        Boost_lib_LDFLAGS="-L$boost_ldpath -R$boost_ldpath"
+        Boost_lib_LDFLAGS="-L$boost_ldpath -Wl,-R$boost_ldpath"
         Boost_lib_LDPATH="$boost_ldpath"
         break 6
       else
@@ -418,15 +422,15 @@ rm -f conftest.$ac_objext
 ])
 case $Boost_lib in #(
   no) _AC_MSG_LOG_CONFTEST
-    m4_if([$6], [],  [AC_MSG_ERROR([cannot find the flags to link with Boost $1])],
-                      [AC_MSG_NOTICE([cannot find the flags to link with Boost $1])])
+    m4_if([$6], [], [AC_MSG_ERROR([cannot find the flags to link with Boost $1])],
+                    [AC_MSG_NOTICE([cannot find the flags to link with Boost $1])])
     $6
     ;;
 esac
-AC_SUBST(AS_TR_CPP([BOOST_$1_LDFLAGS]), [$Boost_lib_LDFLAGS])
-AC_SUBST(AS_TR_CPP([BOOST_$1_LDPATH]), [$Boost_lib_LDPATH])
-AC_SUBST([BOOST_LDPATH], [$Boost_lib_LDPATH])
-AC_SUBST(AS_TR_CPP([BOOST_$1_LIBS]), [$Boost_lib_LIBS])
+AC_SUBST(AS_TR_CPP([BOOST_$1_LDFLAGS]), [$Boost_lib_LDFLAGS])dnl
+AC_SUBST(AS_TR_CPP([BOOST_$1_LDPATH]), [$Boost_lib_LDPATH])dnl
+AC_SUBST([BOOST_LDPATH], [$Boost_lib_LDPATH])dnl
+AC_SUBST(AS_TR_CPP([BOOST_$1_LIBS]), [$Boost_lib_LIBS])dnl
 CPPFLAGS=$boost_save_CPPFLAGS
 AS_VAR_POPDEF([Boost_lib])dnl
 AS_VAR_POPDEF([Boost_lib_LDFLAGS])dnl
@@ -445,17 +449,31 @@ fi
 # The page http://beta.boost.org/doc/libs is useful: it gives the first release
 # version of each library (among other things).
 
+# BOOST_DEFUN(LIBRARY, CODE)
+# --------------------------
+# Define BOOST_<LIBRARY-UPPERCASE> as a macro that runs CODE.
+#
+# Use indir to avoid the warning on underquoted macro name given to AC_DEFUN.
+m4_define([BOOST_DEFUN],
+[m4_indir([AC_DEFUN],
+          m4_toupper([BOOST_$1]),
+[m4_pushdef([BOOST_Library], [$1])dnl
+$2
+m4_popdef([BOOST_Library])dnl
+])
+])
+
 # BOOST_ARRAY()
 # -------------
 # Look for Boost.Array
-AC_DEFUN([BOOST_ARRAY],
+BOOST_DEFUN([Array],
 [BOOST_FIND_HEADER([boost/array.hpp])])
 
 
 # BOOST_ASIO()
 # ------------
 # Look for Boost.Asio (new in Boost 1.35).
-AC_DEFUN([BOOST_ASIO],
+BOOST_DEFUN([Asio],
 [AC_REQUIRE([BOOST_SYSTEM])dnl
 BOOST_FIND_HEADER([boost/asio.hpp])])
 
@@ -463,14 +481,41 @@ BOOST_FIND_HEADER([boost/asio.hpp])])
 # BOOST_BIND()
 # ------------
 # Look for Boost.Bind
-AC_DEFUN([BOOST_BIND],
+BOOST_DEFUN([Bind],
 [BOOST_FIND_HEADER([boost/bind.hpp])])
 
 
+# BOOST_CHRONO()
+# ------------------
+# Look for Boost.Chrono
+BOOST_DEFUN([Chrono],
+[# Do we have to check for Boost.System?  This link-time dependency was
+# added as of 1.35.0.  If we have a version <1.35, we must not attempt to
+# find Boost.System as it didn't exist by then.
+if test $boost_major_version -ge 135; then
+BOOST_SYSTEM([$1])
+fi # end of the Boost.System check.
+boost_filesystem_save_LIBS=$LIBS
+boost_filesystem_save_LDFLAGS=$LDFLAGS
+m4_pattern_allow([^BOOST_SYSTEM_(LIBS|LDFLAGS)$])dnl
+LIBS="$LIBS $BOOST_SYSTEM_LIBS"
+LDFLAGS="$LDFLAGS $BOOST_SYSTEM_LDFLAGS"
+BOOST_FIND_LIB([chrono], [$1],
+                [boost/chrono.hpp],
+                [boost::chrono::thread_clock d;])
+if test $enable_static_boost = yes && test $boost_major_version -ge 135; then
+    AC_SUBST([BOOST_FILESYSTEM_LIBS], ["$BOOST_FILESYSTEM_LIBS $BOOST_SYSTEM_LIBS"])
+fi
+LIBS=$boost_filesystem_save_LIBS
+LDFLAGS=$boost_filesystem_save_LDFLAGS
+
+])# BOOST_CHRONO
+
+
 # BOOST_CONVERSION()
 # ------------------
 # Look for Boost.Conversion (cast / lexical_cast)
-AC_DEFUN([BOOST_CONVERSION],
+BOOST_DEFUN([Conversion],
 [BOOST_FIND_HEADER([boost/cast.hpp])
 BOOST_FIND_HEADER([boost/lexical_cast.hpp])
 ])# BOOST_CONVERSION
@@ -480,7 +525,7 @@ BOOST_FIND_HEADER([boost/lexical_cast.hpp])
 # -----------------------------------
 # Look for Boost.Date_Time.  For the documentation of PREFERRED-RT-OPT, see the
 # documentation of BOOST_FIND_LIB above.
-AC_DEFUN([BOOST_DATE_TIME],
+BOOST_DEFUN([Date_Time],
 [BOOST_FIND_LIB([date_time], [$1],
                 [boost/date_time/posix_time/posix_time.hpp],
                 [boost::posix_time::ptime t;])
@@ -493,7 +538,7 @@ AC_DEFUN([BOOST_DATE_TIME],
 # the documentation of BOOST_FIND_LIB above.
 # Do not check for boost/filesystem.hpp because this file was introduced in
 # 1.34.
-AC_DEFUN([BOOST_FILESYSTEM],
+BOOST_DEFUN([Filesystem],
 [# Do we have to check for Boost.System?  This link-time dependency was
 # added as of 1.35.0.  If we have a version <1.35, we must not attempt to
 # find Boost.System as it didn't exist by then.
@@ -507,6 +552,9 @@ LIBS="$LIBS $BOOST_SYSTEM_LIBS"
 LDFLAGS="$LDFLAGS $BOOST_SYSTEM_LDFLAGS"
 BOOST_FIND_LIB([filesystem], [$1],
                 [boost/filesystem/path.hpp], [boost::filesystem::path p;])
+if test $enable_static_boost = yes && test $boost_major_version -ge 135; then
+    AC_SUBST([BOOST_FILESYSTEM_LIBS], ["$BOOST_FILESYSTEM_LIBS $BOOST_SYSTEM_LIBS"])
+fi
 LIBS=$boost_filesystem_save_LIBS
 LDFLAGS=$boost_filesystem_save_LDFLAGS
 ])# BOOST_FILESYSTEM
@@ -515,7 +563,7 @@ LDFLAGS=$boost_filesystem_save_LDFLAGS
 # BOOST_FOREACH()
 # ---------------
 # Look for Boost.Foreach
-AC_DEFUN([BOOST_FOREACH],
+BOOST_DEFUN([Foreach],
 [BOOST_FIND_HEADER([boost/foreach.hpp])])
 
 
@@ -526,14 +574,14 @@ AC_DEFUN([BOOST_FOREACH],
 # standalone.  It can't be compiled because it triggers the following error:
 # boost/format/detail/config_macros.hpp:88: error: 'locale' in namespace 'std'
 #                                                  does not name a type
-AC_DEFUN([BOOST_FORMAT],
+BOOST_DEFUN([Format],
 [BOOST_FIND_HEADER([boost/format.hpp])])
 
 
 # BOOST_FUNCTION()
 # ----------------
 # Look for Boost.Function
-AC_DEFUN([BOOST_FUNCTION],
+BOOST_DEFUN([Function],
 [BOOST_FIND_HEADER([boost/function.hpp])])
 
 
@@ -541,17 +589,17 @@ AC_DEFUN([BOOST_FUNCTION],
 # -------------------------------
 # Look for Boost.Graphs.  For the documentation of PREFERRED-RT-OPT, see the
 # documentation of BOOST_FIND_LIB above.
-AC_DEFUN([BOOST_GRAPH],
+BOOST_DEFUN([Graph],
 [BOOST_FIND_LIB([graph], [$1],
                 [boost/graph/adjacency_list.hpp], [boost::adjacency_list<> g;])
 ])# BOOST_GRAPH
 
 
 # BOOST_IOSTREAMS([PREFERRED-RT-OPT])
-# -------------------------------
+# -----------------------------------
 # Look for Boost.IOStreams.  For the documentation of PREFERRED-RT-OPT, see the
 # documentation of BOOST_FIND_LIB above.
-AC_DEFUN([BOOST_IOSTREAMS],
+BOOST_DEFUN([IOStreams],
 [BOOST_FIND_LIB([iostreams], [$1],
                 [boost/iostreams/device/file_descriptor.hpp],
                 [boost::iostreams::file_descriptor fd; fd.close();])
@@ -561,17 +609,40 @@ AC_DEFUN([BOOST_IOSTREAMS],
 # BOOST_HASH()
 # ------------
 # Look for Boost.Functional/Hash
-AC_DEFUN([BOOST_HASH],
+BOOST_DEFUN([Hash],
 [BOOST_FIND_HEADER([boost/functional/hash.hpp])])
 
 
 # BOOST_LAMBDA()
 # --------------
 # Look for Boost.Lambda
-AC_DEFUN([BOOST_LAMBDA],
+BOOST_DEFUN([Lambda],
 [BOOST_FIND_HEADER([boost/lambda/lambda.hpp])])
 
 
+# BOOST_LOG([PREFERRED-RT-OPT])
+# -----------------------------
+# Look for Boost.Log For the documentation of PREFERRED-RT-OPT, see the
+# documentation of BOOST_FIND_LIB above.
+BOOST_DEFUN([Log],
+[BOOST_FIND_LIB([log], [$1],
+    [boost/log/core/core.hpp],
+    [boost::log::attribute a; a.get_value();])
+])# BOOST_LOG
+
+
+# BOOST_LOG_SETUP([PREFERRED-RT-OPT])
+# -----------------------------------
+# Look for Boost.Log For the documentation of PREFERRED-RT-OPT, see the
+# documentation of BOOST_FIND_LIB above.
+BOOST_DEFUN([Log_Setup],
+[AC_REQUIRE([BOOST_LOG])dnl
+BOOST_FIND_LIB([log_setup], [$1],
+    [boost/log/utility/init/from_settings.hpp],
+    [boost::log::basic_settings<char> bs; bs.empty();])
+])# BOOST_LOG_SETUP
+
+
 # BOOST_MATH()
 # ------------
 # Look for Boost.Math
@@ -580,21 +651,21 @@ AC_DEFUN([BOOST_LAMBDA],
 # libboost_math_c99f, libboost_math_c99l, libboost_math_tr1,
 # libboost_math_tr1f, libboost_math_tr1l).  This macro must be fixed to do the
 # right thing anyway.
-AC_DEFUN([BOOST_MATH],
+BOOST_DEFUN([Math],
 [BOOST_FIND_HEADER([boost/math/special_functions.hpp])])
 
 
 # BOOST_MULTIARRAY()
 # ------------------
 # Look for Boost.MultiArray
-AC_DEFUN([BOOST_MULTIARRAY],
+BOOST_DEFUN([MultiArray],
 [BOOST_FIND_HEADER([boost/multi_array.hpp])])
 
 
 # BOOST_NUMERIC_CONVERSION()
 # --------------------------
 # Look for Boost.NumericConversion (policy-based numeric conversion)
-AC_DEFUN([BOOST_NUMERIC_CONVERSION],
+BOOST_DEFUN([Numeric_Conversion],
 [BOOST_FIND_HEADER([boost/numeric/conversion/converter.hpp])
 ])# BOOST_NUMERIC_CONVERSION
 
@@ -602,32 +673,76 @@ AC_DEFUN([BOOST_NUMERIC_CONVERSION],
 # BOOST_OPTIONAL()
 # ----------------
 # Look for Boost.Optional
-AC_DEFUN([BOOST_OPTIONAL],
+BOOST_DEFUN([Optional],
 [BOOST_FIND_HEADER([boost/optional.hpp])])
 
 
 # BOOST_PREPROCESSOR()
 # --------------------
 # Look for Boost.Preprocessor
-AC_DEFUN([BOOST_PREPROCESSOR],
+BOOST_DEFUN([Preprocessor],
 [BOOST_FIND_HEADER([boost/preprocessor/repeat.hpp])])
 
 
+# BOOST_UNORDERED()
+# -----------------
+# Look for Boost.Unordered
+BOOST_DEFUN([Unordered],
+[BOOST_FIND_HEADER([boost/unordered_map.hpp])])
+
+
+# BOOST_UUID()
+# ------------
+# Look for Boost.Uuid
+BOOST_DEFUN([Uuid],
+[BOOST_FIND_HEADER([boost/uuid/uuid.hpp])])
+
+
 # BOOST_PROGRAM_OPTIONS([PREFERRED-RT-OPT])
 # -----------------------------------------
-# Look for Boost.Program_options.  For the documentation of PREFERRED-RT-OPT, see
-# the documentation of BOOST_FIND_LIB above.
-AC_DEFUN([BOOST_PROGRAM_OPTIONS],
+# Look for Boost.Program_options.  For the documentation of PREFERRED-RT-OPT,
+# see the documentation of BOOST_FIND_LIB above.
+BOOST_DEFUN([Program_Options],
 [BOOST_FIND_LIB([program_options], [$1],
                 [boost/program_options.hpp],
                 [boost::program_options::options_description d("test");])
 ])# BOOST_PROGRAM_OPTIONS
 
 
+
+# _BOOST_PYTHON_CONFIG(VARIABLE, FLAG)
+# ------------------------------------
+# Save VARIABLE, and define it via `python-config --FLAG`.
+# Substitute BOOST_PYTHON_VARIABLE.
+m4_define([_BOOST_PYTHON_CONFIG],
+[AC_SUBST([BOOST_PYTHON_$1],
+          [`python-config --$2 2>/dev/null`])dnl
+boost_python_save_$1=$$1
+$1="$$1 $BOOST_PYTHON_$1"])
+
+
+# BOOST_PYTHON([PREFERRED-RT-OPT])
+# --------------------------------
+# Look for Boost.Python.  For the documentation of PREFERRED-RT-OPT,
+# see the documentation of BOOST_FIND_LIB above.
+BOOST_DEFUN([Python],
+[_BOOST_PYTHON_CONFIG([CPPFLAGS], [includes])
+_BOOST_PYTHON_CONFIG([LDFLAGS],   [ldflags])
+_BOOST_PYTHON_CONFIG([LIBS],      [libs])
+m4_pattern_allow([^BOOST_PYTHON_MODULE$])dnl
+BOOST_FIND_LIB([python], [$1],
+               [boost/python.hpp],
+               [], [BOOST_PYTHON_MODULE(empty) {}])
+CPPFLAGS=$boost_python_save_CPPFLAGS
+LDFLAGS=$boost_python_save_LDFLAGS
+LIBS=$boost_python_save_LIBS
+])# BOOST_PYTHON
+
+
 # BOOST_REF()
 # -----------
 # Look for Boost.Ref
-AC_DEFUN([BOOST_REF],
+BOOST_DEFUN([Ref],
 [BOOST_FIND_HEADER([boost/ref.hpp])])
 
 
@@ -635,7 +750,7 @@ AC_DEFUN([BOOST_REF],
 # -------------------------------
 # Look for Boost.Regex.  For the documentation of PREFERRED-RT-OPT, see the
 # documentation of BOOST_FIND_LIB above.
-AC_DEFUN([BOOST_REGEX],
+BOOST_DEFUN([Regex],
 [BOOST_FIND_LIB([regex], [$1],
                 [boost/regex.hpp],
                 [boost::regex exp("*"); boost::regex_match("foo", exp);])
@@ -646,19 +761,19 @@ AC_DEFUN([BOOST_REGEX],
 # ---------------------------------------
 # Look for Boost.Serialization.  For the documentation of PREFERRED-RT-OPT, see
 # the documentation of BOOST_FIND_LIB above.
-AC_DEFUN([BOOST_SERIALIZATION],
+BOOST_DEFUN([Serialization],
 [BOOST_FIND_LIB([serialization], [$1],
                 [boost/archive/text_oarchive.hpp],
                 [std::ostream* o = 0; // Cheap way to get an ostream...
                 boost::archive::text_oarchive t(*o);])
-])# BOOST_SIGNALS
+])# BOOST_SERIALIZATION
 
 
 # BOOST_SIGNALS([PREFERRED-RT-OPT])
 # ---------------------------------
 # Look for Boost.Signals.  For the documentation of PREFERRED-RT-OPT, see the
 # documentation of BOOST_FIND_LIB above.
-AC_DEFUN([BOOST_SIGNALS],
+BOOST_DEFUN([Signals],
 [BOOST_FIND_LIB([signals], [$1],
                 [boost/signal.hpp],
                 [boost::signal<void ()> s;])
@@ -668,7 +783,7 @@ AC_DEFUN([BOOST_SIGNALS],
 # BOOST_SMART_PTR()
 # -----------------
 # Look for Boost.SmartPtr
-AC_DEFUN([BOOST_SMART_PTR],
+BOOST_DEFUN([Smart_Ptr],
 [BOOST_FIND_HEADER([boost/scoped_ptr.hpp])
 BOOST_FIND_HEADER([boost/shared_ptr.hpp])
 ])
@@ -677,14 +792,14 @@ BOOST_FIND_HEADER([boost/shared_ptr.hpp])
 # BOOST_STATICASSERT()
 # --------------------
 # Look for Boost.StaticAssert
-AC_DEFUN([BOOST_STATICASSERT],
+BOOST_DEFUN([StaticAssert],
 [BOOST_FIND_HEADER([boost/static_assert.hpp])])
 
 
 # BOOST_STRING_ALGO()
 # -------------------
 # Look for Boost.StringAlgo
-AC_DEFUN([BOOST_STRING_ALGO],
+BOOST_DEFUN([String_Algo],
 [BOOST_FIND_HEADER([boost/algorithm/string.hpp])
 ])
 
@@ -694,7 +809,7 @@ AC_DEFUN([BOOST_STRING_ALGO],
 # Look for Boost.System.  For the documentation of PREFERRED-RT-OPT, see the
 # documentation of BOOST_FIND_LIB above.  This library was introduced in Boost
 # 1.35.0.
-AC_DEFUN([BOOST_SYSTEM],
+BOOST_DEFUN([System],
 [BOOST_FIND_LIB([system], [$1],
                 [boost/system/error_code.hpp],
                 [boost::system::error_code e; e.clear();])
@@ -705,7 +820,7 @@ AC_DEFUN([BOOST_SYSTEM],
 # ------------------------------
 # Look for Boost.Test.  For the documentation of PREFERRED-RT-OPT, see the
 # documentation of BOOST_FIND_LIB above.
-AC_DEFUN([BOOST_TEST],
+BOOST_DEFUN([Test],
 [m4_pattern_allow([^BOOST_CHECK$])dnl
 BOOST_FIND_LIB([unit_test_framework], [$1],
                [boost/test/unit_test.hpp], [BOOST_CHECK(2 == 2);],
@@ -721,25 +836,49 @@ BOOST_FIND_LIB([unit_test_framework], [$1],
 # documentation of BOOST_FIND_LIB above.  If ACTION-IF-NOT-FOUND is given,
 # errors are non-fatal; if it's absent, errors are fatal.
 # FIXME: Provide an alias "BOOST_THREAD".
-AC_DEFUN([BOOST_THREADS],
+BOOST_DEFUN([Threads],
 [dnl Having the pthread flag is required at least on GCC3 where
 dnl boost/thread.hpp would complain if we try to compile without
 dnl -pthread on GNU/Linux.
 AC_REQUIRE([_BOOST_PTHREAD_FLAG])dnl
 boost_threads_save_LIBS=$LIBS
+boost_threads_save_LDFLAGS=$LDFLAGS
 boost_threads_save_CPPFLAGS=$CPPFLAGS
-LIBS="$LIBS $boost_cv_pthread_flag"
+# Link-time dependency from thread to system was added as of 1.49.0.
+if test $boost_major_version -ge 149; then
+BOOST_SYSTEM([$1])
+fi # end of the Boost.System check.
+m4_pattern_allow([^BOOST_SYSTEM_(LIBS|LDFLAGS)$])dnl
+LIBS="$LIBS $BOOST_SYSTEM_LIBS $boost_cv_pthread_flag"
+LDFLAGS="$LDFLAGS $BOOST_SYSTEM_LDFLAGS"
 # Yes, we *need* to put the -pthread thing in CPPFLAGS because with GCC3,
 # boost/thread.hpp will trigger a #error if -pthread isn't used:
 #   boost/config/requires_threads.hpp:47:5: #error "Compiler threading support
 #   is not turned on. Please set the correct command line options for
 #   threading: -pthread (Linux), -pthreads (Solaris) or -mthreads (Mingw32)"
 CPPFLAGS="$CPPFLAGS $boost_cv_pthread_flag"
-BOOST_FIND_LIB([thread], [$1],
-                [boost/thread.hpp], [boost::thread t; boost::mutex m;], [], [$2])
-BOOST_THREAD_LIBS="$BOOST_THREAD_LIBS $boost_cv_pthread_flag"
+
+# When compiling for the Windows platform, the threads library is named
+# differently.
+case $host_os in
+  (*mingw*)
+    BOOST_FIND_LIB([thread_win32], [$1],
+                   [boost/thread.hpp], [boost::thread t; boost::mutex m;], [], [$2])
+    BOOST_THREAD_LDFLAGS=$BOOST_THREAD_WIN32_LDFLAGS
+    BOOST_THREAD_LDPATH=$BOOST_THREAD_WIN32_LDPATH
+    BOOST_THREAD_LIBS=$BOOST_THREAD_WIN32_LIBS
+  ;;
+  (*)
+    BOOST_FIND_LIB([thread], [$1],
+                   [boost/thread.hpp], [boost::thread t; boost::mutex m;], [], [$2])
+  ;;
+esac
+
+BOOST_THREAD_LIBS="$BOOST_THREAD_LIBS $BOOST_SYSTEM_LIBS $boost_cv_pthread_flag"
+BOOST_THREAD_LDFLAGS="$BOOST_SYSTEM_LDFLAGS"
 BOOST_CPPFLAGS="$BOOST_CPPFLAGS $boost_cv_pthread_flag"
 LIBS=$boost_threads_save_LIBS
+LDFLAGS=$boost_threads_save_LDFLAGS
 CPPFLAGS=$boost_threads_save_CPPFLAGS
 ])# BOOST_THREADS
 
@@ -747,14 +886,14 @@ CPPFLAGS=$boost_threads_save_CPPFLAGS
 # BOOST_TOKENIZER()
 # -----------------
 # Look for Boost.Tokenizer
-AC_DEFUN([BOOST_TOKENIZER],
+BOOST_DEFUN([Tokenizer],
 [BOOST_FIND_HEADER([boost/tokenizer.hpp])])
 
 
 # BOOST_TRIBOOL()
 # ---------------
 # Look for Boost.Tribool
-AC_DEFUN([BOOST_TRIBOOL],
+BOOST_DEFUN([Tribool],
 [BOOST_FIND_HEADER([boost/logic/tribool_fwd.hpp])
 BOOST_FIND_HEADER([boost/logic/tribool.hpp])
 ])
@@ -763,14 +902,14 @@ BOOST_FIND_HEADER([boost/logic/tribool.hpp])
 # BOOST_TUPLE()
 # -------------
 # Look for Boost.Tuple
-AC_DEFUN([BOOST_TUPLE],
+BOOST_DEFUN([Tuple],
 [BOOST_FIND_HEADER([boost/tuple/tuple.hpp])])
 
 
 # BOOST_TYPETRAITS()
 # --------------------
 # Look for Boost.TypeTraits
-AC_DEFUN([BOOST_TYPETRAITS],
+BOOST_DEFUN([TypeTraits],
 [BOOST_FIND_HEADER([boost/type_traits.hpp])])
 
 
@@ -778,14 +917,14 @@ AC_DEFUN([BOOST_TYPETRAITS],
 # ---------------
 # Look for Boost.Utility (noncopyable, result_of, base-from-member idiom,
 # etc.)
-AC_DEFUN([BOOST_UTILITY],
+BOOST_DEFUN([Utility],
 [BOOST_FIND_HEADER([boost/utility.hpp])])
 
 
 # BOOST_VARIANT()
 # ---------------
 # Look for Boost.Variant.
-AC_DEFUN([BOOST_VARIANT],
+BOOST_DEFUN([Variant],
 [BOOST_FIND_HEADER([boost/variant/variant_fwd.hpp])
 BOOST_FIND_HEADER([boost/variant.hpp])])
 
@@ -796,15 +935,15 @@ BOOST_FIND_HEADER([boost/variant.hpp])])
 # call BOOST_THREADS first.
 # Look for Boost.Wave.  For the documentation of PREFERRED-RT-OPT, see the
 # documentation of BOOST_FIND_LIB above.
-AC_DEFUN([BOOST_WAVE],
+BOOST_DEFUN([Wave],
 [AC_REQUIRE([BOOST_FILESYSTEM])dnl
 AC_REQUIRE([BOOST_DATE_TIME])dnl
 boost_wave_save_LIBS=$LIBS
 boost_wave_save_LDFLAGS=$LDFLAGS
 m4_pattern_allow([^BOOST_((FILE)?SYSTEM|DATE_TIME|THREAD)_(LIBS|LDFLAGS)$])dnl
-LIBS="$LIBS $BOOST_SYSTEM_LIBS $BOOST_FILESYSTEM_LIBS $BOOST_DATE_TIME_LIBS\
+LIBS="$LIBS $BOOST_SYSTEM_LIBS $BOOST_FILESYSTEM_LIBS $BOOST_DATE_TIME_LIBS \
 $BOOST_THREAD_LIBS"
-LDFLAGS="$LDFLAGS $BOOST_SYSTEM_LDFLAGS $BOOST_FILESYSTEM_LDFLAGS\
+LDFLAGS="$LDFLAGS $BOOST_SYSTEM_LDFLAGS $BOOST_FILESYSTEM_LDFLAGS \
 $BOOST_DATE_TIME_LDFLAGS $BOOST_THREAD_LDFLAGS"
 BOOST_FIND_LIB([wave], [$1],
                 [boost/wave.hpp],
@@ -817,7 +956,7 @@ LDFLAGS=$boost_wave_save_LDFLAGS
 # BOOST_XPRESSIVE()
 # -----------------
 # Look for Boost.Xpressive (new since 1.36.0).
-AC_DEFUN([BOOST_XPRESSIVE],
+BOOST_DEFUN([Xpressive],
 [BOOST_FIND_HEADER([boost/xpressive/xpressive.hpp])])
 
 
@@ -924,6 +1063,9 @@ if test x$boost_cv_inc_path != xno; then
   # I'm not sure about my test for `il' (be careful: Intel's ICC pre-defines
   # the same defines as GCC's).
   for i in \
+    _BOOST_gcc_test(4, 8) \
+    _BOOST_gcc_test(4, 7) \
+    _BOOST_gcc_test(4, 6) \
     _BOOST_gcc_test(4, 5) \
     _BOOST_gcc_test(4, 4) \
     _BOOST_gcc_test(4, 3) \
index 90785c7a0523d1cfc68efa5b8e3b6c2abdd22a4a..95783628511b0df7969cca29c7020dc9727da38e 100644 (file)
@@ -70,6 +70,7 @@ fi
 # Try AC_CHECK_LIB(readline) with the given linking libraries
 AC_DEFUN([CVC4_TRY_READLINE_WITH], [
 if test -z "$READLINE_LIBS"; then
+  unset ac_cv_lib_readline_readline
   AC_CHECK_LIB([readline], [readline],
                [AC_CHECK_HEADER([readline/readline.h],
                   [READLINE_LIBS="-lreadline $1"],
index 5e4d3a37194a08223b236b195506fdafb2b55ad6..f94f07419495beaa1e300f1483c8e1ee543be3c0 100644 (file)
@@ -379,6 +379,7 @@ echo ./config.status "\$@"
 EOF
     chmod +x config.reconfig
   fi
+  ln -sf "builds/$target/$build_type/config.log" "config.log"
   exit $exitval
 else
   AC_MSG_RESULT([this one (user-specified)])
@@ -929,7 +930,7 @@ if test "$enable_thread_support" = no; then
   fi
 else
   BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
-                   cvc4_has_threads=no])
+                     cvc4_has_threads=no])
 fi
 LDFLAGS="$cvc4_save_LDFLAGS"
 if test $cvc4_has_threads = no; then
@@ -1129,6 +1130,8 @@ else
   AC_SUBST([CVC4_HAS_THREADS], 0)
 fi
 
+AM_CONDITIONAL([CVC4_NEEDS_REPLACEMENT_FUNCTIONS], [test -n "$LTLIBOBJS"])
+
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
index c56bac7012035de18e759a861f15fccb9b6d86a5..8228c2ace6f714533ec1f3c55814ff3a24c58e06 100755 (executable)
@@ -49,10 +49,10 @@ cd libantlr3c-3.4
 
 if [ ${MACHINE_TYPE} == 'x86_64' ]; then
   # 64-bit stuff here
-  ./configure --enable-64bit --prefix=`pwd`/../..
+  ./configure --enable-64bit --disable-antlrdebug --prefix=`pwd`/../..
 else
   # 32-bit stuff here
-  ./configure --prefix=`pwd`/../..
+  ./configure --disable-antlrdebug --prefix=`pwd`/../..
 fi
 
 cp Makefile Makefile.orig
index 204ea63f85067e2ef24c0342e8541dca03cc2e92..40d3823e96a1de5945baf62f4cf48fe1626370f6 100644 (file)
@@ -44,8 +44,7 @@ libcvc4_la_LIBADD = \
        @builddir@/printer/libprinter.la \
        @builddir@/smt/libsmt.la \
        @builddir@/theory/libtheory.la \
-       @builddir@/decision/libdecision.la \
-       @builddir@/lib/libreplacements.la
+       @builddir@/decision/libdecision.la
 libcvc4_noinst_la_LIBADD = \
        @builddir@/options/liboptions.la \
        @builddir@/util/libutil.la \
@@ -58,8 +57,14 @@ libcvc4_noinst_la_LIBADD = \
        @builddir@/printer/libprinter.la \
        @builddir@/smt/libsmt.la \
        @builddir@/theory/libtheory.la \
-       @builddir@/decision/libdecision.la \
+       @builddir@/decision/libdecision.la
+
+if CVC4_NEEDS_REPLACEMENT_FUNCTIONS
+libcvc4_la_LIBADD += \
        @builddir@/lib/libreplacements.la
+libcvc4_noinst_la_LIBADD += \
+       @builddir@/lib/libreplacements.la
+endif
 
 CLEANFILES = \
        subversion_versioninfo.cpp \
index 6b09fcc27ec057f335778128f4de68ff9209f4ac..952951655132eeceeb5efcb9c49a2c07ef294bd0 100644 (file)
@@ -31,8 +31,11 @@ pcvc4_LDADD = \
        @builddir@/../parser/libcvc4parser.la \
        @builddir@/../libcvc4.la \
        @builddir@/../util/libstatistics.la \
-       @builddir@/../lib/libreplacements.la \
        $(READLINE_LIBS)
+if CVC4_NEEDS_REPLACEMENT_FUNCTIONS
+pcvc4_LDADD += \
+       @builddir@/../lib/libreplacements.la
+endif
 pcvc4_CPPFLAGS = $(AM_CPPFLAGS) $(BOOST_CPPFLAGS) -DPORTFOLIO_BUILD
 pcvc4_LDADD += $(BOOST_THREAD_LIBS) -lpthread
 pcvc4_LDADD += $(BOOST_THREAD_LDFLAGS)
@@ -53,8 +56,11 @@ cvc4_LDADD = \
        @builddir@/../parser/libcvc4parser.la \
        @builddir@/../libcvc4.la \
        @builddir@/../util/libstatistics.la \
-       @builddir@/../lib/libreplacements.la \
        $(READLINE_LIBS)
+if CVC4_NEEDS_REPLACEMENT_FUNCTIONS
+cvc4_LDADD += \
+       @builddir@/../lib/libreplacements.la
+endif
 
 BUILT_SOURCES = \
        $(TOKENS_FILES)
index 155c1b249c0bd6d42360a08f212b40f181b8feaa..7f7fe78cd721551e7a17d4f1acc6a4772e2fb2bd 100644 (file)
@@ -157,7 +157,7 @@ endif
 Debug_tags.tmp Trace_tags.tmp:
        $(AM_V_GEN)\
        grep '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \
-               `find @srcdir@/../ -name "*.cpp" -or -name "*.h" -or -name "*.cc" -or -name "*.g"` | \
+               `find @srcdir@/../ -name "*.cpp" -o -name "*.h" -o -name "*.cc" -o -name "*.g"` | \
        sed 's/^$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | LC_ALL=C sort | uniq >"$@"
 
 MOSTLYCLEANFILES = \
index 9ef05c1b2d83e58d2cfe599338cc5995b62d8533..0632cb3f9947fb9997eb9942d1aae0de85f41e7f 100755 (executable)
@@ -253,7 +253,7 @@ function handle_option {
 
   # scan ahead to see where the type is
   type_pos=2
-  while [ $(($type_pos+1)) -lt ${#args[@]} ] && ! expr "${args[$(($type_pos+1))]}" : ":" &>/dev/null; do
+  while [ $(($type_pos+1)) -lt ${#args[@]} ] && ! expr "${args[$(($type_pos+1))]}" : '\:' &>/dev/null; do
     let ++type_pos
   done
 
@@ -270,13 +270,13 @@ function handle_option {
   else
     i=2
     while [ $i -lt $type_pos ]; do
-      if expr "${args[$i]}" : '--' &>/dev/null || expr "${args[$i]}" : '/--' &>/dev/null; then
+      if expr "${args[$i]}" : '\--' &>/dev/null || expr "${args[$i]}" : '/--' &>/dev/null; then
         if [ -n "$long_option" -o -n "$long_option_alternate" ]; then
           ERR "malformed option line for \`$internal': unexpected \`${args[$i]}'"
         fi
         long_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
         if [ -n "$long_option" ]; then
-          if ! expr "$long_option" : '--.' &>/dev/null; then
+          if ! expr "$long_option" : '\--.' &>/dev/null; then
             ERR "bad long option \`$long_option': expected something like \`--foo'"
           fi
           long_option="$(echo "$long_option" | sed 's,^--,,')"
@@ -285,27 +285,27 @@ function handle_option {
           long_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')"
           long_option_alternate_set=set
           if [ -n "$long_option_alternate" ]; then
-            if ! expr "$long_option_alternate" : '--.' &>/dev/null; then
+            if ! expr "$long_option_alternate" : '\--.' &>/dev/null; then
               ERR "bad alternate long option \`$long_option_alternate': expected something like \`--foo'"
             fi
             long_option_alternate="$(echo "$long_option_alternate" | sed 's,^--,,')"
           fi
         fi
-      elif expr "${args[$i]}" : '-' &>/dev/null || expr "${args[$i]}" : '/-' &>/dev/null; then
+      elif expr "${args[$i]}" : '\-' &>/dev/null || expr "${args[$i]}" : '/-' &>/dev/null; then
         if [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then
           ERR "malformed option line for \`$internal': unexpected \`${args[$i]}'"
         fi
         short_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
         if [ -n "$short_option" ]; then
-          if ! expr "$short_option" : '-.$' &>/dev/null; then
+          if ! expr "$short_option" : '\-.$' &>/dev/null; then
             ERR "bad short option \`$short_option': expected something like \`-x'"
           fi
           short_option="$(echo "$short_option" | sed 's,^-,,')"
         fi
         if expr "${args[$i]}" : '.*/' &>/dev/null; then
           short_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')"
-          if expr "$short_option_alternate" : - &>/dev/null; then
-            if ! expr "$short_option_alternate" : '-.$' &>/dev/null; then
+          if expr "$short_option_alternate" : '\-' &>/dev/null; then
+            if ! expr "$short_option_alternate" : '\-.$' &>/dev/null; then
               ERR "bad alternate short option \`$short_option_alternate': expected something like \`-x'"
             fi
             short_option_alternate="$(echo "$short_option_alternate" | sed 's,^-,,')"
@@ -396,13 +396,13 @@ function handle_option {
        handlers="${args[$i]}"
        ;;
     :predicate)
-       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
          let ++i
          predicates="${predicates} ${args[$i]}"
        done
        ;;
     :link)
-       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
          let ++i
          link="${args[$i]}"
          if expr "${args[$i]}" : '.*/' &>/dev/null; then
@@ -415,7 +415,7 @@ function handle_option {
        done
        ;;
     :include)
-       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
          let ++i
          module_includes="${module_includes}
 #line $lineno \"$kf\"
@@ -423,7 +423,7 @@ function handle_option {
        done
        ;;
     :handler-include|:predicate-include)
-       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
          let ++i
          option_handler_includes="${option_handler_includes}
 #line $lineno \"$kf\"
@@ -831,10 +831,10 @@ function handle_alias {
     ERR "malformed \"alias\" command; expected more arguments"
   fi
   cases=
-  if ! expr "$option" : - &>/dev/null; then
+  if ! expr "$option" : '\-' &>/dev/null; then
     ERR "alias for SMT options not yet supported"
   fi
-  if expr "$option" : -- &>/dev/null; then
+  if expr "$option" : '\--' &>/dev/null; then
     if expr "$option" : '.*=' &>/dev/null; then
       expect_arg_long=required_argument
       arg="$(echo "$option" | sed 's,[^=]*=\(.*\),\1,')"
@@ -851,8 +851,8 @@ function handle_alias {
     let ++n_long
     long_option="${long_option:+$long_option | --}$option"
   else
-    if ! expr "$option" : '-.$' &>/dev/null; then
-      if ! expr "$option" : '-.=' &>/dev/null; then
+    if ! expr "$option" : '\-.$' &>/dev/null; then
+      if ! expr "$option" : '\-.=' &>/dev/null; then
         ERR "expected short option specification, got \`$option'"
       fi
       expect_arg=:
index ff3f8b27d55587c0d9de1151960e2b0ee886db25..9f72ac51c39adb7ec72ff20931188b784d0b281e 100644 (file)
@@ -18,7 +18,7 @@
 #include <stdio.h>
 #include <stdint.h>
 
-#include <sys/errno.h>
+#include <cerrno>
 #include <sys/mman.h>
 #include <sys/stat.h>
 #include <antlr3input.h>
@@ -95,14 +95,7 @@ static ANTLR3_UINT32 MemoryMapFile(pANTLR3_INPUT_STREAM input,
     return ANTLR3_ERR_NOFILE;
   }
 
-
-#ifndef MAP_FILE
-  //Tim: This is required for SunOS
   input->data = mmap(0, input->sizeBuf, PROT_READ, MAP_PRIVATE, fd, 0);
-#else
-  input->data = mmap(0, input->sizeBuf, PROT_READ, MAP_FILE | MAP_PRIVATE, fd, 0);
-#endif
-
   errno = 0;
   if(intptr_t(input->data) == -1) {
     return ANTLR3_ERR_NOMEM;