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