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