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