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