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