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