configure.ac

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