# 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
if test -z "${with_build+set}"; then
with_build=production
fi
-if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}"; then
+if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}" -a -z "${with_abc+set}"; then
custom_build_profile=no
else
custom_build_profile=yes
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"
btargs="$btargs glpk"
fi
fi
+if test -n "${with_abc+set}"; then
+ if test "$with_abc" = yes; then
+ btargs="$btargs abc"
+ fi
+fi
AC_MSG_RESULT([$with_build])
AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
if test $cvc4_use_cln = 2; then
- if test -n "$CVC4_BSD_LICENSED_CODE_ONLY" -o "$with_portfolio" = yes; then
+ if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1 -o "$with_portfolio" = yes; then
cvc4_use_cln=0
cvc4_use_gmp=1
fi
# we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
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++])
],
[if test $cvc4_use_cln = 1; then
)
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])
CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_GLPK"
fi
AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
+AC_SUBST([GLPK_LDFLAGS])
AC_SUBST([GLPK_LIBS])
+# Build with libabc (defined in config/abc.m4)
+AC_ARG_WITH([abc],
+ [AS_HELP_STRING([--with-abc],
+ [use the ABC AIG library])], [], [with_abc=])
+CVC4_CHECK_FOR_ABC
+if test $have_libabc -eq 1; then
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_ABC"
+fi
+AM_CONDITIONAL([CVC4_USE_ABC], [test $have_libabc -eq 1])
+AC_SUBST([ABC_LDFLAGS])
+AC_SUBST([ABC_LIBS])
+
# Check to see if this version/architecture of GNU C++ explicitly
# instantiates __gnu_cxx::hash<uint64_t> or not. Some do, some don't.
# See src/util/hash.h.
AC_LANG_POP([C++])
AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
-AC_MSG_CHECKING([for the pb_ds namespace])
-AC_LANG_PUSH([C++])
-AC_COMPILE_IFELSE([AC_LANG_SOURCE([
-#include <ext/pb_ds/priority_queue.hpp>
-typedef pb_ds::priority_queue<void, void, void> pq;])],
- [CVC4_PB_DS_NAMESPACE=pb_ds],
- [AC_COMPILE_IFELSE([AC_LANG_SOURCE([
- #include <ext/pb_ds/priority_queue.hpp>
- typedef __gnu_pbds::priority_queue<void, void, void> pq;])],
- [CVC4_PB_DS_NAMESPACE=__gnu_pbds],
- [AC_MSG_ERROR([cannot find required priority_queue in either __gnu_pbds or pb_ds namespace.
-
-If you're using a non-GCC compiler (such as clang), you may need to explicitly
-use the GNU standard C++ library by passing:
- CXXFLAGS='-stdlib=libstdc++' CPPFLAGS='-stdlib=libstdc++'
-as arguments to this configure script.
-This is the case on Mac OS Mavericks, for example.])])])
-AC_LANG_POP([C++])
-AC_MSG_RESULT([$CVC4_PB_DS_NAMESPACE])
-AC_DEFINE_UNQUOTED(CVC4_PB_DS_NAMESPACE, ${CVC4_PB_DS_NAMESPACE}, [The namespace for pb_ds data structures.])
-
-# for information: http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
-AC_MSG_CHECKING([whether pb_ds has bug 36612])
-AC_LANG_PUSH([C++])
-AC_COMPILE_IFELSE([AC_LANG_SOURCE([
-#define __throw_container_error inline __throw_container_error
-#define __throw_insert_error inline __throw_insert_error
-#define __throw_join_error inline __throw_join_error
-#define __throw_resize_error inline __throw_resize_error
-#include <ext/pb_ds/exception.hpp>
-])],
- [CVC4_GCC_HAS_PB_DS_BUG=1; bugverb=is],
- [CVC4_GCC_HAS_PB_DS_BUG=0; bugverb="is not"])
-AC_LANG_POP([C++])
-AC_MSG_RESULT([bug $bugverb present])
-AC_DEFINE_UNQUOTED(CVC4_GCC_HAS_PB_DS_BUG, ${CVC4_GCC_HAS_PB_DS_BUG}, [Whether libstdc++ has a certain bug; see http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612])
-
# Check for ANTLR runantlr script (defined in config/antlr.m4)
AC_PROG_ANTLR
# comes last, so it gets other definitions (in particular top_srcdir).
zz_cvc4_use_personal_make_rules='yes
+all:;
include $(top_srcdir)/personal.mk
$(top_srcdir)/personal.mk:; @touch "$@"'
AC_SUBST([zz_cvc4_use_personal_make_rules])
esac
fi
-AC_ARG_VAR(LFSC, [path to LFSC proof checker])
-AC_ARG_VAR(LFSCARGS, [arguments to pass to LFSC proof checker])
-if test -z "$LFSC"; then
- AC_CHECK_PROGS(LFSC, lfsc, [], [])
-else
- AC_CHECK_PROG(LFSC, "$LFSC", [], [])
-fi
-AM_CONDITIONAL([PROOF_REGRESSIONS], [test -n "$LFSC" -a "$enable_proof" = yes])
-if test -n "$LFSC" -a "$enable_proof" = yes; then
- TESTS_ENVIRONMENT="${TESTS_ENVIRONMENT:+$TESTS_ENVIRONMENT }LFSC=\"$LFSC $LFSCARGS\""
+TESTS_ENVIRONMENT=
+RUN_REGRESSION_ARGS=
+if test "$enable_proof" = yes; then
RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof"
fi
AC_SUBST([TESTS_ENVIRONMENT])
AC_SUBST([RUN_REGRESSION_ARGS])
-if test -z "$LFSC"; then
- support_proof_tests='no, lfsc proof checker unavailable'
-elif test "$enable_proof" = yes; then
- support_proof_tests='yes, proof regression tests enabled'
-else
- support_proof_tests='no, proof-generation disabled for this build'
-fi
-AC_SUBST([LFSC])
-AC_SUBST([LFSCARGS])
CXXTESTGEN=
AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
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])
AC_CONFIG_FILES([
Makefile.builds
- Makefile]
+ Makefile
+ proofs/signatures/Makefile]
m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
)
fi
if test "$gpl" = yes; then
- if test -n "$CVC4_BSD_LICENSED_CODE_ONLY"; then
- AC_ERROR([Bad configuration detected: user requested BSD-licensed code only, but also requested GPLed libraries:$gpllibs])
+ if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1; then
+ AC_ERROR([Bad configuration detected: BSD-licensed code only, but also requested GPLed libraries:$gpllibs
+To permit GPL'ed dependences, use the configure flag --enable-gpl])
fi
licensewarn="${licensewarn}"'****************************************************************************
As these libraries are covered under the GPLv3, so is this build of CVC4.
CVC4 is also available to you under the terms of the (modified) BSD license.
If you prefer to license CVC4 under those terms, please configure with the
-option "--bsd".
+option "--bsd", which will disable all optional GPLed library dependences.
****************************************************************************
'
license="GPLv3 (due to optional libraries; see below)"
else
+ licensewarn="${licensewarn}Please note that this configuration is NOT built against any GPL'ed
+libraries, so it is covered by the (modified) BSD license. This is,
+however, not the best-performing configuration of CVC4. To build
+against GPL'ed libraries which improve CVC4's performance, re-configure
+with '--best --enable-gpl'.
+
+"
license="modified BSD"
fi
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])
Muzzle : $enable_muzzle
Unit tests : $support_unit_tests
-Proof tests : $support_proof_tests
gcov support : $enable_coverage
gprof support: $enable_profiling
MP library : $mplibrary
GLPK : $with_glpk
+ABC : $with_abc
Readline : $with_readline
CPPFLAGS : $CPPFLAGS
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