configure.ac

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