diff options
Diffstat (limited to 'configure.ac')
-rw-r--r-- | configure.ac | 1611 |
1 files changed, 0 insertions, 1611 deletions
diff --git a/configure.ac b/configure.ac deleted file mode 100644 index 81fff6c93..000000000 --- a/configure.ac +++ /dev/null @@ -1,1611 +0,0 @@ -# -*- Autoconf -*- -# Process this file with autoconf to produce a configure script. - -m4_define(_CVC4_MAJOR, 1) dnl version (major) -m4_define(_CVC4_MINOR, 7) 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 - -dnl Preprocess CL args. Defined in config/cvc4.m4 -CVC4_AC_INIT - -AC_PREREQ([2.61]) -AC_INIT([cvc4], _CVC4_RELEASE_STRING, [cvc4-bugs@cs.stanford.edu]) -AC_CONFIG_SRCDIR([src/include/cvc4_public.h]) -AC_CONFIG_AUX_DIR([config]) -AC_REQUIRE_AUX_FILE([tap-driver.sh]) -AC_CONFIG_MACRO_DIR([config]) -AC_CONFIG_LIBOBJ_DIR([src/lib]) - -m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])]) - -CVC4_MAJOR=_CVC4_MAJOR -CVC4_MINOR=_CVC4_MINOR -CVC4_RELEASE=_CVC4_RELEASE -CVC4_EXTRAVERSION=_CVC4_EXTRAVERSION -CVC4_RELEASE_STRING=_CVC4_RELEASE_STRING - -# Libtool version numbers for libraries -# Version numbers are in the form current:revision:age -# -# current - -# increment if interfaces have been added, removed or changed -# revision - -# increment if source code has changed -# set to zero if current is incremented -# age - -# increment if interfaces have been added -# set to zero if interfaces have been removed -# or changed -# -# For more information, see: -# http://www.gnu.org/software/libtool/manual/libtool.html#Versioning -# For guidance on when to change the version number, refer to the -# developer's guide. - -m4_define([library_version], [m4_esyscmd([grep -F "$(grep -v '^#' library_versions | awk '{print$][1}' | sed 's,\\,\\\\\\,g' | (while read r; do if echo "]_CVC4_RELEASE_STRING[" | grep -q "^$r\$"; then echo "$r"; exit; fi; done; echo NO_MATCH_FOUND)) " library_versions | awk 'BEGIN {FS=":";OFS=":";RS=" "} /^$1:/ {print$][2,$][3,$][4}' | head -1])]) - -m4_define(_CVC4_LIBRARY_VERSION, library_version([libcvc4]))dnl -m4_define(_CVC4_PARSER_LIBRARY_VERSION, library_version([libcvc4parser]))dnl -m4_define(_CVC4_BINDINGS_LIBRARY_VERSION, library_version([libcvc4bindings]))dnl - -m4_define([fatal_error], [m4_errprint(__program__:__file__:__line__[: fatal error: $* -])m4_exit(1)])dnl - -m4_ifblank(_CVC4_LIBRARY_VERSION,[fatal_error([no CVC4_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl -m4_ifblank(_CVC4_PARSER_LIBRARY_VERSION,[fatal_error([no CVC4_PARSER_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl -m4_ifblank(_CVC4_BINDINGS_LIBRARY_VERSION,[fatal_error([no CVC4_BINDINGS_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl - -CVC4_LIBRARY_VERSION=_CVC4_LIBRARY_VERSION -CVC4_PARSER_LIBRARY_VERSION=_CVC4_PARSER_LIBRARY_VERSION -CVC4_BINDINGS_LIBRARY_VERSION=_CVC4_BINDINGS_LIBRARY_VERSION - -# Using AX_CXX_COMPILE_STDCXX_11 and the AC_CANONICAL_* macros destroy the -# command line you get from $@, which we want later for determining the build -# profile. So we save it. -# (We can't do our build profile stuff here, or it's not included in the -# output... autoconf overrides us on the orderings of some things.) -config_cmdline=("$@") -cvc4_config_cmdline="${config_cmdline[[@]]}" - -# remember if the user set these explicitly (or whether autoconf does) -user_specified_enable_or_disable_static=${enable_static+yes} -user_specified_enable_or_disable_shared=${enable_shared+yes} - -if test -e src/include/cvc4_public.h; then - CVC4_CONFIGURE_AT_TOP_LEVEL=yes -else - CVC4_CONFIGURE_AT_TOP_LEVEL=no -fi - -# override autoconf: we don't want it giving us CFLAGS/CXXFLAGS, but we do -# want to respect the user's flags -if test -z "${CFLAGS+set}"; then CFLAGS=; fi -if test -z "${CXXFLAGS+set}"; then CXXFLAGS=; fi - -# on by default -AM_MAINTAINER_MODE([enable]) - -# turn off static lib building by default -AC_ENABLE_SHARED -AC_DISABLE_STATIC - -AC_CANONICAL_BUILD -AC_CANONICAL_HOST -AC_CANONICAL_TARGET - -# C++11 support in the compiler is now mandatory. Check for support and add -# switches if necessary. -AX_CXX_COMPILE_STDCXX_11([ext], [mandatory]) - -as_me=configure - -if test "$enable_shared" = no -a "$user_specified_enable_or_disable_shared" = yes; then - enable_static=yes -fi - -# Features requested by the user -AC_MSG_CHECKING([for requested build profile]) -AC_ARG_WITH([build], - [AS_HELP_STRING([--with-build=profile], - [for profile in {production,debug,competition,testing}])]) - -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}" -a \ - -z "${with_abc+set}" -a \ - -z "${with_cadical+set}" -a \ - -z "${with_cryptominisat+set}" -a \ - -z "${with_lfsc+set}" -a \ - -z "${with_symfpu+set}"; then - custom_build_profile=no -else - custom_build_profile=yes -fi -btargs= -if test -n "${enable_optimized+set}"; then - if test "$enable_optimized" = yes; then - btargs="$btargs optimized" - else - 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" - else - btargs="$btargs nostaticbinary" - fi -fi -if test -n "${enable_debug_symbols+set}"; then - if test "$enable_debug_symbols" = yes; then - btargs="$btargs debugsymbols" - else - btargs="$btargs nodebugsymbols" - fi -fi -if test -n "${enable_assertions+set}"; then - if test "$enable_assertions" = yes; then - btargs="$btargs assertions" - else - btargs="$btargs noassertions" - fi -fi -if test -n "${enable_proof+set}"; then - if test "$enable_proof" = yes; then - btargs="$btargs proof" - else - btargs="$btargs noproof" - fi -fi -if test -n "${enable_tracing+set}"; then - if test "$enable_tracing" = yes; then - btargs="$btargs tracing" - else - btargs="$btargs notracing" - fi -fi -if test -n "${enable_dumping+set}"; then - if test "$enable_dumping" = yes; then - btargs="$btargs dumping" - else - btargs="$btargs nodumping" - fi -fi -if test -n "${enable_muzzle+set}"; then - if test "$enable_muzzle" = yes; then - btargs="$btargs muzzle" - else - btargs="$btargs nomuzzle" - fi -fi -if test -n "${enable_coverage+set}"; then - if test "$enable_coverage" = yes; then - btargs="$btargs coverage" - else - btargs="$btargs nocoverage" - fi -fi -if test -n "${enable_profiling+set}"; then - if test "$enable_profiling" = yes; then - btargs="$btargs profiling" - else - btargs="$btargs noprofiling" - fi -fi -if test -n "${enable_statistics+set}"; then - if test "$enable_statistics" = yes; then - btargs="$btargs statistics" - else - btargs="$btargs nostatistics" - fi -fi -if test -n "${enable_replay+set}"; then - if test "$enable_replay" = yes; then - btargs="$btargs replay" - else - btargs="$btargs noreplay" - fi -fi -if test -n "${with_glpk+set}"; then - if test "$with_glpk" = yes; then - btargs="$btargs glpk" - fi -fi -if test -n "${with_abc+set}"; then - if test "$with_abc" = yes; then - btargs="$btargs abc" - fi -fi -if test -n "${with_cadical+set}"; then - if test "$with_cadical" = yes; then - btargs="$btargs cadical" - fi -fi -if test -n "${with_cryptominisat+set}"; then - if test "$with_cryptominisat" = yes; then - btargs="$btargs cryptominisat" - fi -fi -if test -n "${with_lfsc+set}"; then - if test "$with_lfsc" = yes; then - enable_proof=yes - btargs="$btargs lfsc" - fi -fi -if test -n "${with_symfpu+set}"; then - if test "$with_symfpu" = yes; then - btargs="$btargs symfpu" - fi -fi - -AC_MSG_RESULT([$with_build]) - -AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects]) -AC_CONFIG_HEADERS([cvc4autoconfig.h]) - -# automake 1.12 changes the test driver mechanism in a way that is -# completely incompatible with 1.11. We figure out here which version -# we're using in order to set up test makefiles correctly. -# See http://lists.gnu.org/archive/html/automake/2012-04/msg00060.html -if test -z "$am__api_version"; then - AC_MSG_ERROR([Cannot determine automake API version ?!]) -fi -case "$am__api_version" in - 1.11*) automake111=true ;; - *) automake111=false ;; -esac -AM_CONDITIONAL([AUTOMAKE_1_11], [$automake111]) - -# Initialize libtool's configuration options. -# we're not DLL-clean yet (i.e., don't properly use dllexport and dllimport) -# _LT_SET_OPTION([LT_INIT],[win32-dll]) -LT_INIT - -# Checks for programs. -AC_PROG_CC -AC_PROG_CXX -AC_PROG_INSTALL - -CVC4_GCC_VERSION - -if test $cross_compiling = "no"; then - AC_MSG_CHECKING([whether C++ exceptions work]) - AC_LANG_PUSH([C++]) - AC_RUN_IFELSE( - AC_LANG_PROGRAM([#include <exception>], [[ - int result = 1; - try { - throw std::exception(); - } catch (...) { - result = 0; - } - return result; - ]]), - [AC_MSG_RESULT([yes])], - [AC_MSG_ERROR([C++ exceptions do not work.])] - ) - AC_LANG_POP([C++]) -else - AC_MSG_WARN([Cross compiling, cannot check whether exceptions work]) -fi - -cvc4_use_gmp=2 -cvc4_use_cln=2 - -AC_ARG_WITH( - [cln], - AS_HELP_STRING( - [--with-cln], - [use CLN instead of GMP] - ), - [case "$withval" in - y|ye|yes|Y|YE|YES) cvc4_use_cln=1 ;; - n|no|N|NO) cvc4_use_cln=0 ;; - esac - ] -) - -AC_ARG_WITH( - [gmp], - AS_HELP_STRING( - [--with-gmp], - [use GMP instead of CLN] - ), - [case "$withval" in - y|ye|yes|Y|YE|YES) cvc4_use_gmp=1 ;; - n|no|N|NO) cvc4_use_gmp=0 ;; - esac - ] -) - -if test $cvc4_use_cln = 1 -a $cvc4_use_gmp = 1 || test $cvc4_use_cln = 0 -a $cvc4_use_gmp = 0; then - AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.]) -fi -if test $cvc4_use_gmp = 1; then - cvc4_use_cln=0 -elif test $cvc4_use_gmp = 0; then - cvc4_use_cln=1 -elif test $cvc4_use_cln = 1; then - cvc4_use_gmp=0 -elif test $cvc4_use_cln = 0; then - cvc4_use_gmp=1 -fi - -# try GMP, fail if not found; GMP is required for both CLN and for GMP -# versions of CVC4 -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 "$CVC4_BSD_LICENSED_CODE_ONLY" = 1 -o "$with_portfolio" = yes; then - cvc4_use_cln=0 - cvc4_use_gmp=1 - fi -fi - -if test $cvc4_use_cln != 0; then - # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail - # gracefully. You can only specify it once for a given library name. That - # is, even on separate if/else branches, you can't put - # PKG_CHECK_MODULES([CLN], ...). That's why things are so convoluted here, - # 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 - ], [ - if test $cvc4_use_cln = 1; then - # fail - AC_MSG_ERROR([CLN installation missing, too old, or not functional for this architecture]) - else - # fall back to GMP - AC_MSG_NOTICE([CLN installation missing, too old, or not functional for this architecture, will use gmp instead]) - cvc4_use_cln=0 - cvc4_use_gmp=1 - fi - ]) - CXXFLAGS="$save_CXXFLAGS" - LIBS="$save_LIBS" - AC_LANG_POP([C++]) - ], - [if test $cvc4_use_cln = 1; then - # fail - AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing]) - else - # fall back to GMP - AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp]) - cvc4_use_cln=0 - cvc4_use_gmp=1 - fi - ] - ) -fi -if test $cvc4_use_cln = 0; then - # 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" - CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS" - CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS" - LIBS="$CLN_LIBS${LIBS:+ $LIBS}" - cvc4_cln_or_gmp=cln -fi - -if test $cvc4_cln_or_gmp = cln; then - AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.]) -else - AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.]) -fi -AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln]) -AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp]) - -# Dumping cannot be used in a portfolio build. Disable dumping by default when -# a portfolio build has been requested, throw an error if dumping has been -# explicitly requested with a portfolio build. -if test "$with_portfolio" = yes; then - if test "$enable_dumping" = yes; then - AC_MSG_ERROR([Dumping is not supported with a portfolio build]) - fi - enable_dumping=no -fi - -# construct the build string -AC_MSG_CHECKING([for appropriate build string]) -if test -z "$ac_confdir"; then - ac_confdir="$srcdir" -fi -build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp` -AC_MSG_RESULT($build_type) - -# Require building in target and build-specific build directory: -# -# If the configure script is invoked from the top-level source -# directory, it creates a suitable build directory (based on the build -# architecture and build profile from $build_type), changes into it, -# and reinvokes itself. CVC4_CONFIGURE_IN_BUILDS is an envariable -# that breaks any possibility of infinite recursion in this process. -AC_MSG_CHECKING([what dir to configure]) -if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then - AC_MSG_RESULT([this one (in builds/)]) -elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then - AC_MSG_RESULT([builds/$target/$build_type]) - $as_echo - if test -z "$ac_srcdir"; then - mkbuilddir=./config/mkbuilddir - else - mkbuilddir=$ac_srcdir/config/mkbuilddir - fi - $as_echo "$mkbuilddir $target $build_type" - source $mkbuilddir "$target" "$build_type" - $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" "../../../configure" "${config_cmdline[[@]]}" - exitval=$? - cd ../../.. - if test $exitval -eq 0; then - cat >config.reconfig <<EOF -[#!/bin/bash -# Generated by configure, `date` -# This script is part of CVC4. - -cd "\`dirname \\"\$0\\"\`" - -if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi - -current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`) -arch=\${current[0]} -build=\${current[1]} - -echo "reconfiguring in builds/\$arch/\$build..." -cd "builds/\$arch/\$build" -echo ./config.status "\$@" -./config.status "\$@"] -EOF - chmod +x config.reconfig - fi - ln -sf "$target/$build_type/config.log" "builds/config.log" - exit $exitval -else - AC_MSG_RESULT([this one (user-specified)]) -fi - -as_me=configure - -# 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="${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_debug_symbols+set}"; then enable_debug_symbols=no ; 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=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 - if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi - ;; - debug) # unoptimized, debug symbols, assertions, tracing, dumping - 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=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 - if test -z "${enable_valgrind+set}" ; then enable_valgrind=optional ; fi - ;; - testing) # moderately optimized, assertions, tracing, dumping - 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_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=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 - if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi - ;; - competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled - 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 - if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi - if test -z "${enable_statistics+set}" ; then enable_statistics=no ; 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_tracing+set}" ; then enable_tracing=no ; fi - if test -z "${enable_dumping+set}" ; then enable_dumping=no ; fi - if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi - if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi - if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi - if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi - if test -z "${enable_static_binary+set}"; then enable_static_binary=yes ; fi - ;; - *) - AC_MSG_FAILURE([unknown build profile: $with_build]) - ;; -esac -if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi - -AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION], [test "$with_build" = production]) -AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG], [test "$with_build" = debug]) -AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition]) -AM_CONDITIONAL([CVC4_BUILD_PROFILE_TESTING], [test "$with_build" = testing]) - -# permit a static binary -AC_MSG_CHECKING([whether to build a static binary]) -AC_ARG_ENABLE([static-binary], - [AS_HELP_STRING([--enable-static-binary], - [build a fully statically-linked binary [default=no]])]) -if test -z "${enable_static_binary+set}"; then - enable_static_binary=no -fi -AC_MSG_RESULT([$enable_static_binary]) -if test "$enable_static_binary" = yes; then - if test "$target_vendor" = apple; then - if test -z "$MAC_STATIC_BINARY_MANUAL_OVERRIDE"; then - AC_MSG_ERROR([[Statically-linked binaries are not supported on macOS. See https://developer.apple.com/library/content/qa/qa1118/_index.html . (If you ABSOLUTELY insist on this going forward and you know what you are doing, set MAC_STATIC_BINARY_MANUAL_OVERRIDE=1)]]) - else - AC_MSG_WARN([MAC_STATIC_BINARY_MANUAL_OVERRIDE was set!]) - AC_MSG_WARN([Will make a static binary during this build. Note that it may fail!]) - fi - fi - if test "$enable_static" != yes; then - enable_static=yes - AC_MSG_WARN([forcing static-library building, --enable-static-binary given]) - fi -fi - -AC_MSG_CHECKING([whether to support proofs in libcvc4]) - -AC_ARG_ENABLE([proof], - [AS_HELP_STRING([--disable-proof], - [do not support proof generation])]) -if test -z "${enable_proof+set}"; then - enable_proof=yes -fi -AC_MSG_RESULT([$enable_proof]) - -if test "$enable_proof" = yes; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF" -fi -AM_CONDITIONAL([CVC4_PROOF], [test "$enable_proof" = yes]) - -AC_MSG_CHECKING([whether to optimize libcvc4]) - -AC_ARG_ENABLE([optimized], - [AS_HELP_STRING([--enable-optimized], - [optimize the build])]) - -if test -z "${enable_optimized+set}"; then - enable_optimized=no -fi - -AC_MSG_RESULT([$enable_optimized]) - -if test "$enable_optimized" = yes; then - CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL" - CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL" -else - # Use -Og if available (optimizations that do not interfere with debugging), - # -O0 otherwise - debug_optimization_level="-O0" - CVC4_CXX_OPTION([-Og], [debug_optimization_level]) - CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${debug_optimization_level}" - CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }${debug_optimization_level}" -fi - -AC_MSG_CHECKING([whether to include debugging symbols in libcvc4]) - -AC_ARG_ENABLE([debug-symbols], - [AS_HELP_STRING([--disable-debug-symbols], - [do not include debug symbols in libcvc4])]) - -if test -z "${enable_debug_symbols+set}"; then - enable_debug_symbols=yes -fi - -AC_MSG_RESULT([$enable_debug_symbols]) - -if test "$enable_debug_symbols" = yes; then - CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3" - CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3" -fi - -AC_MSG_CHECKING([whether to enable Valgrind instrumentation]) - -AC_ARG_ENABLE([valgrind], - [AS_HELP_STRING([--enable-valgrind], - [enable Valgrind instrumentation])]) - -if test -z "${enable_valgrind+set}"; then - enable_valgrind=no -fi - -AC_MSG_RESULT([$enable_valgrind]) - -if test "$enable_valgrind" != no; then - # Valgrind instrumentation is either explicitly enabled (enable_valgrind=yes) - # or enabled if available (enable_valgrind=optional) - AC_CHECK_HEADER([valgrind/memcheck.h], - [CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_VALGRIND"], - [if test "$enable_valgrind" = yes; then - AC_MSG_ERROR([Need valgrind/memcheck.h to enable Valgrind instrumentation]) - else - AC_MSG_NOTICE([valgrind/memcheck.h missing, Valgrind instrumentation disabled]) - fi - ]) -fi - -AC_MSG_CHECKING([whether to use the debug context memory manager]) - -AC_ARG_ENABLE([debug-context-memory-manager], - [AS_HELP_STRING([--enable-debug-context-memory-manager], - [use the debug context memory manager])]) - -if test -z "${enable_debug_context_memory_manager+set}"; then - enable_debug_context_memory_manager=no -fi - -AC_MSG_RESULT([$enable_debug_context_memory_manager]) - -if test "$enable_debug_context_memory_manager" = yes; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER" -fi - -AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4]) - -AC_ARG_ENABLE([statistics], - [AS_HELP_STRING([--disable-statistics], - [do not include statistics in libcvc4])]) - -if test -z "${enable_statistics+set}"; then - enable_statistics=yes -fi - -AC_MSG_RESULT([$enable_statistics]) - -if test "$enable_statistics" = yes; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON" -fi - -AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4]) - -AC_ARG_ENABLE([replay], - [AS_HELP_STRING([--disable-replay], - [turn off the replay feature in libcvc4])]) - -if test -z "${enable_replay+set}"; then - enable_replay=yes -fi - -AC_MSG_RESULT([$enable_replay]) - -if test "$enable_replay" = yes; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY" -fi - -AC_MSG_CHECKING([whether to include assertions in build]) - -AC_ARG_ENABLE([assertions], - [AS_HELP_STRING([--disable-assertions], - [turn off assertions in build])]) - -if test -z "${enable_assertions+set}"; then - enable_assertions=yes -fi - -AC_MSG_RESULT([$enable_assertions]) - -if test "$enable_assertions" = yes; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS" -else - # turn off regular C assert() also - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG" -fi - -AC_MSG_CHECKING([whether to do a traceable build of CVC4]) -AC_ARG_ENABLE([tracing], - [AS_HELP_STRING([--disable-tracing], - [remove all tracing code from CVC4])]) - -if test -z "${enable_tracing+set}"; then - enable_tracing=yes -fi - -AC_MSG_RESULT([$enable_tracing]) - -if test "$enable_tracing" = yes; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING" -fi - -AC_MSG_CHECKING([whether to do a dump-capable build of CVC4]) -AC_ARG_ENABLE([dumping], - [AS_HELP_STRING([--disable-dumping], - [remove all dumping code from CVC4])]) - -if test -z "${enable_dumping+set}"; then - enable_dumping=yes -fi - -AC_MSG_RESULT([$enable_dumping]) - -if test "$enable_dumping" = yes; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING" -fi - -AC_MSG_CHECKING([whether to do a muzzled build of CVC4]) -AC_ARG_ENABLE([muzzle], - [AS_HELP_STRING([--enable-muzzle], - [completely silence CVC4; remove ALL non-result output from build])]) - -if test -z "${enable_muzzle+set}"; then - enable_muzzle=no -fi - -AC_MSG_RESULT([$enable_muzzle]) - -if test "$enable_muzzle" = yes; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE" -fi - -AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4]) -AC_ARG_ENABLE([coverage], - [AS_HELP_STRING([--enable-coverage], - [build with support for gcov coverage testing])]) - -if test -z "${enable_coverage+set}"; then - enable_coverage=no - # make COVERAGE_ON the empty string for makefile conditional function - # $(if $(COVERAGE_ON), action1, action2) - COVERAGE_ON= -fi - -AC_MSG_RESULT([$enable_coverage]) - -if test "$enable_coverage" = yes; then - # For coverage testing, we prefer: - # --enable-static --disable-shared --disable-static-binary - # If the user didn't specify these, we force them here. If the - # user specified them in opposite phase, give warnings that they - # shouldn't do that, or bomb out. - COVERAGE_ON=yes - if test "$user_specified_enable_or_disable_shared" != yes; then - enable_shared=no - AC_MSG_WARN([turning off shared library building due to --enable-coverage]) - elif test "$enable_shared" = yes; then - AC_MSG_WARN([]) - AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared]) - AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.]) - AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.]) - AC_MSG_WARN([]) - fi - if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then - AC_MSG_WARN([]) - AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary]) - AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.]) - AC_MSG_WARN([]) - fi - if test "$user_specified_enable_or_disable_static" != yes; then - enable_static=yes - AC_MSG_WARN([turning on static library building due to --enable-coverage]) - elif test "$enable_static" != yes; then - AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.]) - fi - - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE" - CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage" - CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage" - CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage" -fi - -AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4]) - -AC_ARG_ENABLE([profiling], - [AS_HELP_STRING([--enable-profiling], - [build with support for gprof profiling])]) - -if test -z "${enable_profiling+set}"; then - enable_profiling=no -fi - -AC_MSG_RESULT([$enable_profiling]) - -if test "$enable_profiling" = yes; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING" - CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg" - CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg" - CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg" -fi - -# Check for libglpk (defined in config/glpk.m4) -AC_ARG_WITH([glpk], - [AS_HELP_STRING([--with-glpk], - [use GLPK simplex solver])], [], [with_glpk=]) -CVC4_CHECK_FOR_GLPK -if test $have_libglpk -eq 1; then - 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]) - - -# Build with libcadical -AC_ARG_WITH([cadical], - [AS_HELP_STRING([--with-cadical], - [use the CaDiCaL SAT solver])], [], [with_cadical=]) -CVC4_CHECK_FOR_CADICAL -if test $have_libcadical -eq 1; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CADICAL" - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CADICAL_HOME/src" -fi -AM_CONDITIONAL([CVC4_USE_CADICAL], [test $have_libcadical -eq 1]) -AC_SUBST([CADICAL_LDFLAGS]) -AC_SUBST([CADICAL_LIBS]) - -# Build with libcryptominisat -AC_ARG_WITH([cryptominisat], - [AS_HELP_STRING([--with-cryptominisat], - [use the CRYPTOMINISAT sat solver])], [], [with_cryptominisat=]) -CVC4_CHECK_FOR_CRYPTOMINISAT -if test $have_libcryptominisat -eq 1; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CRYPTOMINISAT" - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/include" -fi -AM_CONDITIONAL([CVC4_USE_CRYPTOMINISAT], [test $have_libcryptominisat -eq 1]) -AC_SUBST([CRYPTOMINISAT_LDFLAGS]) -AC_SUBST([CRYPTOMINISAT_LIBS]) - -# Build with LFSC -AC_ARG_WITH([lfsc], - [AS_HELP_STRING([--with-lfsc], - [use the LFSC proof checker])], [], [with_lfsc=]) -CVC4_CHECK_FOR_LFSC -if test $have_liblfsc -eq 1; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_LFSC" -fi -AM_CONDITIONAL([CVC4_USE_LFSC], [test $have_liblfsc -eq 1]) -AC_SUBST([LFSC_LDFLAGS]) -AC_SUBST([LFSC_LIBS]) - -# Build with symfpu -AC_ARG_WITH([symfpu], - [AS_HELP_STRING([--with-symfpu], - [use symfpu for floating point solver])], [], [with_symfpu=]) -CVC4_CHECK_FOR_SYMFPU -if test $have_symfpu_headers -eq 1; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_SYMFPU" - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$SYMFPU_HOME" -fi -AM_CONDITIONAL([CVC4_USE_SYMFPU], [test $have_symfpu_headers -eq 1]) -AC_SUBST([CVC4_USE_SYMFPU], [$have_symfpu_headers]) - -# Check to see if this version/architecture of GNU C++ explicitly -# instantiates std::hash<uint64_t> or not. Some do, some don't. -# See src/util/hash.h. -AC_MSG_CHECKING([whether std::hash<uint64_t> is already specialized]) -AC_LANG_PUSH([C++]) -AC_COMPILE_IFELSE([AC_LANG_SOURCE([ -#include <cstdint> -#include <functional> -namespace std { template<> struct hash<uint64_t> {}; }])], - [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"], - [AC_MSG_RESULT([yes])]) -AC_LANG_POP([C++]) - -# Check whether "long" and "int64_t" are distinct types w.r.t. overloading. -# Even if they have the same size, they can be distinct, and some platforms -# can have problems with ambiguous function calls when auto-converting -# int64_t to long, and others will complain if you overload a function -# that takes an int64_t with one that takes a long (giving a redefinition -# error). So we have to keep both happy. Probably the same underlying -# issue as the hash specialization above, but let's check separately -# for flexibility. -AC_MSG_CHECKING([for the relationship between long and int64_t]) -AC_LANG_PUSH([C++]) -AC_COMPILE_IFELSE([AC_LANG_SOURCE([ -#include <stdint.h> -void foo(long) {} -void foo(int64_t) {}])], - [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1], - [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0]) -AC_LANG_POP([C++]) -AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS]) - -# Check for ANTLR runantlr script (defined in config/antlr.m4) -AC_PROG_ANTLR - -CVC4_CXX_OPTION([-Werror], [WERROR]) -CVC4_C_OPTION([-Werror], [C_WERROR]) -CVC4_CXX_OPTION([-Wno-deprecated], [WNO_DEPRECATED]) -CVC4_C_OPTION([-Wno-deprecated], [C_WNO_DEPRECATED]) -CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL]) -CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE]) -CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES]) -CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED]) -CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE]) -CVC4_CXX_OPTION([-Wsuggest-override], [W_SUGGEST_OVERRIDE]) -CVC4_CXX_OPTION([-Wnon-virtual-dtor], [W_NON_VIRTUAL_DTOR]) -CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING]) -AC_SUBST([WERROR]) -AC_SUBST([WNO_CONVERSION_NULL]) -AC_SUBST([WNO_TAUTOLOGICAL_COMPARE]) -AC_SUBST([WNO_PARENTHESES]) -AC_SUBST([WNO_UNINITIALIZED]) -AC_SUBST([WNO_UNUSED_VARIABLE]) -AC_SUBST([W_SUGGEST_OVERRIDE]) -AC_SUBST([W_NON_VIRTUAL_DTOR]) -AC_SUBST([FNO_STRICT_ALIASING]) - -CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_SUGGEST_OVERRIDE}" -CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_NON_VIRTUAL_DTOR}" - -# On Mac, we have to fix the visibility of standard library symbols. -# Otherwise, exported template instantiations---even though explicitly -# CVC4_PUBLIC, can be generated as symbols with internal-only linkage. -# Presumably, Apple is distributing a libstdc++ that is built *without* -# --enable-libstdcxx-visibility (?) -if test "$target_vendor" = apple; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\"" -fi - -# Doxygen configuration -AC_ARG_ENABLE([internals-documentation], - [AS_HELP_STRING([--enable-internals-documentation], - [build Doxygen documentation for static and private member functions])]) -if test "$enable_internals_documentation" = yes; then - DOXYGEN_EXTRACT_PRIVATE=YES - DOXYGEN_EXTRACT_STATIC=YES -else - DOXYGEN_EXTRACT_PRIVATE=NO - DOXYGEN_EXTRACT_STATIC=NO -fi -AC_SUBST([DOXYGEN_EXTRACT_PRIVATE]) -AC_SUBST([DOXYGEN_EXTRACT_STATIC]) - -DX_MAN_FEATURE(OFF) -DX_PDF_FEATURE(OFF) -DX_PS_FEATURE(OFF) -DX_DOT_FEATURE(OFF) -DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen) - -AC_ARG_ENABLE([unit-testing], AS_HELP_STRING([--disable-unit-testing], [do not build support for unit testing, even if available]), , [enable_unit_testing=check]) -AC_ARG_VAR(CXXTEST, [path to CxxTest installation]) -AC_ARG_WITH([cxxtest-dir], - [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])], - [CXXTEST="$withval"]) - -TESTS_ENVIRONMENT= -RUN_REGRESSION_ARGS= -if test "$with_lfsc" = yes; then - RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--with-lfsc" -fi -if test "$enable_proof" = yes; then - RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--enable-proof" -fi -AC_SUBST([TESTS_ENVIRONMENT]) -AC_SUBST([RUN_REGRESSION_ARGS]) - -AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)]) -AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)]) -AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)]) - -CXXTESTGEN= -if test "$enable_unit_testing" = "no"; then - AC_MSG_NOTICE([unit tests disabled by user request.]) - CXXTEST= -else - # The latest version of cxxtest distributed from the git repository places - # cxxtest under <cxxtest-root>/bin/cxxtest - AC_PATH_PROGS(CXXTESTGEN, - cxxtestgen.pl cxxtestgen.py cxxtestgen, - [], - [$CXXTEST:$CXXTEST/bin:$PATH]) - - if test -n "$CXXTESTGEN"; then - if "`basename $CXXTESTGEN`" = "cxxtestgen.pl"; then - if test -z "$PERL"; then - AC_CHECK_PROGS(PERL, perl, perl, []) - else - AC_CHECK_PROG(PERL, "$PERL", "$PERL", []) - fi - - if test -z "$PERL"; then - AC_MSG_WARN([unit tests disabled, perl not found.]) - CXXTESTGEN= - CXXTEST= - fi - fi - else - AC_MSG_NOTICE([unit tests disabled, could not find cxxtestgen.pl or cxxtestgen.py or cxxtestgen]) - CXXTEST= - fi - - # check if CxxTest headers exist and set include paths accordingly - if test -n "$CXXTESTGEN"; then - AC_MSG_CHECKING([for location of CxxTest headers]) - if test -n "$CXXTEST"; then - if test -e "$CXXTEST/cxxtest/TestRunner.h"; then - AC_MSG_RESULT([$CXXTEST]) - TEST_CPPFLAGS="${TEST_CPPFLAGS} -I$CXXTEST" - TEST_CXXFLAGS="${TEST_CXXFLAGS} -I$CXXTEST" - else - AC_MSG_RESULT([not found]) - AC_MSG_WARN([unit tests disabled, CxxTest headers not found at $CXXTEST.]) - CXXTESTGEN= - CXXTEST= - fi - # TODO: use more generic way to find cxxtest/TestRunner.h in system headers - elif test -e "/usr/include/cxxtest/TestRunner.h"; then - CXXTEST=/usr/include - AC_MSG_RESULT([$CXXTEST]) - else - CXXTEST=`dirname "$CXXTESTGEN"` - if test -e "$CXXTEST/cxxtest/TestRunner.h"; then - AC_MSG_RESULT([$CXXTEST]) - TEST_CPPFLAGS="${TEST_CPPFLAGS} -I$CXXTEST" - TEST_CXXFLAGS="${TEST_CXXFLAGS} -I$CXXTEST" - else - AC_MSG_RESULT([not found]) - AC_MSG_WARN([unit tests disabled, CxxTest headers not found.]) - CXXTESTGEN= - CXXTEST= - fi - fi - fi -fi - -if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then - AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.]) -fi - -AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"]) - -AC_ARG_VAR(PERL, [PERL interpreter (used when testing)]) - -# Python is now a required dependency for generating options code -AM_PATH_PYTHON([2.7],, [ - AC_MSG_ERROR([Python not found.]) -]) - -# Checks for libraries. - -AC_SEARCH_LIBS([clock_gettime], [rt pthread], - [AC_DEFINE([HAVE_CLOCK_GETTIME], [1], - [Defined to 1 if clock_gettime() is supported by the platform.])], - [AC_LIBOBJ([clock_gettime])]) -AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1], - [Defined to 1 if strtok_r() is supported by the platform.])]) -AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1], - [Defined to 1 if ffs() is supported by the platform.])]) - -AC_LIBOBJ([strtok_r ffs]) - -# Check for sigaltstack (missing in emscripten and mingw) -AC_CHECK_FUNC([sigaltstack], [AC_DEFINE([HAVE_SIGALTSTACK], [1], - [Defined to 1 if sigaltstack() is supported by the platform.])]) - -# Check for antlr C++ runtime (defined in config/antlr.m4) -AC_LIB_ANTLR - -# Check for user preferences for language bindings to build, and for -# build support. The arg list is the default set if unspecified by -# the user (the actual built set is the subset that appears to be -# supported by the build host). -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 ext/stdio_filebuf.h]) - -# Checks for typedefs, structures, and compiler characteristics. -#AC_HEADER_STDBOOL -# these are bad macros, they clash with system header <stdint.h> !! -#AC_TYPE_UINT16_T -#AC_TYPE_UINT32_T -#AC_TYPE_UINT64_T -#AC_TYPE_SIZE_T - -# guard against double-inclusion of the autoheader -AH_TOP([#ifndef __CVC4__CVC4AUTOCONFIG_H -#define __CVC4__CVC4AUTOCONFIG_H]) -AH_BOTTOM([#endif /* __CVC4__CVC4AUTOCONFIG_H */]) - -AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>]) - -# check with which standard strerror_r() complies -AC_FUNC_STRERROR_R - -# require boost library -BOOST_REQUIRE() - -# look for boost threading library -AC_ARG_WITH([portfolio], - AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)])) -cvc4_save_LDFLAGS="$LDFLAGS" -if test "$enable_static_binary" = yes; then - LDFLAGS="-static $LDFLAGS" -fi -cvc4_has_threads=yes -AC_ARG_ENABLE([thread-support], - AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library])) -if test "$enable_thread_support" = no; then - cvc4_has_threads=no - if test "$with_portfolio" = yes; then - AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory]) - fi -else - BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support]) - cvc4_has_threads=no]) -fi -LDFLAGS="$cvc4_save_LDFLAGS" -if test $cvc4_has_threads = no; then - if test "$enable_thread_support" = yes; then - AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?]) - fi - if test "$with_portfolio" = yes; then - AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?]) - fi - with_portfolio=no -fi -if test "$with_portfolio" != yes; then - with_portfolio=no -fi -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]) -# make the flags as close as possible to the final flags, because the Boost -# flags can bring in a different, incompatible readline library than we'd -# get otherwise (e.g. on Mac, where there are commonly two different readlines, -# one in /usr and one in /opt/local) -cvc4_rlcheck_save_CPPFLAGS="$CPPFLAGS" -cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS" -cvc4_rlcheck_save_CFLAGS="$CFLAGS" -cvc4_rlcheck_save_LDFLAGS="$LDFLAGS" -CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS" -CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED" -CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED -fexceptions" -LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS" -CVC4_CHECK_FOR_READLINE -CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS" -CXXFLAGS="$cvc4_rlcheck_save_CXXFLAGS" -CFLAGS="$cvc4_rlcheck_save_CFLAGS" -LDFLAGS="$cvc4_rlcheck_save_LDFLAGS" -AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline]) -AC_DEFINE_UNQUOTED([READLINE_COMPENTRY_FUNC_RETURNS_CHARP], $readline_compentry_func_returns_charp, [Define to 1 if rl_completion_entry_function is declared to return pointer to char]) -AC_SUBST([READLINE_LIBS]) - -# Whether to compile with google profiling tools -cvc4_use_google_perftools=0 -AC_ARG_WITH( - [google_perftools], - AS_HELP_STRING( - [--with-google-perftools], - [use Google Performance Tools] - ), - [if test "$withval" != no; then - cvc4_use_google_perftools=1 - fi - ] -) -AC_MSG_CHECKING([whether to link in google perftools libraries]) -if test $cvc4_use_google_perftools = 1; then - AC_MSG_RESULT([yes]) - AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread]) - AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread]) -else - AC_MSG_RESULT([no (user didn't request it)]) -fi - -# Java -AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)]) -AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)]) -AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)]) -AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)]) -if test "$cvc4_build_java_bindings"; then - dnl AM_PROG_GCJ - if test -z "$JAVA"; then - AC_CHECK_PROGS(JAVA, java, java, []) - else - AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", []) - fi - if test -z "$JAVAC"; then - AC_CHECK_PROGS(JAVAC, javac gcj, javac, []) - if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi - else - AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", []) - fi - if test -z "$JAVAH"; then - AC_CHECK_PROGS(JAVAH, javah gcjh, javah, []) - else - AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", []) - fi - if test -z "$JAR"; then - AC_CHECK_PROGS(JAR, jar, jar, []) - else - AC_CHECK_PROG(JAR, "$JAR", "$JAR", []) - fi -fi - -# on Mac OS X, Java doesn't like the .so module extension; it wants .dylib -module=no eval CVC4_JAVA_MODULE_EXT="$shrext_cmds" -if test -z "$CVC4_JAVA_MODULE_EXT"; then - CVC4_JAVA_MODULE_EXT=.so -fi -AC_SUBST([CVC4_JAVA_MODULE_EXT]) - -# Prepare configure output - -if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi -if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi -if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi -AC_SUBST(BUILDING_SHARED) -AC_SUBST(BUILDING_STATIC) -AC_SUBST(STATIC_BINARY) -AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes]) -AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes]) -AC_SUBST([COVERAGE_ON]) - -AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug]) -AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes]) - -AC_SUBST(CVC4_LIBRARY_VERSION) -AC_SUBST(CVC4_PARSER_LIBRARY_VERSION) -AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION) - -AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.]) -AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.]) -AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.]) -AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.]) -AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.]) - -CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS" -CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated" -CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions" -LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS" - -# visibility flag not supported for Windows builds -# also increase default stack size for Windows binaries -windows_build=no -case $host_os in - (*mingw*) FLAG_VISIBILITY_HIDDEN= - cvc4_LDFLAGS=-Wl,--stack,134217728 - pcvc4_LDFLAGS=-Wl,--stack,134217728 - windows_build=yes -esac - -AM_CONDITIONAL([CVC4_WINDOWS_BUILD], [test "$windows_build" = "yes"]) - -AC_SUBST(FLAG_VISIBILITY_HIDDEN) -AC_SUBST(cvc4_LDFLAGS) -AC_SUBST(pcvc4_LDFLAGS) - -AM_CONDITIONAL(WHITE_AND_BLACK_TESTS, [test -z "$FLAG_VISIBILITY_HIDDEN"]) - -# remember the command line used for configure -AC_SUBST(cvc4_config_cmdline) - -# mk_include -# -# When automake scans Makefiles, it complains about non-standard make -# features (including GNU extensions), and breaks GNU Make's -# "if/endif" construct, replacing the "if" with AM_CONDITIONAL if -# constructs. automake even follows "include" and messes with -# included Makefiles. -# -# CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we -# have to hide some included Makefiles with GNU extensions. We do -# this by defining mk_include as an autoconf substitution and then -# using "@mk_include@ other_makefile" in Makefile.am to include -# makefiles with GNU extensions; this hides them from automake. -mk_include=include -AC_SUBST(mk_include) -# Similar trickery for "if" -mk_if=if -AC_SUBST(mk_if) -mk_empty= -AC_SUBST(mk_empty) - -# CVC4_FALSE -# -# This is used to _always_ comment out rules in automake makefiles, but -# still trigger certain automake behavior; see test/unit/Makefile.am. -AM_CONDITIONAL([CVC4_FALSE], [false]) - -# set up substitutions for src/util/{rational,integer}.h.in -if test $cvc4_cln_or_gmp = cln; then - CVC4_USE_CLN_IMP=1 - CVC4_USE_GMP_IMP=0 -else - CVC4_USE_CLN_IMP=0 - CVC4_USE_GMP_IMP=1 -fi -AC_SUBST(CVC4_USE_CLN_IMP) -AC_SUBST(CVC4_USE_GMP_IMP) - -# month/year for man pages -MAN_DATE=`date '+%B %Y'` -AC_SUBST(MAN_DATE) - -AC_CONFIG_FILES([ - Makefile.builds - 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$,,']) -) - -if test $cvc4_has_threads = yes; then - support_multithreaded='with boost threading library' - AM_CONDITIONAL([CVC4_HAS_THREADS], [true]) - AC_SUBST([CVC4_HAS_THREADS], 1) -else - support_multithreaded='no' - AM_CONDITIONAL([CVC4_HAS_THREADS], [false]) - AC_SUBST([CVC4_HAS_THREADS], 0) -fi - -# Final information to the user -gpl=no -licensewarn= - -if test "$custom_build_profile" = yes; then - with_build="$with_build (customized)" -fi - -support_unit_tests='cxxtest not found; unit tests not supported' -if test -n "$CXXTEST"; then - support_unit_tests='unit testing infrastructure enabled in build directory' -elif test "$enable_unit_testing" = no; then - support_unit_tests='unit testing disabled by user' -fi - -if test "$enable_optimized" = yes; then - optimized="yes, at level $OPTLEVEL" -else - optimized="no" -fi - -if test $have_libglpk -eq 1; then - gpl=yes - gpllibs="${gpllibs} glpk" -fi - -if test $have_libreadline -eq 1; then - gpl=yes - gpllibs="${gpllibs} readline" -fi - -if test $cvc4_cln_or_gmp = cln; then - mplibrary='cln (GPL)' - gpl=yes - gpllibs="${gpllibs} cln" - if test $with_portfolio = yes; then - AC_ERROR([Bad configuration detected: cannot build portfolio with CLN. -Please specify only one of --with-portfolio and --with-cln.]) - fi -else - mplibrary='gmp' -fi - -if test "$gpl" = yes; then - 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}"'**************************************************************************** -Please note that CVC4 will be built against the following GPLed libraries: - '"$gpllibs"' -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", 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 - -if test "$gpl" = yes; then isgpl=1; else isgpl=0; fi -AC_DEFINE_UNQUOTED(CVC4_GPL_DEPS, $isgpl, [Whether CVC4 is built with the (optional) GPLed library dependences.]) - -CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION" -if test -z "$CVC4_LANGUAGE_BINDINGS"; then - CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A" -fi - -bindings_to_be_built=none -if test -n "$CVC4_LANGUAGE_BINDINGS"; then - bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS" -fi - -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/floatingpoint.h]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.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]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3]) - -AC_OUTPUT - -cat <<EOF - -CVC4 $VERSION - -Build profile: $with_build -Build ID : $build_type -Optimized : $optimized -Debug symbols: $enable_debug_symbols -Proofs : $enable_proof -Statistics : $enable_statistics -Replay : $enable_replay -Assertions : $enable_assertions -Tracing : $enable_tracing -Dumping : $enable_dumping -Muzzle : $enable_muzzle - -Unit tests : $support_unit_tests -gcov support : $enable_coverage -gprof support: $enable_profiling - -Static libs : $enable_static -Shared libs : $enable_shared -Static binary: $enable_static_binary -Bindings : $bindings_to_be_built - -Multithreaded: $support_multithreaded -Portfolio : $with_portfolio - -ABC : $with_abc -CaDiCaL : $with_cadical -Cryptominisat: $with_cryptominisat -GLPK : $with_glpk -LFSC : $with_lfsc -MP library : $mplibrary -Readline : $with_readline -SymFPU : $with_symfpu - -CPPFLAGS : $CPPFLAGS -CXXFLAGS : $CXXFLAGS -CFLAGS : $CFLAGS -LIBS : $LIBS -LDFLAGS : $LDFLAGS - -libcvc4 version : $CVC4_LIBRARY_VERSION -libcvc4parser version : $CVC4_PARSER_LIBRARY_VERSION -libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild - -Install into : $prefix - -CVC4 license : $license - -${licensewarn}Now just type make, followed by make check or make install, as you like. - -EOF - -if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then - AC_MSG_WARN([]) - 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 - -if test -n "$CVC4_INTEGRITY_WARNING"; then - AC_MSG_WARN([]) - AC_MSG_WARN($CVC4_INTEGRITY_WARNING) - AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library]) - AC_MSG_WARN([]) -fi |