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