configure.ac

   1 #                                               -*- Autoconf -*-
   2 # Process this file with autoconf to produce a configure script.
   3
   4 m4_define(_CVC4_MAJOR,          1)       dnl version (major)
   5 m4_define(_CVC4_MINOR,          7)       dnl version (minor)
   6 m4_define(_CVC4_RELEASE,        0)       dnl version (alpha)
   7 m4_define(_CVC4_EXTRAVERSION,   [-prerelease])      dnl version (extra)
   8 m4_define(_CVC4_RELEASE_STRING, _CVC4_MAJOR[.]_CVC4_MINOR[]m4_if(_CVC4_RELEASE,[0],,[.]_CVC4_RELEASE)_CVC4_EXTRAVERSION) dnl version string
   9
  10 dnl Preprocess CL args. Defined in config/cvc4.m4
  11 CVC4_AC_INIT
  12
  13 AC_PREREQ([2.61])
  14 AC_INIT([cvc4], _CVC4_RELEASE_STRING, [cvc4-bugs@cs.stanford.edu])
  15 AC_CONFIG_SRCDIR([src/include/cvc4_public.h])
  16 AC_CONFIG_AUX_DIR([config])
  17 AC_REQUIRE_AUX_FILE([tap-driver.sh])
  18 AC_CONFIG_MACRO_DIR([config])
  19 AC_CONFIG_LIBOBJ_DIR([src/lib])
  20
  21 m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])])
  22
  23 CVC4_MAJOR=_CVC4_MAJOR
  24 CVC4_MINOR=_CVC4_MINOR
  25 CVC4_RELEASE=_CVC4_RELEASE
  26 CVC4_EXTRAVERSION=_CVC4_EXTRAVERSION
  27 CVC4_RELEASE_STRING=_CVC4_RELEASE_STRING
  28
  29 # Libtool version numbers for libraries
  30 # Version numbers are in the form current:revision:age
  31 #
  32 # current -
  33 #   increment if interfaces have been added, removed or changed
  34 # revision -
  35 #   increment if source code has changed
  36 #   set to zero if current is incremented
  37 # age -
  38 #   increment if interfaces have been added
  39 #   set to zero if interfaces have been removed
  40 #   or changed
  41 #
  42 # For more information, see:
  43 # http://www.gnu.org/software/libtool/manual/libtool.html#Versioning
  44 # For guidance on when to change the version number, refer to the
  45 # developer's guide.
  46
  47 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])])
  48
  49 m4_define(_CVC4_LIBRARY_VERSION, library_version([libcvc4]))dnl
  50 m4_define(_CVC4_PARSER_LIBRARY_VERSION, library_version([libcvc4parser]))dnl
  51 m4_define(_CVC4_BINDINGS_LIBRARY_VERSION, library_version([libcvc4bindings]))dnl
  52
  53 m4_define([fatal_error], [m4_errprint(__program__:__file__:__line__[: fatal error: $*
  54 ])m4_exit(1)])dnl
  55
  56 m4_ifblank(_CVC4_LIBRARY_VERSION,[fatal_error([no CVC4_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl
  57 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
  58 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
  59
  60 CVC4_LIBRARY_VERSION=_CVC4_LIBRARY_VERSION
  61 CVC4_PARSER_LIBRARY_VERSION=_CVC4_PARSER_LIBRARY_VERSION
  62 CVC4_BINDINGS_LIBRARY_VERSION=_CVC4_BINDINGS_LIBRARY_VERSION
  63
  64 # Using AX_CXX_COMPILE_STDCXX_11 and the AC_CANONICAL_* macros destroy the
  65 # command line you get from $@, which we want later for determining the build
  66 # profile.  So we save it.
  67 # (We can't do our build profile stuff here, or it's not included in the
  68 # output... autoconf overrides us on the orderings of some things.)
  69 config_cmdline=("$@")
  70 cvc4_config_cmdline="${config_cmdline[[@]]}"
  71
  72 # remember if the user set these explicitly (or whether autoconf does)
  73 user_specified_enable_or_disable_static=${enable_static+yes}
  74 user_specified_enable_or_disable_shared=${enable_shared+yes}
  75
  76 if test -e src/include/cvc4_public.h; then
  77   CVC4_CONFIGURE_AT_TOP_LEVEL=yes
  78 else
  79   CVC4_CONFIGURE_AT_TOP_LEVEL=no
  80 fi
  81
  82 # override autoconf: we don't want it giving us CFLAGS/CXXFLAGS, but we do
  83 # want to respect the user's flags
  84 if test -z "${CFLAGS+set}"; then CFLAGS=; fi
  85 if test -z "${CXXFLAGS+set}"; then CXXFLAGS=; fi
  86
  87 # on by default
  88 AM_MAINTAINER_MODE([enable])
  89
  90 # turn off static lib building by default
  91 AC_ENABLE_SHARED
  92 AC_DISABLE_STATIC
  93
  94 AC_CANONICAL_BUILD
  95 AC_CANONICAL_HOST
  96 AC_CANONICAL_TARGET
  97
  98 # C++11 support in the compiler is now mandatory. Check for support and add
  99 # switches if necessary.
 100 AX_CXX_COMPILE_STDCXX_11([ext], [mandatory])
 101
 102 as_me=configure
 103
 104 if test "$enable_shared" = no -a "$user_specified_enable_or_disable_shared" = yes; then
 105   enable_static=yes
 106 fi
 107
 108 # Features requested by the user
 109 AC_MSG_CHECKING([for requested build profile])
 110 AC_ARG_WITH([build],
 111   [AS_HELP_STRING([--with-build=profile],
 112      [for profile in {production,debug,competition,testing}])])
 113
 114 if test -z "${with_build+set}"; then
 115   with_build=production
 116 fi
 117 if test -z "${enable_optimized+set}" -a \
 118         -z "${enable_debug_symbols+set}" -a \
 119         -z "${enable_assertions+set}" -a \
 120         -z "${enable_tracing+set}" -a \
 121         -z "${enable_dumping+set}" -a \
 122         -z "${enable_muzzle+set}" -a \
 123         -z "${enable_coverage+set}" -a \
 124         -z "${enable_profiling+set}" -a \
 125         -z "${enable_statistics+set}" -a \
 126         -z "${enable_replay+set}" -a \
 127         -z "${with_gmp+set}" -a \
 128         -z "${with_cln+set}" -a \
 129         -z "${with_glpk+set}" -a \
 130         -z "${with_abc+set}" -a \
 131         -z "${with_cadical+set}" -a \
 132         -z "${with_cryptominisat+set}" -a \
 133         -z "${with_lfsc+set}" -a \
 134         -z "${with_symfpu+set}"; then
 135   custom_build_profile=no
 136 else
 137   custom_build_profile=yes
 138 fi
 139 btargs=
 140 if test -n "${enable_optimized+set}"; then
 141   if test "$enable_optimized" = yes; then
 142     btargs="$btargs optimized"
 143   else
 144     btargs="$btargs nooptimized"
 145   fi
 146 fi
 147 # --enable-staticbinary is an alias for --enable-static-binary
 148 if test -n "${enable_staticbinary+set}"; then
 149   enable_static_binary="$enable_staticbinary"
 150 fi
 151 if test -n "${enable_static_binary+set}"; then
 152   if test "$enable_static_binary" = yes; then
 153     btargs="$btargs staticbinary"
 154   else
 155     btargs="$btargs nostaticbinary"
 156   fi
 157 fi
 158 if test -n "${enable_debug_symbols+set}"; then
 159   if test "$enable_debug_symbols" = yes; then
 160     btargs="$btargs debugsymbols"
 161   else
 162     btargs="$btargs nodebugsymbols"
 163   fi
 164 fi
 165 if test -n "${enable_assertions+set}"; then
 166   if test "$enable_assertions" = yes; then
 167     btargs="$btargs assertions"
 168   else
 169     btargs="$btargs noassertions"
 170   fi
 171 fi
 172 if test -n "${enable_proof+set}"; then
 173   if test "$enable_proof" = yes; then
 174     btargs="$btargs proof"
 175   else
 176     btargs="$btargs noproof"
 177   fi
 178 fi
 179 if test -n "${enable_tracing+set}"; then
 180   if test "$enable_tracing" = yes; then
 181     btargs="$btargs tracing"
 182   else
 183     btargs="$btargs notracing"
 184   fi
 185 fi
 186 if test -n "${enable_dumping+set}"; then
 187   if test "$enable_dumping" = yes; then
 188     btargs="$btargs dumping"
 189   else
 190     btargs="$btargs nodumping"
 191   fi
 192 fi
 193 if test -n "${enable_muzzle+set}"; then
 194   if test "$enable_muzzle" = yes; then
 195     btargs="$btargs muzzle"
 196   else
 197     btargs="$btargs nomuzzle"
 198   fi
 199 fi
 200 if test -n "${enable_coverage+set}"; then
 201   if test "$enable_coverage" = yes; then
 202     btargs="$btargs coverage"
 203   else
 204     btargs="$btargs nocoverage"
 205   fi
 206 fi
 207 if test -n "${enable_profiling+set}"; then
 208   if test "$enable_profiling" = yes; then
 209     btargs="$btargs profiling"
 210   else
 211     btargs="$btargs noprofiling"
 212   fi
 213 fi
 214 if test -n "${enable_statistics+set}"; then
 215   if test "$enable_statistics" = yes; then
 216     btargs="$btargs statistics"
 217   else
 218     btargs="$btargs nostatistics"
 219   fi
 220 fi
 221 if test -n "${enable_replay+set}"; then
 222   if test "$enable_replay" = yes; then
 223     btargs="$btargs replay"
 224   else
 225     btargs="$btargs noreplay"
 226   fi
 227 fi
 228 if test -n "${with_glpk+set}"; then
 229   if test "$with_glpk" = yes; then
 230     btargs="$btargs glpk"
 231   fi
 232 fi
 233 if test -n "${with_abc+set}"; then
 234   if test "$with_abc" = yes; then
 235     btargs="$btargs abc"
 236   fi
 237 fi
 238 if test -n "${with_cadical+set}"; then
 239   if test "$with_cadical" = yes; then
 240     btargs="$btargs cadical"
 241   fi
 242 fi
 243 if test -n "${with_cryptominisat+set}"; then
 244   if test "$with_cryptominisat" = yes; then
 245     btargs="$btargs cryptominisat"
 246   fi
 247 fi
 248 if test -n "${with_lfsc+set}"; then
 249   if test "$with_lfsc" = yes; then
 250     enable_proof=yes
 251     btargs="$btargs lfsc"
 252   fi
 253 fi
 254 if test -n "${with_symfpu+set}"; then
 255   if test "$with_symfpu" = yes; then
 256     btargs="$btargs symfpu"
 257   fi
 258 fi
 259
 260 AC_MSG_RESULT([$with_build])
 261
 262 AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
 263 AC_CONFIG_HEADERS([cvc4autoconfig.h])
 264
 265 # automake 1.12 changes the test driver mechanism in a way that is
 266 # completely incompatible with 1.11.  We figure out here which version
 267 # we're using in order to set up test makefiles correctly.
 268 # See http://lists.gnu.org/archive/html/automake/2012-04/msg00060.html
 269 if test -z "$am__api_version"; then
 270   AC_MSG_ERROR([Cannot determine automake API version ?!])
 271 fi
 272 case "$am__api_version" in
 273   1.11*) automake111=true ;;
 274   *) automake111=false ;;
 275 esac
 276 AM_CONDITIONAL([AUTOMAKE_1_11], [$automake111])
 277
 278 # Initialize libtool's configuration options.
 279 # we're not DLL-clean yet (i.e., don't properly use dllexport and dllimport)
 280 # _LT_SET_OPTION([LT_INIT],[win32-dll])
 281 LT_INIT
 282
 283 # Checks for programs.
 284 AC_PROG_CC
 285 AC_PROG_CXX
 286 AC_PROG_INSTALL
 287
 288 CVC4_GCC_VERSION
 289
 290 if test $cross_compiling = "no"; then
 291   AC_MSG_CHECKING([whether C++ exceptions work])
 292   AC_LANG_PUSH([C++])
 293   AC_RUN_IFELSE(
 294     AC_LANG_PROGRAM([#include <exception>], [[
 295       int result = 1;
 296       try {
 297         throw std::exception();
 298       } catch (...) {
 299         result = 0;
 300       }
 301       return result;
 302     ]]),
 303     [AC_MSG_RESULT([yes])],
 304     [AC_MSG_ERROR([C++ exceptions do not work.])]
 305   )
 306   AC_LANG_POP([C++])
 307 else
 308   AC_MSG_WARN([Cross compiling, cannot check whether exceptions work])
 309 fi
 310
 311 cvc4_use_gmp=2
 312 cvc4_use_cln=2
 313
 314 AC_ARG_WITH(
 315   [cln],
 316   AS_HELP_STRING(
 317     [--with-cln],
 318     [use CLN instead of GMP]
 319   ),
 320   [case "$withval" in
 321    y|ye|yes|Y|YE|YES) cvc4_use_cln=1 ;;
 322    n|no|N|NO) cvc4_use_cln=0 ;;
 323    esac
 324   ]
 325 )
 326
 327 AC_ARG_WITH(
 328   [gmp],
 329   AS_HELP_STRING(
 330     [--with-gmp],
 331     [use GMP instead of CLN]
 332   ),
 333   [case "$withval" in
 334    y|ye|yes|Y|YE|YES) cvc4_use_gmp=1 ;;
 335    n|no|N|NO) cvc4_use_gmp=0 ;;
 336    esac
 337   ]
 338 )
 339
 340 if test $cvc4_use_cln = 1 -a $cvc4_use_gmp = 1 || test $cvc4_use_cln = 0 -a $cvc4_use_gmp = 0; then
 341   AC_MSG_ERROR([You must use either CLN and GMP.  Please pick one.])
 342 fi
 343 if test $cvc4_use_gmp = 1; then
 344   cvc4_use_cln=0
 345 elif test $cvc4_use_gmp = 0; then
 346   cvc4_use_cln=1
 347 elif test $cvc4_use_cln = 1; then
 348   cvc4_use_gmp=0
 349 elif test $cvc4_use_cln = 0; then
 350   cvc4_use_gmp=1
 351 fi
 352
 353 # try GMP, fail if not found; GMP is required for both CLN and for GMP
 354 # versions of CVC4
 355 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
 356
 357 if test $cvc4_use_cln = 2; then
 358   if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1 -o "$with_portfolio" = yes; then
 359     cvc4_use_cln=0
 360     cvc4_use_gmp=1
 361   fi
 362 fi
 363
 364 if test $cvc4_use_cln != 0; then
 365   # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
 366   # gracefully.  You can only specify it once for a given library name.  That
 367   # is, even on separate if/else branches, you can't put
 368   # PKG_CHECK_MODULES([CLN], ...).  That's why things are so convoluted here,
 369   # we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
 370   PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
 371     [AC_LANG_PUSH([C++])
 372      save_LIBS="$LIBS"
 373      save_CXXFLAGS="$CXXFLAGS"
 374      LIBS="$CLN_LIBS $LIBS"
 375      CXXFLAGS="$CLN_CFLAGS $CXXFLAGS"
 376      AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])], [
 377        cvc4_use_cln=1
 378      ], [
 379        if test $cvc4_use_cln = 1; then
 380          # fail
 381          AC_MSG_ERROR([CLN installation missing, too old, or not functional for this architecture])
 382        else
 383          # fall back to GMP
 384          AC_MSG_NOTICE([CLN installation missing, too old, or not functional for this architecture, will use gmp instead])
 385          cvc4_use_cln=0
 386          cvc4_use_gmp=1
 387        fi
 388      ])
 389      CXXFLAGS="$save_CXXFLAGS"
 390      LIBS="$save_LIBS"
 391      AC_LANG_POP([C++])
 392     ],
 393     [if test $cvc4_use_cln = 1; then
 394        # fail
 395        AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
 396      else
 397        # fall back to GMP
 398        AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
 399        cvc4_use_cln=0
 400        cvc4_use_gmp=1
 401      fi
 402     ]
 403   )
 404 fi
 405 if test $cvc4_use_cln = 0; then
 406   # try GMPXX, fail if not found; don't need to link against it, only need its header
 407   AC_LANG_PUSH([C++])
 408   AC_CHECK_HEADER([gmpxx.h], , [AC_MSG_ERROR([GNU MP C++ library header (gmpxx.h) required but not found, see http://gmplib.org/])])
 409   AC_LANG_POP([C++])
 410   cvc4_cln_or_gmp=gmp
 411 else
 412   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
 413   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
 414   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
 415   LIBS="$CLN_LIBS${LIBS:+ $LIBS}"
 416   cvc4_cln_or_gmp=cln
 417 fi
 418
 419 if test $cvc4_cln_or_gmp = cln; then
 420   AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.])
 421 else
 422   AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.])
 423 fi
 424 AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln])
 425 AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
 426
 427 # Dumping cannot be used in a portfolio build. Disable dumping by default when
 428 # a portfolio build has been requested, throw an error if dumping has been
 429 # explicitly requested with a portfolio build.
 430 if test "$with_portfolio" = yes; then
 431   if test "$enable_dumping" = yes; then
 432     AC_MSG_ERROR([Dumping is not supported with a portfolio build])
 433   fi
 434   enable_dumping=no
 435 fi
 436
 437 # construct the build string
 438 AC_MSG_CHECKING([for appropriate build string])
 439 if test -z "$ac_confdir"; then
 440   ac_confdir="$srcdir"
 441 fi
 442 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
 443 AC_MSG_RESULT($build_type)
 444
 445 # Require building in target and build-specific build directory:
 446 #
 447 # If the configure script is invoked from the top-level source
 448 # directory, it creates a suitable build directory (based on the build
 449 # architecture and build profile from $build_type), changes into it,
 450 # and reinvokes itself.  CVC4_CONFIGURE_IN_BUILDS is an envariable
 451 # that breaks any possibility of infinite recursion in this process.
 452 AC_MSG_CHECKING([what dir to configure])
 453 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
 454   AC_MSG_RESULT([this one (in builds/)])
 455 elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
 456   AC_MSG_RESULT([builds/$target/$build_type])
 457   $as_echo
 458   if test -z "$ac_srcdir"; then
 459     mkbuilddir=./config/mkbuilddir
 460   else
 461     mkbuilddir=$ac_srcdir/config/mkbuilddir
 462   fi
 463   $as_echo "$mkbuilddir $target $build_type"
 464   source $mkbuilddir "$target" "$build_type"
 465   $as_echo "cd builds/$target/$build_type"
 466   cd "builds/$target/$build_type"
 467   CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
 468   # Runs the single recursive configure invocation using a relative path.
 469   # See https://lists.gnu.org/archive/html/autoconf/2011-04/msg00060.html
 470   echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
 471   "$SHELL" "../../../configure" "${config_cmdline[[@]]}"
 472   exitval=$?
 473   cd ../../..
 474   if test $exitval -eq 0; then
 475     cat >config.reconfig <<EOF
 476 [#!/bin/bash
 477 # Generated by configure, `date`
 478 # This script is part of CVC4.
 479
 480 cd "\`dirname \\"\$0\\"\`"
 481
 482 if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi
 483
 484 current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`)
 485 arch=\${current[0]}
 486 build=\${current[1]}
 487
 488 echo "reconfiguring in builds/\$arch/\$build..."
 489 cd "builds/\$arch/\$build"
 490 echo ./config.status "\$@"
 491 ./config.status "\$@"]
 492 EOF
 493     chmod +x config.reconfig
 494   fi
 495   ln -sf "$target/$build_type/config.log" "builds/config.log"
 496   exit $exitval
 497 else
 498   AC_MSG_RESULT([this one (user-specified)])
 499 fi
 500
 501 as_me=configure
 502
 503 # Unpack standard build types. Any particular options can be overriden with
 504 # --enable/disable-X options
 505 # Tim: This needs to keep CVC4CPPFLAGS, CVC4CXXFLAGS, etc. set by earlier checks
 506 case "$with_build" in
 507   production) # highly optimized, no assertions, no tracing, dumping
 508     CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
 509     CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
 510     CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
 511     CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
 512     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
 513     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=3                       ; fi
 514     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 515     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no          ; fi
 516     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
 517     if test -z "${enable_replay+set}"       ; then enable_replay=no                 ; fi
 518     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
 519     if test -z "${enable_proof+set}"        ; then enable_proof=yes                 ; fi
 520     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
 521     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
 522     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 523     if test -z "${enable_valgrind+set}"     ; then enable_valgrind=no               ; fi
 524     ;;
 525   debug) # unoptimized, debug symbols, assertions, tracing, dumping
 526     CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG"
 527     CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-fno-inline"
 528     CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-fno-inline"
 529     CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
 530     FLAG_VISIBILITY_HIDDEN=
 531     if test -z "${enable_optimized+set}"    ; then enable_optimized=no              ; fi
 532     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
 533     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
 534     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
 535     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
 536     if test -z "${enable_proof+set}"        ; then enable_proof=yes                 ; fi
 537     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
 538     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
 539     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 540     if test -z "${enable_valgrind+set}"     ; then enable_valgrind=optional         ; fi
 541     ;;
 542   testing) # moderately optimized, assertions, tracing, dumping
 543     CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
 544     CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
 545     CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
 546     CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
 547     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
 548     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=2                       ; fi
 549     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 550     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
 551     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
 552     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
 553     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
 554     if test -z "${enable_proof+set}"        ; then enable_proof=yes                 ; fi
 555     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
 556     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
 557     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 558     if test -z "${enable_valgrind+set}"     ; then enable_valgrind=no               ; fi
 559     ;;
 560   competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
 561     CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COMPETITION_MODE"
 562     CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
 563     CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
 564     CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
 565     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
 566     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=9                       ; fi
 567     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 568     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no          ; fi
 569     if test -z "${enable_statistics+set}"   ; then enable_statistics=no             ; fi
 570     if test -z "${enable_replay+set}"       ; then enable_replay=no                 ; fi
 571     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
 572     if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
 573     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
 574     if test -z "${enable_dumping+set}"      ; then enable_dumping=no                ; fi
 575     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=yes                ; fi
 576     if test -z "${enable_valgrind+set}"     ; then enable_valgrind=no               ; fi
 577     if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi
 578     if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi
 579     if test -z "${enable_static_binary+set}"; then enable_static_binary=yes         ; fi
 580     ;;
 581   *)
 582     AC_MSG_FAILURE([unknown build profile: $with_build])
 583     ;;
 584 esac
 585 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
 586
 587 AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION],  [test "$with_build" = production])
 588 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG],       [test "$with_build" = debug])
 589 AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
 590 AM_CONDITIONAL([CVC4_BUILD_PROFILE_TESTING],     [test "$with_build" = testing])
 591
 592 # permit a static binary
 593 AC_MSG_CHECKING([whether to build a static binary])
 594 AC_ARG_ENABLE([static-binary],
 595      [AS_HELP_STRING([--enable-static-binary],
 596                      [build a fully statically-linked binary [default=no]])])
 597 if test -z "${enable_static_binary+set}"; then
 598   enable_static_binary=no
 599 fi
 600 AC_MSG_RESULT([$enable_static_binary])
 601 if test "$enable_static_binary" = yes; then
 602   if test "$target_vendor" = apple; then
 603     if test -z "$MAC_STATIC_BINARY_MANUAL_OVERRIDE"; then
 604       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)]])
 605     else
 606       AC_MSG_WARN([MAC_STATIC_BINARY_MANUAL_OVERRIDE was set!])
 607       AC_MSG_WARN([Will make a static binary during this build.  Note that it may fail!])
 608     fi
 609   fi
 610   if test "$enable_static" != yes; then
 611     enable_static=yes
 612     AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
 613   fi
 614 fi
 615
 616 AC_MSG_CHECKING([whether to support proofs in libcvc4])
 617
 618 AC_ARG_ENABLE([proof],
 619   [AS_HELP_STRING([--disable-proof],
 620      [do not support proof generation])])
 621 if test -z "${enable_proof+set}"; then
 622   enable_proof=yes
 623 fi
 624 AC_MSG_RESULT([$enable_proof])
 625
 626 if test "$enable_proof" = yes; then
 627   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
 628 fi
 629 AM_CONDITIONAL([CVC4_PROOF], [test "$enable_proof" = yes])
 630
 631 AC_MSG_CHECKING([whether to optimize libcvc4])
 632
 633 AC_ARG_ENABLE([optimized],
 634   [AS_HELP_STRING([--enable-optimized],
 635      [optimize the build])])
 636
 637 if test -z "${enable_optimized+set}"; then
 638   enable_optimized=no
 639 fi
 640
 641 AC_MSG_RESULT([$enable_optimized])
 642
 643 if test "$enable_optimized" = yes; then
 644   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
 645   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
 646 else
 647   # Use -Og if available (optimizations that do not interfere with debugging),
 648   # -O0 otherwise
 649   debug_optimization_level="-O0"
 650   CVC4_CXX_OPTION([-Og], [debug_optimization_level])
 651   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${debug_optimization_level}"
 652   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }${debug_optimization_level}"
 653 fi
 654
 655 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
 656
 657 AC_ARG_ENABLE([debug-symbols],
 658   [AS_HELP_STRING([--disable-debug-symbols],
 659      [do not include debug symbols in libcvc4])])
 660
 661 if test -z "${enable_debug_symbols+set}"; then
 662   enable_debug_symbols=yes
 663 fi
 664
 665 AC_MSG_RESULT([$enable_debug_symbols])
 666
 667 if test "$enable_debug_symbols" = yes; then
 668   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3"
 669   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
 670 fi
 671
 672 AC_MSG_CHECKING([whether to enable Valgrind instrumentation])
 673
 674 AC_ARG_ENABLE([valgrind],
 675   [AS_HELP_STRING([--enable-valgrind],
 676      [enable Valgrind instrumentation])])
 677
 678 if test -z "${enable_valgrind+set}"; then
 679   enable_valgrind=no
 680 fi
 681
 682 AC_MSG_RESULT([$enable_valgrind])
 683
 684 if test "$enable_valgrind" != no; then
 685   # Valgrind instrumentation is either explicitly enabled (enable_valgrind=yes)
 686   # or enabled if available (enable_valgrind=optional)
 687   AC_CHECK_HEADER([valgrind/memcheck.h],
 688                   [CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_VALGRIND"],
 689                   [if test "$enable_valgrind" = yes; then
 690                     AC_MSG_ERROR([Need valgrind/memcheck.h to enable Valgrind instrumentation])
 691                    else
 692                     AC_MSG_NOTICE([valgrind/memcheck.h missing, Valgrind instrumentation disabled])
 693                    fi
 694                   ])
 695 fi
 696
 697 AC_MSG_CHECKING([whether to use the debug context memory manager])
 698
 699 AC_ARG_ENABLE([debug-context-memory-manager],
 700   [AS_HELP_STRING([--enable-debug-context-memory-manager],
 701      [use the debug context memory manager])])
 702
 703 if test -z "${enable_debug_context_memory_manager+set}"; then
 704   enable_debug_context_memory_manager=no
 705 fi
 706
 707 AC_MSG_RESULT([$enable_debug_context_memory_manager])
 708
 709 if test "$enable_debug_context_memory_manager" = yes; then
 710   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER"
 711 fi
 712
 713 AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])
 714
 715 AC_ARG_ENABLE([statistics],
 716   [AS_HELP_STRING([--disable-statistics],
 717      [do not include statistics in libcvc4])])
 718
 719 if test -z "${enable_statistics+set}"; then
 720   enable_statistics=yes
 721 fi
 722
 723 AC_MSG_RESULT([$enable_statistics])
 724
 725 if test "$enable_statistics" = yes; then
 726   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
 727 fi
 728
 729 AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
 730
 731 AC_ARG_ENABLE([replay],
 732   [AS_HELP_STRING([--disable-replay],
 733      [turn off the replay feature in libcvc4])])
 734
 735 if test -z "${enable_replay+set}"; then
 736   enable_replay=yes
 737 fi
 738
 739 AC_MSG_RESULT([$enable_replay])
 740
 741 if test "$enable_replay" = yes; then
 742   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
 743 fi
 744
 745 AC_MSG_CHECKING([whether to include assertions in build])
 746
 747 AC_ARG_ENABLE([assertions],
 748   [AS_HELP_STRING([--disable-assertions],
 749      [turn off assertions in build])])
 750
 751 if test -z "${enable_assertions+set}"; then
 752   enable_assertions=yes
 753 fi
 754
 755 AC_MSG_RESULT([$enable_assertions])
 756
 757 if test "$enable_assertions" = yes; then
 758   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS"
 759 else
 760   # turn off regular C assert() also
 761   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG"
 762 fi
 763
 764 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
 765 AC_ARG_ENABLE([tracing],
 766   [AS_HELP_STRING([--disable-tracing],
 767      [remove all tracing code from CVC4])])
 768
 769 if test -z "${enable_tracing+set}"; then
 770   enable_tracing=yes
 771 fi
 772
 773 AC_MSG_RESULT([$enable_tracing])
 774
 775 if test "$enable_tracing" = yes; then
 776   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
 777 fi
 778
 779 AC_MSG_CHECKING([whether to do a dump-capable build of CVC4])
 780 AC_ARG_ENABLE([dumping],
 781   [AS_HELP_STRING([--disable-dumping],
 782      [remove all dumping code from CVC4])])
 783
 784 if test -z "${enable_dumping+set}"; then
 785   enable_dumping=yes
 786 fi
 787
 788 AC_MSG_RESULT([$enable_dumping])
 789
 790 if test "$enable_dumping" = yes; then
 791   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING"
 792 fi
 793
 794 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
 795 AC_ARG_ENABLE([muzzle],
 796   [AS_HELP_STRING([--enable-muzzle],
 797      [completely silence CVC4; remove ALL non-result output from build])])
 798
 799 if test -z "${enable_muzzle+set}"; then
 800   enable_muzzle=no
 801 fi
 802
 803 AC_MSG_RESULT([$enable_muzzle])
 804
 805 if test "$enable_muzzle" = yes; then
 806   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE"
 807 fi
 808
 809 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
 810 AC_ARG_ENABLE([coverage],
 811   [AS_HELP_STRING([--enable-coverage],
 812      [build with support for gcov coverage testing])])
 813
 814 if test -z "${enable_coverage+set}"; then
 815   enable_coverage=no
 816   # make COVERAGE_ON the empty string for makefile conditional function
 817   # $(if $(COVERAGE_ON), action1, action2)
 818   COVERAGE_ON=
 819 fi
 820
 821 AC_MSG_RESULT([$enable_coverage])
 822
 823 if test "$enable_coverage" = yes; then
 824   # For coverage testing, we prefer:
 825   #     --enable-static --disable-shared --disable-static-binary
 826   # If the user didn't specify these, we force them here.  If the
 827   # user specified them in opposite phase, give warnings that they
 828   # shouldn't do that, or bomb out.
 829   COVERAGE_ON=yes
 830   if test "$user_specified_enable_or_disable_shared" != yes; then
 831     enable_shared=no
 832     AC_MSG_WARN([turning off shared library building due to --enable-coverage])
 833   elif test "$enable_shared" = yes; then
 834     AC_MSG_WARN([])
 835     AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared])
 836     AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.])
 837     AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.])
 838     AC_MSG_WARN([])
 839   fi
 840   if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then
 841     AC_MSG_WARN([])
 842     AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary])
 843     AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.])
 844     AC_MSG_WARN([])
 845   fi
 846   if test "$user_specified_enable_or_disable_static" != yes; then
 847     enable_static=yes
 848     AC_MSG_WARN([turning on static library building due to --enable-coverage])
 849   elif test "$enable_static" != yes; then
 850     AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.])
 851   fi
 852
 853   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE"
 854   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage"
 855   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage"
 856   CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage"
 857 fi
 858
 859 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
 860
 861 AC_ARG_ENABLE([profiling],
 862   [AS_HELP_STRING([--enable-profiling],
 863      [build with support for gprof profiling])])
 864
 865 if test -z "${enable_profiling+set}"; then
 866   enable_profiling=no
 867 fi
 868
 869 AC_MSG_RESULT([$enable_profiling])
 870
 871 if test "$enable_profiling" = yes; then
 872   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING"
 873   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg"
 874   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg"
 875   CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
 876 fi
 877
 878 # Check for libglpk (defined in config/glpk.m4)
 879 AC_ARG_WITH([glpk],
 880   [AS_HELP_STRING([--with-glpk],
 881      [use GLPK simplex solver])], [], [with_glpk=])
 882 CVC4_CHECK_FOR_GLPK
 883 if test $have_libglpk -eq 1; then
 884   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_GLPK"
 885 fi
 886 AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
 887 AC_SUBST([GLPK_LDFLAGS])
 888 AC_SUBST([GLPK_LIBS])
 889
 890 # Build with libabc (defined in config/abc.m4)
 891 AC_ARG_WITH([abc],
 892   [AS_HELP_STRING([--with-abc],
 893      [use the ABC AIG library])], [], [with_abc=])
 894 CVC4_CHECK_FOR_ABC
 895 if test $have_libabc -eq 1; then
 896   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_ABC"
 897 fi
 898 AM_CONDITIONAL([CVC4_USE_ABC], [test $have_libabc -eq 1])
 899 AC_SUBST([ABC_LDFLAGS])
 900 AC_SUBST([ABC_LIBS])
 901
 902
 903 # Build with libcadical
 904 AC_ARG_WITH([cadical],
 905   [AS_HELP_STRING([--with-cadical],
 906      [use the CaDiCaL SAT solver])], [], [with_cadical=])
 907 CVC4_CHECK_FOR_CADICAL
 908 if test $have_libcadical -eq 1; then
 909   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CADICAL"
 910   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CADICAL_HOME/src"
 911 fi
 912 AM_CONDITIONAL([CVC4_USE_CADICAL], [test $have_libcadical -eq 1])
 913 AC_SUBST([CADICAL_LDFLAGS])
 914 AC_SUBST([CADICAL_LIBS])
 915
 916 # Build with libcryptominisat
 917 AC_ARG_WITH([cryptominisat],
 918   [AS_HELP_STRING([--with-cryptominisat],
 919      [use the CRYPTOMINISAT sat solver])], [], [with_cryptominisat=])
 920 CVC4_CHECK_FOR_CRYPTOMINISAT
 921 if test $have_libcryptominisat -eq 1; then
 922   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CRYPTOMINISAT"
 923   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/include"
 924 fi
 925 AM_CONDITIONAL([CVC4_USE_CRYPTOMINISAT], [test $have_libcryptominisat -eq 1])
 926 AC_SUBST([CRYPTOMINISAT_LDFLAGS])
 927 AC_SUBST([CRYPTOMINISAT_LIBS])
 928
 929 # Build with LFSC
 930 AC_ARG_WITH([lfsc],
 931   [AS_HELP_STRING([--with-lfsc],
 932      [use the LFSC proof checker])], [], [with_lfsc=])
 933 CVC4_CHECK_FOR_LFSC
 934 if test $have_liblfsc -eq 1; then
 935   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_LFSC"
 936 fi
 937 AM_CONDITIONAL([CVC4_USE_LFSC], [test $have_liblfsc -eq 1])
 938 AC_SUBST([LFSC_LDFLAGS])
 939 AC_SUBST([LFSC_LIBS])
 940
 941 # Build with symfpu
 942 AC_ARG_WITH([symfpu],
 943   [AS_HELP_STRING([--with-symfpu],
 944      [use symfpu for floating point solver])], [], [with_symfpu=])
 945 CVC4_CHECK_FOR_SYMFPU
 946 if test $have_symfpu_headers -eq 1; then
 947   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_SYMFPU"
 948   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$SYMFPU_HOME"
 949 fi
 950 AM_CONDITIONAL([CVC4_USE_SYMFPU], [test $have_symfpu_headers -eq 1])
 951 AC_SUBST([CVC4_USE_SYMFPU], [$have_symfpu_headers])
 952
 953 # Check to see if this version/architecture of GNU C++ explicitly
 954 # instantiates std::hash<uint64_t> or not.  Some do, some don't.
 955 # See src/util/hash.h.
 956 AC_MSG_CHECKING([whether std::hash<uint64_t> is already specialized])
 957 AC_LANG_PUSH([C++])
 958 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
 959 #include <cstdint>
 960 #include <functional>
 961 namespace std { template<> struct hash<uint64_t> {}; }])],
 962                   [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
 963                   [AC_MSG_RESULT([yes])])
 964 AC_LANG_POP([C++])
 965
 966 # Check whether "long" and "int64_t" are distinct types w.r.t. overloading.
 967 # Even if they have the same size, they can be distinct, and some platforms
 968 # can have problems with ambiguous function calls when auto-converting
 969 # int64_t to long, and others will complain if you overload a function
 970 # that takes an int64_t with one that takes a long (giving a redefinition
 971 # error).  So we have to keep both happy.  Probably the same underlying
 972 # issue as the hash specialization above, but let's check separately
 973 # for flexibility.
 974 AC_MSG_CHECKING([for the relationship between long and int64_t])
 975 AC_LANG_PUSH([C++])
 976 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
 977 #include <stdint.h>
 978 void foo(long) {}
 979 void foo(int64_t) {}])],
 980                   [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1],
 981                   [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0])
 982 AC_LANG_POP([C++])
 983 AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
 984
 985 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 986 AC_PROG_ANTLR
 987
 988 CVC4_CXX_OPTION([-Werror], [WERROR])
 989 CVC4_C_OPTION([-Werror], [C_WERROR])
 990 CVC4_CXX_OPTION([-Wno-deprecated], [WNO_DEPRECATED])
 991 CVC4_C_OPTION([-Wno-deprecated], [C_WNO_DEPRECATED])
 992 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
 993 CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE])
 994 CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
 995 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
 996 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
 997 CVC4_CXX_OPTION([-Wsuggest-override], [W_SUGGEST_OVERRIDE])
 998 CVC4_CXX_OPTION([-Wnon-virtual-dtor], [W_NON_VIRTUAL_DTOR])
 999 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
1000 AC_SUBST([WERROR])
1001 AC_SUBST([WNO_CONVERSION_NULL])
1002 AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
1003 AC_SUBST([WNO_PARENTHESES])
1004 AC_SUBST([WNO_UNINITIALIZED])
1005 AC_SUBST([WNO_UNUSED_VARIABLE])
1006 AC_SUBST([W_SUGGEST_OVERRIDE])
1007 AC_SUBST([W_NON_VIRTUAL_DTOR])
1008 AC_SUBST([FNO_STRICT_ALIASING])
1009
1010 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_SUGGEST_OVERRIDE}"
1011 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_NON_VIRTUAL_DTOR}"
1012
1013 # On Mac, we have to fix the visibility of standard library symbols.
1014 # Otherwise, exported template instantiations---even though explicitly
1015 # CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
1016 # Presumably, Apple is distributing a libstdc++ that is built *without*
1017 # --enable-libstdcxx-visibility (?)
1018 if test "$target_vendor" = apple; then
1019   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
1020 fi
1021
1022 # Doxygen configuration
1023 AC_ARG_ENABLE([internals-documentation],
1024   [AS_HELP_STRING([--enable-internals-documentation],
1025      [build Doxygen documentation for static and private member functions])])
1026 if test "$enable_internals_documentation" = yes; then
1027   DOXYGEN_EXTRACT_PRIVATE=YES
1028   DOXYGEN_EXTRACT_STATIC=YES
1029 else
1030   DOXYGEN_EXTRACT_PRIVATE=NO
1031   DOXYGEN_EXTRACT_STATIC=NO
1032 fi
1033 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
1034 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
1035
1036 DX_MAN_FEATURE(OFF)
1037 DX_PDF_FEATURE(OFF)
1038 DX_PS_FEATURE(OFF)
1039 DX_DOT_FEATURE(OFF)
1040 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
1041
1042 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])
1043 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
1044 AC_ARG_WITH([cxxtest-dir],
1045   [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
1046   [CXXTEST="$withval"])
1047
1048 TESTS_ENVIRONMENT=
1049 RUN_REGRESSION_ARGS=
1050 if test "$with_lfsc" = yes; then
1051   RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--with-lfsc"
1052 fi
1053 if test "$enable_proof" = yes; then
1054   RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--enable-proof"
1055 fi
1056 AC_SUBST([TESTS_ENVIRONMENT])
1057 AC_SUBST([RUN_REGRESSION_ARGS])
1058
1059 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
1060 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
1061 AC_ARG_VAR(TEST_LDFLAGS,  [LDFLAGS to use when testing (default=$LDFLAGS)])
1062
1063 CXXTESTGEN=
1064 if test "$enable_unit_testing" = "no"; then
1065   AC_MSG_NOTICE([unit tests disabled by user request.])
1066   CXXTEST=
1067 else
1068   # The latest version of cxxtest distributed from the git repository places
1069   # cxxtest under <cxxtest-root>/bin/cxxtest
1070   AC_PATH_PROGS(CXXTESTGEN,
1071                 cxxtestgen.pl cxxtestgen.py cxxtestgen,
1072                 [],
1073                 [$CXXTEST:$CXXTEST/bin:$PATH])
1074
1075   if test -n "$CXXTESTGEN"; then
1076     if "`basename $CXXTESTGEN`" = "cxxtestgen.pl"; then
1077       if test -z "$PERL"; then
1078         AC_CHECK_PROGS(PERL, perl, perl, [])
1079       else
1080         AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
1081       fi
1082
1083       if test -z "$PERL"; then
1084         AC_MSG_WARN([unit tests disabled, perl not found.])
1085         CXXTESTGEN=
1086         CXXTEST=
1087       fi
1088     fi
1089   else
1090     AC_MSG_NOTICE([unit tests disabled, could not find cxxtestgen.pl or cxxtestgen.py or cxxtestgen])
1091     CXXTEST=
1092   fi
1093
1094   # check if CxxTest headers exist and set include paths accordingly
1095   if test -n "$CXXTESTGEN"; then
1096     AC_MSG_CHECKING([for location of CxxTest headers])
1097     if test -n "$CXXTEST"; then
1098       if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
1099         AC_MSG_RESULT([$CXXTEST])
1100         TEST_CPPFLAGS="${TEST_CPPFLAGS} -I$CXXTEST"
1101         TEST_CXXFLAGS="${TEST_CXXFLAGS} -I$CXXTEST"
1102       else
1103         AC_MSG_RESULT([not found])
1104         AC_MSG_WARN([unit tests disabled, CxxTest headers not found at $CXXTEST.])
1105         CXXTESTGEN=
1106         CXXTEST=
1107       fi
1108     # TODO: use more generic way to find cxxtest/TestRunner.h in system headers
1109     elif test -e "/usr/include/cxxtest/TestRunner.h"; then
1110       CXXTEST=/usr/include
1111       AC_MSG_RESULT([$CXXTEST])
1112     else
1113       CXXTEST=`dirname "$CXXTESTGEN"`
1114       if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
1115         AC_MSG_RESULT([$CXXTEST])
1116         TEST_CPPFLAGS="${TEST_CPPFLAGS} -I$CXXTEST"
1117         TEST_CXXFLAGS="${TEST_CXXFLAGS} -I$CXXTEST"
1118       else
1119         AC_MSG_RESULT([not found])
1120         AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
1121         CXXTESTGEN=
1122         CXXTEST=
1123       fi
1124     fi
1125   fi
1126 fi
1127
1128 if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
1129   AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
1130 fi
1131
1132 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
1133
1134 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
1135
1136 # Python is now a required dependency for generating options code
1137 AM_PATH_PYTHON([2.7],, [
1138   AC_MSG_ERROR([Python not found.])
1139 ])
1140
1141 # Checks for libraries.
1142
1143 AC_SEARCH_LIBS([clock_gettime], [rt pthread],
1144                [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
1145                           [Defined to 1 if clock_gettime() is supported by the platform.])],
1146                [AC_LIBOBJ([clock_gettime])])
1147 AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1],
1148                                      [Defined to 1 if strtok_r() is supported by the platform.])])
1149 AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1],
1150                                 [Defined to 1 if ffs() is supported by the platform.])])
1151
1152 AC_LIBOBJ([strtok_r ffs])
1153
1154 # Check for sigaltstack (missing in emscripten and mingw)
1155 AC_CHECK_FUNC([sigaltstack], [AC_DEFINE([HAVE_SIGALTSTACK], [1],
1156                                         [Defined to 1 if sigaltstack() is supported by the platform.])])
1157
1158 # Check for antlr C++ runtime (defined in config/antlr.m4)
1159 AC_LIB_ANTLR
1160
1161 # Check for user preferences for language bindings to build, and for
1162 # build support.  The arg list is the default set if unspecified by
1163 # the user (the actual built set is the subset that appears to be
1164 # supported by the build host).
1165 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
1166
1167 # Checks for header files and their contents.
1168 AC_CHECK_HEADERS([getopt.h unistd.h ext/stdio_filebuf.h])
1169
1170 # Checks for typedefs, structures, and compiler characteristics.
1171 #AC_HEADER_STDBOOL
1172 # these are bad macros, they clash with system header <stdint.h> !!
1173 #AC_TYPE_UINT16_T
1174 #AC_TYPE_UINT32_T
1175 #AC_TYPE_UINT64_T
1176 #AC_TYPE_SIZE_T
1177
1178 # guard against double-inclusion of the autoheader
1179 AH_TOP([#ifndef __CVC4__CVC4AUTOCONFIG_H
1180 #define __CVC4__CVC4AUTOCONFIG_H])
1181 AH_BOTTOM([#endif /* __CVC4__CVC4AUTOCONFIG_H */])
1182
1183 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
1184
1185 # check with which standard strerror_r() complies
1186 AC_FUNC_STRERROR_R
1187
1188 # require boost library
1189 BOOST_REQUIRE()
1190
1191 # look for boost threading library
1192 AC_ARG_WITH([portfolio],
1193     AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)]))
1194 cvc4_save_LDFLAGS="$LDFLAGS"
1195 if test "$enable_static_binary" = yes; then
1196   LDFLAGS="-static $LDFLAGS"
1197 fi
1198 cvc4_has_threads=yes
1199 AC_ARG_ENABLE([thread-support],
1200     AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library]))
1201 if test "$enable_thread_support" = no; then
1202   cvc4_has_threads=no
1203   if test "$with_portfolio" = yes; then
1204     AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory])
1205   fi
1206 else
1207   BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
1208                      cvc4_has_threads=no])
1209 fi
1210 LDFLAGS="$cvc4_save_LDFLAGS"
1211 if test $cvc4_has_threads = no; then
1212   if test "$enable_thread_support" = yes; then
1213     AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?])
1214   fi
1215   if test "$with_portfolio" = yes; then
1216     AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
1217   fi
1218   with_portfolio=no
1219 fi
1220 if test "$with_portfolio" != yes; then
1221   with_portfolio=no
1222 fi
1223 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
1224 if test "$with_portfolio" = yes; then
1225   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
1226
1227   # see if Boost has thread attributes (should be any version >= 1.50.0)
1228   # non-fatal error if not, but we won't support --thread-stack option
1229   AC_MSG_CHECKING([whether Boost threads support thread attrs])
1230   AC_LANG_PUSH([C++])
1231   cvc4_save_CPPFLAGS="$CPPFLAGS"
1232   cvc4_save_LIBS="$LIBS"
1233   cvc4_save_LDFLAGS="$LDFLAGS"
1234   CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS"
1235   LIBS="$LIBS $BOOST_THREAD_LIBS"
1236   LDFLAGS="$LDFLAGS $BOOST_THREAD_LDFLAGS"
1237   AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <boost/thread.hpp>],
1238          [boost::thread::attributes attrs; attrs.set_stack_size(10 * 1024 * 1024);])],
1239     [cvc4_boost_has_thread_attr=1;
1240      AC_MSG_RESULT([yes])],
1241     [cvc4_boost_has_thread_attr=0;
1242      AC_MSG_RESULT([no])])
1243   CPPFLAGS="$cvc4_save_CPPFLAGS"
1244   LIBS="$cvc4_save_LIBS"
1245   LDFLAGS="$cvc4_save_LDFLAGS"
1246   AC_LANG_POP([C++])
1247 else
1248   cvc4_boost_has_thread_attr=0
1249 fi
1250 AC_DEFINE_UNQUOTED([BOOST_HAS_THREAD_ATTR], $cvc4_boost_has_thread_attr, [Define to 1 if Boost threading library has support for thread attributes])
1251
1252 # Check for libreadline (defined in config/readline.m4)
1253 AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
1254 # make the flags as close as possible to the final flags, because the Boost
1255 # flags can bring in a different, incompatible readline library than we'd
1256 # get otherwise (e.g. on Mac, where there are commonly two different readlines,
1257 # one in /usr and one in /opt/local)
1258 cvc4_rlcheck_save_CPPFLAGS="$CPPFLAGS"
1259 cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS"
1260 cvc4_rlcheck_save_CFLAGS="$CFLAGS"
1261 cvc4_rlcheck_save_LDFLAGS="$LDFLAGS"
1262 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1263 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED"
1264 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED -fexceptions"
1265 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1266 CVC4_CHECK_FOR_READLINE
1267 CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS"
1268 CXXFLAGS="$cvc4_rlcheck_save_CXXFLAGS"
1269 CFLAGS="$cvc4_rlcheck_save_CFLAGS"
1270 LDFLAGS="$cvc4_rlcheck_save_LDFLAGS"
1271 AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
1272 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])
1273 AC_SUBST([READLINE_LIBS])
1274
1275 # Whether to compile with google profiling tools
1276 cvc4_use_google_perftools=0
1277 AC_ARG_WITH(
1278     [google_perftools],
1279     AS_HELP_STRING(
1280         [--with-google-perftools],
1281         [use Google Performance Tools]
1282     ),
1283     [if test "$withval" != no; then
1284         cvc4_use_google_perftools=1
1285      fi
1286     ]
1287 )
1288 AC_MSG_CHECKING([whether to link in google perftools libraries])
1289 if test $cvc4_use_google_perftools = 1; then
1290   AC_MSG_RESULT([yes])
1291   AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
1292   AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
1293 else
1294   AC_MSG_RESULT([no (user didn't request it)])
1295 fi
1296
1297 # Java
1298 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
1299 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
1300 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
1301 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
1302 if test "$cvc4_build_java_bindings"; then
1303   dnl AM_PROG_GCJ
1304   if test -z "$JAVA"; then
1305     AC_CHECK_PROGS(JAVA, java, java, [])
1306   else
1307     AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
1308   fi
1309   if test -z "$JAVAC"; then
1310     AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
1311     if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
1312   else
1313     AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
1314   fi
1315   if test -z "$JAVAH"; then
1316     AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
1317   else
1318     AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
1319   fi
1320   if test -z "$JAR"; then
1321     AC_CHECK_PROGS(JAR, jar, jar, [])
1322   else
1323     AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
1324   fi
1325 fi
1326
1327 # on Mac OS X, Java doesn't like the .so module extension; it wants .dylib
1328 module=no eval CVC4_JAVA_MODULE_EXT="$shrext_cmds"
1329 if test -z "$CVC4_JAVA_MODULE_EXT"; then
1330   CVC4_JAVA_MODULE_EXT=.so
1331 fi
1332 AC_SUBST([CVC4_JAVA_MODULE_EXT])
1333
1334 # Prepare configure output
1335
1336 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
1337 if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
1338 if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
1339 AC_SUBST(BUILDING_SHARED)
1340 AC_SUBST(BUILDING_STATIC)
1341 AC_SUBST(STATIC_BINARY)
1342 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
1343 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
1344 AC_SUBST([COVERAGE_ON])
1345
1346 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
1347 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
1348
1349 AC_SUBST(CVC4_LIBRARY_VERSION)
1350 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
1351 AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
1352
1353 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
1354 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
1355 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
1356 AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
1357 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
1358
1359 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1360 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
1361 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
1362 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1363
1364 # visibility flag not supported for Windows builds
1365 # also increase default stack size for Windows binaries
1366 windows_build=no
1367 case $host_os in
1368   (*mingw*) FLAG_VISIBILITY_HIDDEN=
1369             cvc4_LDFLAGS=-Wl,--stack,134217728
1370             pcvc4_LDFLAGS=-Wl,--stack,134217728
1371             windows_build=yes
1372 esac
1373
1374 AM_CONDITIONAL([CVC4_WINDOWS_BUILD], [test "$windows_build" = "yes"])
1375
1376 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
1377 AC_SUBST(cvc4_LDFLAGS)
1378 AC_SUBST(pcvc4_LDFLAGS)
1379
1380 AM_CONDITIONAL(WHITE_AND_BLACK_TESTS, [test -z "$FLAG_VISIBILITY_HIDDEN"])
1381
1382 # remember the command line used for configure
1383 AC_SUBST(cvc4_config_cmdline)
1384
1385 # mk_include
1386 #
1387 # When automake scans Makefiles, it complains about non-standard make
1388 # features (including GNU extensions), and breaks GNU Make's
1389 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
1390 # constructs.  automake even follows "include" and messes with
1391 # included Makefiles.
1392 #
1393 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
1394 # have to hide some included Makefiles with GNU extensions.  We do
1395 # this by defining mk_include as an autoconf substitution and then
1396 # using "@mk_include@ other_makefile" in Makefile.am to include
1397 # makefiles with GNU extensions; this hides them from automake.
1398 mk_include=include
1399 AC_SUBST(mk_include)
1400 # Similar trickery for "if"
1401 mk_if=if
1402 AC_SUBST(mk_if)
1403 mk_empty=
1404 AC_SUBST(mk_empty)
1405
1406 # CVC4_FALSE
1407 #
1408 # This is used to _always_ comment out rules in automake makefiles, but
1409 # still trigger certain automake behavior; see test/unit/Makefile.am.
1410 AM_CONDITIONAL([CVC4_FALSE], [false])
1411
1412 # set up substitutions for src/util/{rational,integer}.h.in
1413 if test $cvc4_cln_or_gmp = cln; then
1414   CVC4_USE_CLN_IMP=1
1415   CVC4_USE_GMP_IMP=0
1416 else
1417   CVC4_USE_CLN_IMP=0
1418   CVC4_USE_GMP_IMP=1
1419 fi
1420 AC_SUBST(CVC4_USE_CLN_IMP)
1421 AC_SUBST(CVC4_USE_GMP_IMP)
1422
1423 # month/year for man pages
1424 MAN_DATE=`date '+%B %Y'`
1425 AC_SUBST(MAN_DATE)
1426
1427 AC_CONFIG_FILES([
1428   Makefile.builds
1429   Makefile
1430   proofs/signatures/Makefile]
1431   m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
1432 )
1433
1434 if test $cvc4_has_threads = yes; then
1435   support_multithreaded='with boost threading library'
1436   AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1437   AC_SUBST([CVC4_HAS_THREADS], 1)
1438 else
1439   support_multithreaded='no'
1440   AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1441   AC_SUBST([CVC4_HAS_THREADS], 0)
1442 fi
1443
1444 # Final information to the user
1445 gpl=no
1446 licensewarn=
1447
1448 if test "$custom_build_profile" = yes; then
1449   with_build="$with_build (customized)"
1450 fi
1451
1452 support_unit_tests='cxxtest not found; unit tests not supported'
1453 if test -n "$CXXTEST"; then
1454   support_unit_tests='unit testing infrastructure enabled in build directory'
1455 elif test "$enable_unit_testing" = no; then
1456   support_unit_tests='unit testing disabled by user'
1457 fi
1458
1459 if test "$enable_optimized" = yes; then
1460   optimized="yes, at level $OPTLEVEL"
1461 else
1462   optimized="no"
1463 fi
1464
1465 if test $have_libglpk -eq 1; then
1466   gpl=yes
1467   gpllibs="${gpllibs} glpk"
1468 fi
1469
1470 if test $have_libreadline -eq 1; then
1471   gpl=yes
1472   gpllibs="${gpllibs} readline"
1473 fi
1474
1475 if test $cvc4_cln_or_gmp = cln; then
1476   mplibrary='cln (GPL)'
1477   gpl=yes
1478   gpllibs="${gpllibs} cln"
1479   if test $with_portfolio = yes; then
1480     AC_ERROR([Bad configuration detected: cannot build portfolio with CLN.
1481 Please specify only one of --with-portfolio and --with-cln.])
1482   fi
1483 else
1484   mplibrary='gmp'
1485 fi
1486
1487 if test "$gpl" = yes; then
1488   if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1; then
1489     AC_ERROR([Bad configuration detected: BSD-licensed code only, but also requested GPLed libraries:$gpllibs
1490 To permit GPL'ed dependences, use the configure flag --enable-gpl])
1491   fi
1492
1493   licensewarn="${licensewarn}"'****************************************************************************
1494 Please note that CVC4 will be built against the following GPLed libraries:
1495  '"$gpllibs"'
1496 As these libraries are covered under the GPLv3, so is this build of CVC4.
1497 CVC4 is also available to you under the terms of the (modified) BSD license.
1498 If you prefer to license CVC4 under those terms, please configure with the
1499 option "--bsd", which will disable all optional GPLed library dependences.
1500 ****************************************************************************
1501
1502 '
1503   license="GPLv3 (due to optional libraries; see below)"
1504 else
1505   licensewarn="${licensewarn}Please note that this configuration is NOT built against any GPL'ed
1506 libraries, so it is covered by the (modified) BSD license.  This is,
1507 however, not the best-performing configuration of CVC4.  To build
1508 against GPL'ed libraries which improve CVC4's performance, re-configure
1509 with '--best --enable-gpl'.
1510
1511 "
1512   license="modified BSD"
1513 fi
1514
1515 if test "$gpl" = yes; then isgpl=1; else isgpl=0; fi
1516 AC_DEFINE_UNQUOTED(CVC4_GPL_DEPS, $isgpl, [Whether CVC4 is built with the (optional) GPLed library dependences.])
1517
1518 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1519 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1520   CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1521 fi
1522
1523 bindings_to_be_built=none
1524 if test -n "$CVC4_LANGUAGE_BINDINGS"; then
1525   bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS"
1526 fi
1527
1528 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/floatingpoint.h])
1529 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1530 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1531
1532 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
1533 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1534 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3])
1535 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
1536 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
1537 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1538
1539 AC_OUTPUT
1540
1541 cat <<EOF
1542
1543 CVC4 $VERSION
1544
1545 Build profile: $with_build
1546 Build ID     : $build_type
1547 Optimized    : $optimized
1548 Debug symbols: $enable_debug_symbols
1549 Proofs       : $enable_proof
1550 Statistics   : $enable_statistics
1551 Replay       : $enable_replay
1552 Assertions   : $enable_assertions
1553 Tracing      : $enable_tracing
1554 Dumping      : $enable_dumping
1555 Muzzle       : $enable_muzzle
1556
1557 Unit tests   : $support_unit_tests
1558 gcov support : $enable_coverage
1559 gprof support: $enable_profiling
1560
1561 Static libs  : $enable_static
1562 Shared libs  : $enable_shared
1563 Static binary: $enable_static_binary
1564 Bindings     : $bindings_to_be_built
1565
1566 Multithreaded: $support_multithreaded
1567 Portfolio    : $with_portfolio
1568
1569 ABC          : $with_abc
1570 CaDiCaL      : $with_cadical
1571 Cryptominisat: $with_cryptominisat
1572 GLPK         : $with_glpk
1573 LFSC         : $with_lfsc
1574 MP library   : $mplibrary
1575 Readline     : $with_readline
1576 SymFPU       : $with_symfpu
1577
1578 CPPFLAGS     : $CPPFLAGS
1579 CXXFLAGS     : $CXXFLAGS
1580 CFLAGS       : $CFLAGS
1581 LIBS         : $LIBS
1582 LDFLAGS      : $LDFLAGS
1583
1584 libcvc4 version        : $CVC4_LIBRARY_VERSION
1585 libcvc4parser version  : $CVC4_PARSER_LIBRARY_VERSION
1586 libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
1587
1588 Install into : $prefix
1589
1590 CVC4 license : $license
1591
1592 ${licensewarn}Now just type make, followed by make check or make install, as you like.
1593
1594 EOF
1595
1596 if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then
1597   AC_MSG_WARN([])
1598   AC_MSG_WARN([You are electing to build unsupported language binding(s):])
1599   AC_MSG_WARN([    $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
1600   AC_MSG_WARN([Please be aware that these bindings may not compile, or])
1601   AC_MSG_WARN([work, and the interface to CVC4 via these bindings may])
1602   AC_MSG_WARN([change drastically in upcoming releases of CVC4.])
1603   AC_MSG_WARN([])
1604 fi
1605
1606 if test -n "$CVC4_INTEGRITY_WARNING"; then
1607   AC_MSG_WARN([])
1608   AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
1609   AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])
1610   AC_MSG_WARN([])
1611 fi