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