# Process this file with autoconf to produce a configure script.
m4_define(_CVC4_MAJOR, 1) dnl version (major)
-m4_define(_CVC4_MINOR, 4) dnl version (minor)
+m4_define(_CVC4_MINOR, 5) dnl version (minor)
m4_define(_CVC4_RELEASE, 0) dnl version (alpha)
m4_define(_CVC4_EXTRAVERSION, [-prerelease]) dnl version (extra)
m4_define(_CVC4_RELEASE_STRING, _CVC4_MAJOR[.]_CVC4_MINOR[]m4_if(_CVC4_RELEASE,[0],,[.]_CVC4_RELEASE)_CVC4_EXTRAVERSION) dnl version string
btargs="$btargs nooptimized"
fi
fi
+# --enable-staticbinary is an alias for --enable-static-binary
+if test -n "${enable_staticbinary+set}"; then
+ enable_static_binary="$enable_staticbinary"
+fi
if test -n "${enable_static_binary+set}"; then
if test "$enable_static_binary" = yes; then
btargs="$btargs staticbinary"
PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
[AC_LANG_PUSH([C++])
save_LIBS="$LIBS"
+ save_CXXFLAGS="$CXXFLAGS"
LIBS="$CLN_LIBS $LIBS"
+ CXXFLAGS="$CLN_CFLAGS $CXXFLAGS"
AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])], [
cvc4_use_cln=1
], [
cvc4_use_gmp=1
fi
])
+ CXXFLAGS="$save_CXXFLAGS"
LIBS="$save_LIBS"
AC_LANG_POP([C++])
],
)
fi
if test $cvc4_use_cln = 0; then
- # try GMPXX, fail if not found
- AC_CHECK_LIB(gmpxx, __gmpz_init, , [AC_MSG_ERROR([GNU MP C++ library (libgmpxx) not found, see http://gmplib.org/])])
+ # try GMPXX, fail if not found; don't need to link against it, only need its header
+ AC_LANG_PUSH([C++])
+ AC_CHECK_HEADER([gmpxx.h], , [AC_MSG_ERROR([GNU MP C++ library header (gmpxx.h) required but not found, see http://gmplib.org/])])
+ AC_LANG_POP([C++])
cvc4_cln_or_gmp=gmp
else
CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
$as_echo "cd builds/$target/$build_type"
cd "builds/$target/$build_type"
CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
+ # Runs the single recursive configure invocation using a relative path.
+ # See https://lists.gnu.org/archive/html/autoconf/2011-04/msg00060.html
echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
- "$SHELL" "`pwd`/../../../configure" "${config_cmdline[[@]]}"
+ "$SHELL" "../../../configure" "${config_cmdline[[@]]}"
exitval=$?
cd ../../..
if test $exitval -eq 0; then
# Unpack standard build types. Any particular options can be overriden with
# --enable/disable-X options
+# Tim: This needs to keep CVC4CPPFLAGS, CVC4CXXFLAGS, etc. set by earlier checks
case "$with_build" in
production) # highly optimized, no assertions, no tracing, dumping
- CVC4CPPFLAGS=
- CVC4CXXFLAGS=
- CVC4CFLAGS=
- CVC4LDFLAGS=
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
+ CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
+ CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
+ CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi
if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
- if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
+ if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
;;
debug) # unoptimized, debug symbols, assertions, tracing, dumping
- CVC4CPPFLAGS='-DCVC4_DEBUG'
- CVC4CXXFLAGS='-fno-inline'
- CVC4CFLAGS='-fno-inline'
- CVC4LDFLAGS=
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG"
+ CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-fno-inline"
+ CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-fno-inline"
+ CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
FLAG_VISIBILITY_HIDDEN=
if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi
if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
- if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
+ if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
;;
default) # moderately optimized, assertions, tracing, dumping
- CVC4CPPFLAGS=
- CVC4CXXFLAGS=
- CVC4CFLAGS=
- CVC4LDFLAGS=
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
+ CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
+ CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
+ CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=2 ; fi
if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
- if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
+ if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
;;
competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
- CVC4CPPFLAGS='-DCVC4_COMPETITION_MODE'
- CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
- CVC4CFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
- CVC4LDFLAGS=
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COMPETITION_MODE"
+ CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
+ CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
+ CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=9 ; fi
if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
AC_MSG_CHECKING([whether to support proofs in libcvc4])
AC_ARG_ENABLE([proof],
- [AS_HELP_STRING([--enable-proof],
- [support proof generation])])
+ [AS_HELP_STRING([--disable-proof],
+ [do not support proof generation])])
if test -z "${enable_proof+set}"; then
- enable_proof=no
+ enable_proof=yes
fi
AC_MSG_RESULT([$enable_proof])
if test -z "$CXXTESTGEN"; then
AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST:$PATH])
fi
+# The latest version of cxxtest distributed from the git repository places
+# cxxtest under <cxxtest-root>/bin/cxxtest
+if test -z "$CXXTESTGEN"; then
+ AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST/bin:$PATH])
+fi
if test "$enable_unit_testing" = "no"; then
AC_MSG_NOTICE([unit tests disabled by user request.])
CXXTESTGEN=
CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
# Checks for header files and their contents.
-AC_CHECK_HEADERS([getopt.h unistd.h])
+AC_CHECK_HEADERS([getopt.h unistd.h ext/stdio_filebuf.h])
# Checks for typedefs, structures, and compiler characteristics.
#AC_HEADER_STDBOOL
# check with which standard strerror_r() complies
AC_FUNC_STRERROR_R
+# is is_sorted() in std or __gnu_cxx?
+CHECK_FOR_IS_SORTED
+
# require boost library
BOOST_REQUIRE()
AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
if test "$with_portfolio" = yes; then
CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
+
+ # see if Boost has thread attributes (should be any version >= 1.50.0)
+ # non-fatal error if not, but we won't support --thread-stack option
+ AC_MSG_CHECKING([whether Boost threads support thread attrs])
+ AC_LANG_PUSH([C++])
+ cvc4_save_CPPFLAGS="$CPPFLAGS"
+ cvc4_save_LIBS="$LIBS"
+ cvc4_save_LDFLAGS="$LDFLAGS"
+ CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS"
+ LIBS="$LIBS $BOOST_THREAD_LIBS"
+ LDFLAGS="$LDFLAGS $BOOST_THREAD_LDFLAGS"
+ AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <boost/thread.hpp>],
+ [boost::thread::attributes attrs; attrs.set_stack_size(10 * 1024 * 1024);])],
+ [cvc4_boost_has_thread_attr=1;
+ AC_MSG_RESULT([yes])],
+ [cvc4_boost_has_thread_attr=0;
+ AC_MSG_RESULT([no])])
+ CPPFLAGS="$cvc4_save_CPPFLAGS"
+ LIBS="$cvc4_save_LIBS"
+ LDFLAGS="$cvc4_save_LDFLAGS"
+ AC_LANG_POP([C++])
+else
+ cvc4_boost_has_thread_attr=0
fi
+AC_DEFINE_UNQUOTED([BOOST_HAS_THREAD_ATTR], $cvc4_boost_has_thread_attr, [Define to 1 if Boost threading library has support for thread attributes])
# Check for libreadline (defined in config/readline.m4)
AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
fi
fi
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/base/tls.h])
CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then
AC_MSG_WARN([])
- AC_MSG_WARN([You are electing to build unsupported language binding(s): $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
- AC_MSG_WARN([Please be aware that these bindings may not compile, or work, and the interface to CVC4 via])
- AC_MSG_WARN([these bindings may change drastically in upcoming releases of CVC4.])
+ AC_MSG_WARN([You are electing to build unsupported language binding(s):])
+ AC_MSG_WARN([ $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
+ AC_MSG_WARN([Please be aware that these bindings may not compile, or])
+ AC_MSG_WARN([work, and the interface to CVC4 via these bindings may])
+ AC_MSG_WARN([change drastically in upcoming releases of CVC4.])
AC_MSG_WARN([])
fi
projects / cvc5.git / blobdiff