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