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