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 "$CVC4_BSD_LICENSED_CODE_ONLY" = 1 -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      save_LIBS="$LIBS"
 303      LIBS="$CLN_LIBS $LIBS"
 304      AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])], [
 305        cvc4_use_cln=1
 306      ], [
 307        if test $cvc4_use_cln = 1; then
 308          # fail
 309          AC_MSG_ERROR([CLN installation missing, too old, or not functional for this architecture])
 310        else
 311          # fall back to GMP
 312          AC_MSG_NOTICE([CLN installation missing, too old, or not functional for this architecture, will use gmp instead])
 313          cvc4_use_cln=0
 314          cvc4_use_gmp=1
 315        fi
 316      ])
 317      LIBS="$save_LIBS"
 318      AC_LANG_POP([C++])
 319     ],
 320     [if test $cvc4_use_cln = 1; then
 321        # fail
 322        AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
 323      else
 324        # fall back to GMP
 325        AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
 326        cvc4_use_cln=0
 327        cvc4_use_gmp=1
 328      fi
 329     ]
 330   )
 331 fi
 332 if test $cvc4_use_cln = 0; then
 333   # try GMPXX, fail if not found
 334   AC_CHECK_LIB(gmpxx, __gmpz_init, , [AC_MSG_ERROR([GNU MP C++ library (libgmpxx) not found, see http://gmplib.org/])])
 335   cvc4_cln_or_gmp=gmp
 336 else
 337   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
 338   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
 339   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
 340   LIBS="$CLN_LIBS${LIBS:+ $LIBS}"
 341   cvc4_cln_or_gmp=cln
 342 fi
 343
 344 if test $cvc4_cln_or_gmp = cln; then
 345   AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.])
 346 else
 347   AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.])
 348 fi
 349 AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln])
 350 AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
 351
 352 # construct the build string
 353 AC_MSG_CHECKING([for appropriate build string])
 354 if test -z "$ac_confdir"; then
 355   ac_confdir="$srcdir"
 356 fi
 357 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
 358 AC_MSG_RESULT($build_type)
 359
 360 # Require building in target and build-specific build directory:
 361 #
 362 # If the configure script is invoked from the top-level source
 363 # directory, it creates a suitable build directory (based on the build
 364 # architecture and build profile from $build_type), changes into it,
 365 # and reinvokes itself.  CVC4_CONFIGURE_IN_BUILDS is an envariable
 366 # that breaks any possibility of infinite recursion in this process.
 367 AC_MSG_CHECKING([what dir to configure])
 368 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
 369   AC_MSG_RESULT([this one (in builds/)])
 370 elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
 371   AC_MSG_RESULT([builds/$target/$build_type])
 372   $as_echo
 373   if test -z "$ac_srcdir"; then
 374     mkbuilddir=./config/mkbuilddir
 375   else
 376     mkbuilddir=$ac_srcdir/config/mkbuilddir
 377   fi
 378   $as_echo "$mkbuilddir $target $build_type"
 379   source $mkbuilddir "$target" "$build_type"
 380   $as_echo "cd builds/$target/$build_type"
 381   cd "builds/$target/$build_type"
 382   CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
 383   echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
 384   "$SHELL" "`pwd`/../../../configure" "${config_cmdline[[@]]}"
 385   exitval=$?
 386   cd ../../..
 387   if test $exitval -eq 0; then
 388     cat >config.reconfig <<EOF
 389 [#!/bin/bash
 390 # Generated by configure, `date`
 391 # This script is part of CVC4.
 392
 393 cd "\`dirname \\"\$0\\"\`"
 394
 395 if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi
 396
 397 current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`)
 398 arch=\${current[0]}
 399 build=\${current[1]}
 400
 401 echo "reconfiguring in builds/\$arch/\$build..."
 402 cd "builds/\$arch/\$build"
 403 echo ./config.status "\$@"
 404 ./config.status "\$@"]
 405 EOF
 406     chmod +x config.reconfig
 407   fi
 408   ln -sf "$target/$build_type/config.log" "builds/config.log"
 409   exit $exitval
 410 else
 411   AC_MSG_RESULT([this one (user-specified)])
 412 fi
 413
 414 as_me=configure
 415
 416 # Unpack standard build types. Any particular options can be overriden with
 417 # --enable/disable-X options
 418 case "$with_build" in
 419   production) # highly optimized, no assertions, no tracing, dumping
 420     CVC4CPPFLAGS=
 421     CVC4CXXFLAGS=
 422     CVC4CFLAGS=
 423     CVC4LDFLAGS=
 424     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
 425     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=3                       ; fi
 426     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; 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=no                 ; fi
 430     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
 431     if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
 432     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; 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   debug) # unoptimized, debug symbols, assertions, tracing, dumping
 437     CVC4CPPFLAGS='-DCVC4_DEBUG'
 438     CVC4CXXFLAGS='-fno-inline'
 439     CVC4CFLAGS='-fno-inline'
 440     CVC4LDFLAGS=
 441     FLAG_VISIBILITY_HIDDEN=
 442     if test -z "${enable_optimized+set}"    ; then enable_optimized=no              ; fi
 443     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
 444     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
 445     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
 446     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
 447     if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
 448     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
 449     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
 450     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 451     ;;
 452   default) # moderately optimized, assertions, tracing, dumping
 453     CVC4CPPFLAGS=
 454     CVC4CXXFLAGS=
 455     CVC4CFLAGS=
 456     CVC4LDFLAGS=
 457     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
 458     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=2                       ; fi
 459     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 460     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
 461     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
 462     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
 463     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
 464     if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
 465     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
 466     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
 467     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 468     ;;
 469   competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
 470     CVC4CPPFLAGS='-DCVC4_COMPETITION_MODE'
 471     CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
 472     CVC4CFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
 473     CVC4LDFLAGS=
 474     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
 475     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=9                       ; fi
 476     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 477     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no          ; fi
 478     if test -z "${enable_statistics+set}"   ; then enable_statistics=no             ; fi
 479     if test -z "${enable_replay+set}"       ; then enable_replay=no                 ; fi
 480     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
 481     if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
 482     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
 483     if test -z "${enable_dumping+set}"      ; then enable_dumping=no                ; fi
 484     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=yes                ; fi
 485     if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi
 486     if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi
 487     if test -z "${enable_static_binary+set}"; then enable_static_binary=yes         ; fi
 488     ;;
 489   *)
 490     AC_MSG_FAILURE([unknown build profile: $with_build])
 491     ;;
 492 esac
 493 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
 494
 495 AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION],  [test "$with_build" = production])
 496 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG],       [test "$with_build" = debug])
 497 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEFAULT],     [test "$with_build" = default])
 498 AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
 499
 500 # permit a static binary
 501 AC_MSG_CHECKING([whether to build a static binary])
 502 AC_ARG_ENABLE([static-binary],
 503      [AS_HELP_STRING([--enable-static-binary],
 504                      [build a fully statically-linked binary [default=no]])])
 505 if test -z "${enable_static_binary+set}"; then
 506   enable_static_binary=no
 507 fi
 508 AC_MSG_RESULT([$enable_static_binary])
 509 if test "$enable_static_binary" = yes; then
 510   if test "$target_vendor" = apple; then
 511     if test -z "$MAC_STATIC_BINARY_MANUAL_OVERRIDE"; then
 512       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)]])
 513     else
 514       AC_MSG_WARN([MAC_STATIC_BINARY_MANUAL_OVERRIDE was set!])
 515       AC_MSG_WARN([Will make a static binary during this build.  Note that it may fail!])
 516     fi
 517   fi
 518   if test "$enable_static" != yes; then
 519     enable_static=yes
 520     AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
 521   fi
 522 fi
 523
 524 AC_MSG_CHECKING([whether to support proofs in libcvc4])
 525
 526 AC_ARG_ENABLE([proof],
 527   [AS_HELP_STRING([--enable-proof],
 528      [support proof generation])])
 529 if test -z "${enable_proof+set}"; then
 530   enable_proof=no
 531 fi
 532 AC_MSG_RESULT([$enable_proof])
 533
 534 if test "$enable_proof" = yes; then
 535   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
 536 fi
 537 AM_CONDITIONAL([CVC4_PROOF], [test "$enable_proof" = yes])
 538
 539 AC_MSG_CHECKING([whether to optimize libcvc4])
 540
 541 AC_ARG_ENABLE([optimized],
 542   [AS_HELP_STRING([--enable-optimized],
 543      [optimize the build])])
 544
 545 if test -z "${enable_optimized+set}"; then
 546   enable_optimized=no
 547 fi
 548
 549 AC_MSG_RESULT([$enable_optimized])
 550
 551 if test "$enable_optimized" = yes; then
 552   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
 553   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
 554 else
 555   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O0"
 556   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O0"
 557 fi
 558
 559 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
 560
 561 AC_ARG_ENABLE([debug-symbols],
 562   [AS_HELP_STRING([--disable-debug-symbols],
 563      [do not include debug symbols in libcvc4])])
 564
 565 if test -z "${enable_debug_symbols+set}"; then
 566   enable_debug_symbols=yes
 567 fi
 568
 569 AC_MSG_RESULT([$enable_debug_symbols])
 570
 571 if test "$enable_debug_symbols" = yes; then
 572   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3"
 573   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
 574 fi
 575
 576 AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])
 577
 578 AC_ARG_ENABLE([statistics],
 579   [AS_HELP_STRING([--disable-statistics],
 580      [do not include statistics in libcvc4])])
 581
 582 if test -z "${enable_statistics+set}"; then
 583   enable_statistics=yes
 584 fi
 585
 586 AC_MSG_RESULT([$enable_statistics])
 587
 588 if test "$enable_statistics" = yes; then
 589   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
 590 fi
 591
 592 AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
 593
 594 AC_ARG_ENABLE([replay],
 595   [AS_HELP_STRING([--disable-replay],
 596      [turn off the replay feature in libcvc4])])
 597
 598 if test -z "${enable_replay+set}"; then
 599   enable_replay=yes
 600 fi
 601
 602 AC_MSG_RESULT([$enable_replay])
 603
 604 if test "$enable_replay" = yes; then
 605   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
 606 fi
 607
 608 AC_MSG_CHECKING([whether to include assertions in build])
 609
 610 AC_ARG_ENABLE([assertions],
 611   [AS_HELP_STRING([--disable-assertions],
 612      [turn off assertions in build])])
 613
 614 if test -z "${enable_assertions+set}"; then
 615   enable_assertions=yes
 616 fi
 617
 618 AC_MSG_RESULT([$enable_assertions])
 619
 620 if test "$enable_assertions" = yes; then
 621   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS"
 622 else
 623   # turn off regular C assert() also
 624   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG"
 625 fi
 626
 627 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
 628 AC_ARG_ENABLE([tracing],
 629   [AS_HELP_STRING([--disable-tracing],
 630      [remove all tracing code from CVC4])])
 631
 632 if test -z "${enable_tracing+set}"; then
 633   enable_tracing=yes
 634 fi
 635
 636 AC_MSG_RESULT([$enable_tracing])
 637
 638 if test "$enable_tracing" = yes; then
 639   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
 640 fi
 641
 642 AC_MSG_CHECKING([whether to do a dump-capable build of CVC4])
 643 AC_ARG_ENABLE([dumping],
 644   [AS_HELP_STRING([--disable-dumping],
 645      [remove all dumping code from CVC4])])
 646
 647 if test -z "${enable_dumping+set}"; then
 648   enable_dumping=yes
 649 fi
 650
 651 AC_MSG_RESULT([$enable_dumping])
 652
 653 if test "$enable_dumping" = yes; then
 654   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING"
 655 fi
 656
 657 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
 658 AC_ARG_ENABLE([muzzle],
 659   [AS_HELP_STRING([--enable-muzzle],
 660      [completely silence CVC4; remove ALL non-result output from build])])
 661
 662 if test -z "${enable_muzzle+set}"; then
 663   enable_muzzle=no
 664 fi
 665
 666 AC_MSG_RESULT([$enable_muzzle])
 667
 668 if test "$enable_muzzle" = yes; then
 669   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE"
 670 fi
 671
 672 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
 673 AC_ARG_ENABLE([coverage],
 674   [AS_HELP_STRING([--enable-coverage],
 675      [build with support for gcov coverage testing])])
 676
 677 if test -z "${enable_coverage+set}"; then
 678   enable_coverage=no
 679 fi
 680
 681 AC_MSG_RESULT([$enable_coverage])
 682
 683 if test "$enable_coverage" = yes; then
 684   # For coverage testing, we prefer:
 685   #     --enable-static --disable-shared --disable-static-binary
 686   # If the user didn't specify these, we force them here.  If the
 687   # user specified them in opposite phase, give warnings that they
 688   # shouldn't do that, or bomb out.
 689   if test "$user_specified_enable_or_disable_shared" != yes; then
 690     enable_shared=no
 691     AC_MSG_WARN([turning off shared library building due to --enable-coverage])
 692   elif test "$enable_shared" = yes; then
 693     AC_MSG_WARN([])
 694     AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared])
 695     AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.])
 696     AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.])
 697     AC_MSG_WARN([])
 698   fi
 699   if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then
 700     AC_MSG_WARN([])
 701     AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary])
 702     AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.])
 703     AC_MSG_WARN([])
 704   fi
 705   if test "$user_specified_enable_or_disable_static" != yes; then
 706     enable_static=yes
 707     AC_MSG_WARN([turning on static library building due to --enable-coverage])
 708   elif test "$enable_static" != yes; then
 709     AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.])
 710   fi
 711
 712   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE"
 713   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage"
 714   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage"
 715   CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage"
 716 fi
 717
 718 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
 719
 720 AC_ARG_ENABLE([profiling],
 721   [AS_HELP_STRING([--enable-profiling],
 722      [build with support for gprof profiling])])
 723
 724 if test -z "${enable_profiling+set}"; then
 725   enable_profiling=no
 726 fi
 727
 728 AC_MSG_RESULT([$enable_profiling])
 729
 730 if test "$enable_profiling" = yes; then
 731   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING"
 732   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg"
 733   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg"
 734   CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
 735 fi
 736
 737 # Check for libglpk (defined in config/glpk.m4)
 738 AC_ARG_WITH([glpk],
 739   [AS_HELP_STRING([--with-glpk],
 740      [use GLPK simplex solver])], [], [with_glpk=])
 741 CVC4_CHECK_FOR_GLPK
 742 if test $have_libglpk -eq 1; then
 743   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_GLPK"
 744 fi
 745 AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
 746 AC_SUBST([GLPK_LIBS])
 747
 748 # Check to see if this version/architecture of GNU C++ explicitly
 749 # instantiates __gnu_cxx::hash<uint64_t> or not.  Some do, some don't.
 750 # See src/util/hash.h.
 751 AC_MSG_CHECKING([whether __gnu_cxx::hash<uint64_t> is already specialized])
 752 AC_LANG_PUSH([C++])
 753 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
 754 #include <stdint.h>
 755 #include <ext/hash_map>
 756 namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])],
 757                   [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
 758                   [AC_MSG_RESULT([yes])])
 759 AC_LANG_POP([C++])
 760
 761 # Check whether "long" and "int64_t" are distinct types w.r.t. overloading.
 762 # Even if they have the same size, they can be distinct, and some platforms
 763 # can have problems with ambiguous function calls when auto-converting
 764 # int64_t to long, and others will complain if you overload a function
 765 # that takes an int64_t with one that takes a long (giving a redefinition
 766 # error).  So we have to keep both happy.  Probably the same underlying
 767 # issue as the hash specialization above, but let's check separately
 768 # for flexibility.
 769 AC_MSG_CHECKING([for the relationship between long and int64_t])
 770 AC_LANG_PUSH([C++])
 771 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
 772 #include <stdint.h>
 773 void foo(long) {}
 774 void foo(int64_t) {}])],
 775                   [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1],
 776                   [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0])
 777 AC_LANG_POP([C++])
 778 AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
 779
 780 AC_MSG_CHECKING([for the pb_ds namespace])
 781 AC_LANG_PUSH([C++])
 782 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
 783 #include <ext/pb_ds/priority_queue.hpp>
 784 typedef pb_ds::priority_queue<void, void, void> pq;])],
 785   [CVC4_PB_DS_NAMESPACE=pb_ds],
 786   [AC_COMPILE_IFELSE([AC_LANG_SOURCE([
 787     #include <ext/pb_ds/priority_queue.hpp>
 788     typedef __gnu_pbds::priority_queue<void, void, void> pq;])],
 789       [CVC4_PB_DS_NAMESPACE=__gnu_pbds],
 790       [AC_MSG_ERROR([cannot find required priority_queue in either __gnu_pbds or pb_ds namespace.
 791
 792 If you're using a non-GCC compiler (such as clang), you may need to explicitly
 793 use the GNU standard C++ library by passing:
 794     CXXFLAGS='-stdlib=libstdc++' CPPFLAGS='-stdlib=libstdc++'
 795 as arguments to this configure script.
 796 This is the case on Mac OS Mavericks, for example.])])])
 797 AC_LANG_POP([C++])
 798 AC_MSG_RESULT([$CVC4_PB_DS_NAMESPACE])
 799 AC_DEFINE_UNQUOTED(CVC4_PB_DS_NAMESPACE, ${CVC4_PB_DS_NAMESPACE}, [The namespace for pb_ds data structures.])
 800
 801 # for information: http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
 802 AC_MSG_CHECKING([whether pb_ds has bug 36612])
 803 AC_LANG_PUSH([C++])
 804 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
 805 #define __throw_container_error inline __throw_container_error
 806 #define __throw_insert_error inline __throw_insert_error
 807 #define __throw_join_error inline __throw_join_error
 808 #define __throw_resize_error inline __throw_resize_error
 809 #include <ext/pb_ds/exception.hpp>
 810 ])],
 811   [CVC4_GCC_HAS_PB_DS_BUG=1; bugverb=is],
 812   [CVC4_GCC_HAS_PB_DS_BUG=0; bugverb="is not"])
 813 AC_LANG_POP([C++])
 814 AC_MSG_RESULT([bug $bugverb present])
 815 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])
 816
 817 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 818 AC_PROG_ANTLR
 819
 820 CVC4_CXX_OPTION([-Werror], [WERROR])
 821 CVC4_C_OPTION([-Werror], [C_WERROR])
 822 CVC4_CXX_OPTION([-Wno-deprecated], [WNO_DEPRECATED])
 823 CVC4_C_OPTION([-Wno-deprecated], [C_WNO_DEPRECATED])
 824 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
 825 CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE])
 826 CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
 827 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
 828 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
 829 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
 830 AC_SUBST([WERROR])
 831 AC_SUBST([WNO_CONVERSION_NULL])
 832 AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
 833 AC_SUBST([WNO_PARENTHESES])
 834 AC_SUBST([WNO_UNINITIALIZED])
 835 AC_SUBST([WNO_UNUSED_VARIABLE])
 836 AC_SUBST([FNO_STRICT_ALIASING])
 837
 838 # On Mac, we have to fix the visibility of standard library symbols.
 839 # Otherwise, exported template instantiations---even though explicitly
 840 # CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
 841 # Presumably, Apple is distributing a libstdc++ that is built *without*
 842 # --enable-libstdcxx-visibility (?)
 843 if test "$target_vendor" = apple; then
 844   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
 845 fi
 846
 847 # Tell top-level Makefile to include $(top_srcdir)/personal.mk
 848 AC_ARG_ENABLE([personal-make-rules],
 849   [AS_HELP_STRING([--enable-personal-make-rules],
 850      [include top-level personal.mk (if it exists)])])
 851 if test "$enable_personal_make_rules" = yes; then
 852   # This allows us to include a personal.mk makefile from every
 853   # generated makefile.  Named zz_* in order to make sure this
 854   # comes last, so it gets other definitions (in particular top_srcdir).
 855   zz_cvc4_use_personal_make_rules='yes
 856
 857 include $(top_srcdir)/personal.mk
 858 $(top_srcdir)/personal.mk:; @touch "$@"'
 859   AC_SUBST([zz_cvc4_use_personal_make_rules])
 860 fi
 861
 862 # Doxygen configuration
 863 AC_ARG_ENABLE([internals-documentation],
 864   [AS_HELP_STRING([--enable-internals-documentation],
 865      [build Doxygen documentation for static and private member functions])])
 866 if test "$enable_internals_documentation" = yes; then
 867   DOXYGEN_EXTRACT_PRIVATE=YES
 868   DOXYGEN_EXTRACT_STATIC=YES
 869 else
 870   DOXYGEN_EXTRACT_PRIVATE=NO
 871   DOXYGEN_EXTRACT_STATIC=NO
 872 fi
 873 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
 874 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
 875
 876 DX_MAN_FEATURE(OFF)
 877 DX_PDF_FEATURE(OFF)
 878 DX_PS_FEATURE(OFF)
 879 DX_DOT_FEATURE(OFF)
 880 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
 881
 882 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])
 883 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
 884
 885 AC_SUBST([CXXTEST])
 886
 887 AC_ARG_WITH([cxxtest-dir],
 888   [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
 889   [CXXTEST="$withval"])
 890
 891 # In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
 892 # relative path) and having switched the configure directory (see above),
 893 # search with respect to the top source dir, not the build dir
 894 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then
 895   case "$CXXTEST" in
 896     /*) ;;
 897     *)  CXXTEST="$srcdir/$CXXTEST" ;;
 898   esac
 899 fi
 900
 901 TESTS_ENVIRONMENT=
 902 RUN_REGRESSION_ARGS=
 903 if test "$enable_proof" = yes; then
 904   RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof"
 905 fi
 906 AC_SUBST([TESTS_ENVIRONMENT])
 907 AC_SUBST([RUN_REGRESSION_ARGS])
 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   proofs/signatures/Makefile]
1281   m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
1282 )
1283
1284 if test $cvc4_has_threads = yes; then
1285   support_multithreaded='with boost threading library'
1286   AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1287   AC_SUBST([CVC4_HAS_THREADS], 1)
1288 else
1289   support_multithreaded='no'
1290   AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1291   AC_SUBST([CVC4_HAS_THREADS], 0)
1292 fi
1293
1294 AM_CONDITIONAL([CVC4_NEEDS_REPLACEMENT_FUNCTIONS], [test -n "$LIBOBJS"])
1295
1296 # Final information to the user
1297 gpl=no
1298 licensewarn=
1299
1300 if test "$custom_build_profile" = yes; then
1301   with_build="$with_build (customized)"
1302 fi
1303
1304 support_unit_tests='cxxtest not found; unit tests not supported'
1305 if test -n "$CXXTEST"; then
1306   support_unit_tests='unit testing infrastructure enabled in build directory'
1307 elif test "$enable_unit_testing" = no; then
1308   support_unit_tests='unit testing disabled by user'
1309 fi
1310
1311 if test "$enable_optimized" = yes; then
1312   optimized="yes, at level $OPTLEVEL"
1313 else
1314   optimized="no"
1315 fi
1316
1317 if test $have_libglpk -eq 1; then
1318   gpl=yes
1319   gpllibs="${gpllibs} glpk"
1320 fi
1321
1322 if test $have_libreadline -eq 1; then
1323   gpl=yes
1324   gpllibs="${gpllibs} readline"
1325 fi
1326
1327 if test $cvc4_cln_or_gmp = cln; then
1328   mplibrary='cln (GPL)'
1329   gpl=yes
1330   gpllibs="${gpllibs} cln"
1331   if test $with_portfolio = yes; then
1332     AC_ERROR([Bad configuration detected: cannot build portfolio with CLN.
1333 Please specify only one of --with-portfolio and --with-cln.])
1334   fi
1335 else
1336   mplibrary='gmp'
1337 fi
1338
1339 if test "$gpl" = yes; then
1340   if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1; then
1341     AC_ERROR([Bad configuration detected: BSD-licensed code only, but also requested GPLed libraries:$gpllibs
1342 To permit GPL'ed dependences, use the configure flag --enable-gpl])
1343   fi
1344
1345   licensewarn="${licensewarn}"'****************************************************************************
1346 Please note that CVC4 will be built against the following GPLed libraries:
1347  '"$gpllibs"'
1348 As these libraries are covered under the GPLv3, so is this build of CVC4.
1349 CVC4 is also available to you under the terms of the (modified) BSD license.
1350 If you prefer to license CVC4 under those terms, please configure with the
1351 option "--bsd", which will disable all optional GPLed library dependences.
1352 ****************************************************************************
1353
1354 '
1355   license="GPLv3 (due to optional libraries; see below)"
1356 else
1357   licensewarn="${licensewarn}Please note that this configuration is NOT built against any GPL'ed
1358 libraries, so it is covered by the (modified) BSD license.  This is,
1359 however, not the best-performing configuration of CVC4.  To build
1360 against GPL'ed libraries which improve CVC4's performance, re-configure
1361 with '--best --enable-gpl'.
1362
1363 "
1364   license="modified BSD"
1365 fi
1366
1367 if test "$gpl" = yes; then isgpl=1; else isgpl=0; fi
1368 AC_DEFINE_UNQUOTED(CVC4_GPL_DEPS, $isgpl, [Whether CVC4 is built with the (optional) GPLed library dependences.])
1369
1370 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
1371 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1372 if test "$CVC4_BUILD_LIBCOMPAT" = no; then
1373   CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="N/A"
1374 fi
1375 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1376   CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1377 fi
1378
1379 bindings_to_be_built=none
1380 if test -n "$CVC4_LANGUAGE_BINDINGS"; then
1381   bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS"
1382   if test -z "$SWIG"; then
1383     bindings_to_be_built="$bindings_to_be_built (for CVC3 compatibility layer only; SWIG not found)"
1384   fi
1385 fi
1386
1387 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1388 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1389 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
1390
1391 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
1392 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1393 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
1394 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
1395 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
1396 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1397 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
1398
1399 AC_OUTPUT
1400
1401 cat <<EOF
1402
1403 CVC4 $VERSION
1404
1405 Build profile: $with_build
1406 Build ID     : $build_type
1407 Optimized    : $optimized
1408 Debug symbols: $enable_debug_symbols
1409 Proofs       : $enable_proof
1410 Statistics   : $enable_statistics
1411 Replay       : $enable_replay
1412 Assertions   : $enable_assertions
1413 Tracing      : $enable_tracing
1414 Dumping      : $enable_dumping
1415 Muzzle       : $enable_muzzle
1416
1417 Unit tests   : $support_unit_tests
1418 gcov support : $enable_coverage
1419 gprof support: $enable_profiling
1420
1421 Static libs  : $enable_static
1422 Shared libs  : $enable_shared
1423 Static binary: $enable_static_binary
1424 Compat lib   : $CVC4_BUILD_LIBCOMPAT
1425 Bindings     : $bindings_to_be_built
1426
1427 Multithreaded: $support_multithreaded
1428 TLS support  : $CVC4_TLS_explanation
1429 Portfolio    : $with_portfolio
1430
1431 MP library   : $mplibrary
1432 GLPK         : $with_glpk
1433 Readline     : $with_readline
1434
1435 CPPFLAGS     : $CPPFLAGS
1436 CXXFLAGS     : $CXXFLAGS
1437 CFLAGS       : $CFLAGS
1438 LIBS         : $LIBS
1439 LDFLAGS      : $LDFLAGS
1440
1441 libcvc4 version        : $CVC4_LIBRARY_VERSION
1442 libcvc4parser version  : $CVC4_PARSER_LIBRARY_VERSION
1443 libcvc4compat version  : $CVC4_COMPAT_LIBRARY_VERSION_or_nobuild
1444 libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
1445
1446 Install into : $prefix
1447
1448 CVC4 license : $license
1449
1450 ${licensewarn}Now just type make, followed by make check or make install, as you like.
1451
1452 EOF
1453
1454 if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then
1455   AC_MSG_WARN([])
1456   AC_MSG_WARN([You are electing to build unsupported language binding(s): $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
1457   AC_MSG_WARN([Please be aware that these bindings may not compile, or work, and the interface to CVC4 via])
1458   AC_MSG_WARN([these bindings may change drastically in upcoming releases of CVC4.])
1459   AC_MSG_WARN([])
1460 fi
1461
1462 if test -n "$CVC4_INTEGRITY_WARNING"; then
1463   AC_MSG_WARN([])
1464   AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
1465   AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])
1466   AC_MSG_WARN([])
1467 fi