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([-Wno-conversion-null], [WNO_CONVERSION_NULL])
 747 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
 748 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
 749 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
 750 AC_SUBST([WNO_CONVERSION_NULL])
 751 AC_SUBST([WNO_UNINITIALIZED])
 752 AC_SUBST([WNO_UNUSED_VARIABLE])
 753 AC_SUBST([FNO_STRICT_ALIASING])
 754
 755 # On Mac, we have to fix the visibility of standard library symbols.
 756 # Otherwise, exported template instantiations---even though explicitly
 757 # CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
 758 # Presumably, Apple is distributing a libstdc++ that is built *without*
 759 # --enable-libstdcxx-visibility (?)
 760 if test "$target_vendor" = apple; then
 761   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
 762 fi
 763
 764 # Doxygen configuration
 765 AC_ARG_ENABLE([internals-documentation],
 766   [AS_HELP_STRING([--enable-internals-documentation],
 767      [build Doxygen documentation for static and private member functions])])
 768 if test "$enable_internals_documentation" = yes; then
 769   DOXYGEN_EXTRACT_PRIVATE=YES
 770   DOXYGEN_EXTRACT_STATIC=YES
 771 else
 772   DOXYGEN_EXTRACT_PRIVATE=NO
 773   DOXYGEN_EXTRACT_STATIC=NO
 774 fi
 775 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
 776 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
 777
 778 DX_MAN_FEATURE(OFF)
 779 DX_PDF_FEATURE(OFF)
 780 DX_PS_FEATURE(OFF)
 781 DX_DOT_FEATURE(OFF)
 782 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
 783
 784 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])
 785 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
 786
 787 AC_SUBST([CXXTEST])
 788
 789 AC_ARG_WITH([cxxtest-dir],
 790   [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
 791   [CXXTEST="$withval"])
 792
 793 # In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
 794 # relative path) and having switched the configure directory (see above),
 795 # search with respect to the top source dir, not the build dir
 796 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then
 797   case "$CXXTEST" in
 798     /*) ;;
 799     *)  CXXTEST="$srcdir/$CXXTEST" ;;
 800   esac
 801 fi
 802
 803 AC_ARG_VAR(LFSC, [path to LFSC proof checker])
 804 AC_ARG_VAR(LFSCARGS, [arguments to pass to LFSC proof checker])
 805 if test -z "$LFSC"; then
 806   AC_CHECK_PROGS(LFSC, lfsc, [], [])
 807 else
 808   AC_CHECK_PROG(LFSC, "$LFSC", [], [])
 809 fi
 810 AM_CONDITIONAL([PROOF_REGRESSIONS], [test -n "$LFSC" -a "$enable_proof" = yes])
 811 if test -n "$LFSC" -a "$enable_proof" = yes; then
 812   TESTS_ENVIRONMENT="${TESTS_ENVIRONMENT:+$TESTS_ENVIRONMENT }LFSC=\"$LFSC $LFSCARGS\""
 813   RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof"
 814 fi
 815 AC_SUBST([TESTS_ENVIRONMENT])
 816 AC_SUBST([RUN_REGRESSION_ARGS])
 817 if test -z "$LFSC"; then
 818   support_proof_tests='no, lfsc proof checker unavailable'
 819 elif test "$enable_proof" = yes; then
 820   support_proof_tests='yes, proof regression tests enabled'
 821 else
 822   support_proof_tests='no, proof generation disabled for this build'
 823 fi
 824 AC_SUBST([LFSC])
 825 AC_SUBST([LFSCARGS])
 826
 827 CXXTESTGEN=
 828 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
 829 if test -z "$CXXTESTGEN"; then
 830   AC_PATH_PROG(CXXTESTGEN, cxxtestgen.py, [], [$CXXTEST:$PATH])
 831 fi
 832 if test -z "$CXXTESTGEN"; then
 833   AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST:$PATH])
 834 fi
 835 if test "$enable_unit_testing" = "no"; then
 836   AC_MSG_NOTICE([unit tests disabled by user request.])
 837   CXXTESTGEN=
 838   CXXTEST=
 839 elif test -z "$CXXTESTGEN"; then
 840   AC_MSG_NOTICE([unit tests disabled, could not find cxxtestgen.pl or cxxtestgen.py or cxxtestgen])
 841 elif test -z "$CXXTEST"; then
 842   CXXTEST=`dirname "$CXXTESTGEN"`
 843   AC_MSG_CHECKING([for location of CxxTest headers])
 844   if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
 845     AC_MSG_RESULT([$CXXTEST])
 846   else
 847     if test -e "/usr/include/cxxtest/TestRunner.h"; then
 848       AC_MSG_RESULT([/usr/include])
 849     else
 850       AC_MSG_RESULT([not found])
 851       AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
 852       CXXTESTGEN=
 853       CXXTEST=
 854     fi
 855   fi
 856 fi
 857
 858 if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
 859   AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
 860 fi
 861
 862 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
 863
 864 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
 865 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
 866 AC_ARG_VAR(TEST_LDFLAGS,  [LDFLAGS to use when testing (default=$LDFLAGS)])
 867
 868 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
 869
 870 if test -n "$CXXTEST"; then
 871   if test -z "$PERL"; then
 872     AC_CHECK_PROGS(PERL, perl, perl, [])
 873   else
 874     AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
 875   fi
 876
 877   if test -z "$PERL"; then
 878     AC_MSG_WARN([unit tests disabled, perl not found.])
 879     CXXTESTGEN=
 880     CXXTEST=
 881   fi
 882 fi
 883
 884 AC_ARG_VAR(PYTHON, [PYTHON interpreter (used for building legacy Java library interface)])
 885
 886 if test -z "$PYTHON"; then
 887   AC_CHECK_PROGS(PYTHON, python, python, [])
 888 else
 889   AC_CHECK_PROG(PYTHON, "$PYTHON", "$PYTHON", [])
 890 fi
 891
 892 if test -z "$PYTHON"; then
 893   AC_MSG_WARN([python not found, cannot build libcvc4compat_java (the legacy Java interface).])
 894   CXXTESTGEN=
 895   CXXTEST=
 896 fi
 897
 898 # Checks for libraries.
 899
 900 AC_SEARCH_LIBS([clock_gettime], [rt],
 901                [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
 902                           [Defined to 1 if clock_gettime() is supported by the platform.])],
 903                [AC_LIBOBJ([clock_gettime])])
 904 AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1],
 905                                      [Defined to 1 if strtok_r() is supported by the platform.])],
 906                           [AC_LIBOBJ([strtok_r])])
 907 AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1],
 908                                 [Defined to 1 if ffs() is supported by the platform.])],
 909                      [AC_LIBOBJ([ffs])])
 910
 911 # Check for the presence of CUDD libraries
 912 CVC4_CHECK_CUDD
 913
 914 # Check for antlr C++ runtime (defined in config/antlr.m4)
 915 AC_LIB_ANTLR
 916
 917 # Check for user preferences for language bindings to build, and for
 918 # build support.  The arg list is the default set if unspecified by
 919 # the user (the actual built set is the subset that appears to be
 920 # supported by the build host).
 921 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
 922
 923 # Checks for header files and their contents.
 924 AC_CHECK_HEADERS([getopt.h unistd.h])
 925
 926 # Checks for typedefs, structures, and compiler characteristics.
 927 #AC_HEADER_STDBOOL
 928 # these are bad macros, they clash with system header <stdint.h> !!
 929 #AC_TYPE_UINT16_T
 930 #AC_TYPE_UINT32_T
 931 #AC_TYPE_UINT64_T
 932 #AC_TYPE_SIZE_T
 933
 934 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
 935
 936 # check with which standard strerror_r() complies
 937 AC_FUNC_STRERROR_R
 938
 939 # require boost library
 940 BOOST_REQUIRE()
 941
 942 # look for boost threading library
 943 AC_ARG_WITH([portfolio],
 944     AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)]))
 945 cvc4_save_LDFLAGS="$LDFLAGS"
 946 if test "$enable_static_binary" = yes; then
 947   LDFLAGS="-static $LDFLAGS"
 948 fi
 949 cvc4_has_threads=yes
 950 AC_ARG_ENABLE([thread-support],
 951     AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library]))
 952 if test "$enable_thread_support" = no; then
 953   cvc4_has_threads=no
 954   if test "$with_portfolio" = yes; then
 955     AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory])
 956   fi
 957 else
 958   BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
 959                      cvc4_has_threads=no])
 960 fi
 961 LDFLAGS="$cvc4_save_LDFLAGS"
 962 if test $cvc4_has_threads = no; then
 963   if test "$enable_thread_support" = yes; then
 964     AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?])
 965   fi
 966   if test "$with_portfolio" = yes; then
 967     AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
 968   fi
 969   with_portfolio=no
 970 fi
 971 if test "$with_portfolio" != yes; then
 972   with_portfolio=no
 973 fi
 974 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
 975 if test "$with_portfolio" = yes; then
 976   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
 977 fi
 978
 979 # Check for libreadline (defined in config/readline.m4)
 980 AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
 981 # make the flags as close as possible to the final flags, because the Boost
 982 # flags can bring in a different, incompatible readline library than we'd
 983 # get otherwise (e.g. on Mac, where there are commonly two different readlines,
 984 # one in /usr and one in /opt/local)
 985 cvc4_rlcheck_save_CPPFLAGS="$CPPFLAGS"
 986 cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS"
 987 cvc4_rlcheck_save_CFLAGS="$CFLAGS"
 988 cvc4_rlcheck_save_LDFLAGS="$LDFLAGS"
 989 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
 990 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
 991 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
 992 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 993 CVC4_CHECK_FOR_READLINE
 994 CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS"
 995 CXXFLAGS="$cvc4_rlcheck_save_CXXFLAGS"
 996 CFLAGS="$cvc4_rlcheck_save_CFLAGS"
 997 LDFLAGS="$cvc4_rlcheck_save_LDFLAGS"
 998 AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
 999 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])
1000 AC_SUBST([READLINE_LIBS])
1001
1002 # Whether to build compatibility library
1003 CVC4_BUILD_LIBCOMPAT=yes
1004 AC_ARG_WITH([compat],
1005     AS_HELP_STRING([--with-compat], [build compatibility library (CVC3 API layer)]),
1006     [if test "$withval" = no; then CVC4_BUILD_LIBCOMPAT=no; fi])
1007 AC_MSG_CHECKING([whether to build compatibility library (CVC3 API layer)])
1008 if test "$CVC4_BUILD_LIBCOMPAT" = yes; then
1009   AC_MSG_RESULT([yes])
1010 else
1011   AC_MSG_RESULT([no, disabled by user])
1012 fi
1013 AC_SUBST(CVC4_BUILD_LIBCOMPAT)
1014 AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
1015
1016 # Check for availability of TLS support (e.g. __thread storage class)
1017 AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
1018 AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
1019 if test $cvc4_has_threads = no; then
1020   # We disable TLS entirely by simply telling the build system that
1021   # the empty string is the __thread keyword.
1022   AC_MSG_RESULT([multithreading disabled])
1023   CVC4_TLS_SUPPORTED=1
1024   CVC4_TLS=
1025   CVC4_TLS_explanation='disabled (no multithreading support)'
1026 else
1027   if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then
1028     AC_MSG_RESULT([yes])
1029     AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=])
1030   else
1031     AC_MSG_RESULT([no])
1032     CVC4_TLS=
1033   fi
1034   if test -n "$CVC4_TLS"; then
1035     CVC4_TLS_SUPPORTED=1
1036     CVC4_TLS_explanation="$CVC4_TLS"
1037   else
1038     CVC4_TLS_explanation='pthread_getspecific()'
1039     CVC4_TLS_SUPPORTED=0
1040   fi
1041 fi
1042 AC_SUBST([CVC4_TLS])
1043 AC_SUBST([CVC4_TLS_SUPPORTED])
1044
1045 # Whether to compile with google profiling tools
1046 cvc4_use_google_perftools=0
1047 AC_ARG_WITH(
1048     [google_perftools],
1049     AS_HELP_STRING(
1050         [--with-google-perftools],
1051         [use Google Performance Tools]
1052     ),
1053     [if test "$withval" != no; then
1054         cvc4_use_google_perftools=1
1055      fi
1056     ]
1057 )
1058 AC_MSG_CHECKING([whether to link in google perftools libraries])
1059 if test $cvc4_use_google_perftools = 1; then
1060   AC_MSG_RESULT([yes])
1061   AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
1062   AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
1063 else
1064   AC_MSG_RESULT([no (user didn't request it)])
1065 fi
1066
1067 # Java
1068 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
1069 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
1070 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
1071 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
1072 if test "$cvc4_build_java_bindings"; then
1073   dnl AM_PROG_GCJ
1074   if test -z "$JAVA"; then
1075     AC_CHECK_PROGS(JAVA, java, java, [])
1076   else
1077     AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
1078   fi
1079   if test -z "$JAVAC"; then
1080     AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
1081     if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
1082   else
1083     AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
1084   fi
1085   if test -z "$JAVAH"; then
1086     AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
1087   else
1088     AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
1089   fi
1090   if test -z "$JAR"; then
1091     AC_CHECK_PROGS(JAR, jar, jar, [])
1092   else
1093     AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
1094   fi
1095 fi
1096
1097 # Prepare configure output
1098
1099 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
1100 if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
1101 if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
1102 AC_SUBST(BUILDING_SHARED)
1103 AC_SUBST(BUILDING_STATIC)
1104 AC_SUBST(STATIC_BINARY)
1105 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
1106 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
1107
1108 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
1109 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
1110
1111 AC_SUBST(CVC4_LIBRARY_VERSION)
1112 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
1113 AC_SUBST(CVC4_COMPAT_LIBRARY_VERSION)
1114 AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
1115
1116 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
1117 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
1118 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
1119 AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
1120 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
1121
1122 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1123 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
1124 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
1125 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1126
1127 # visibility flag not supported for Windows builds
1128 # also increase default stack size for Windows binaries
1129 case $host_os in
1130   (*mingw*) FLAG_VISIBILITY_HIDDEN=
1131             cvc4_LDFLAGS=-Wl,--stack,134217728
1132             pcvc4_LDFLAGS=-Wl,--stack,134217728
1133 esac
1134
1135 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
1136 AC_SUBST(cvc4_LDFLAGS)
1137 AC_SUBST(pcvc4_LDFLAGS)
1138
1139 # mk_include
1140 #
1141 # When automake scans Makefiles, it complains about non-standard make
1142 # features (including GNU extensions), and breaks GNU Make's
1143 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
1144 # constructs.  automake even follows "include" and messes with
1145 # included Makefiles.
1146 #
1147 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
1148 # have to hide some included Makefiles with GNU extensions.  We do
1149 # this by defining mk_include as an autoconf substitution and then
1150 # using "@mk_include@ other_makefile" in Makefile.am to include
1151 # makefiles with GNU extensions; this hides them from automake.
1152 mk_include=include
1153 AC_SUBST(mk_include)
1154
1155 # CVC4_FALSE
1156 #
1157 # This is used to _always_ comment out rules in automake makefiles, but
1158 # still trigger certain automake behavior; see test/unit/Makefile.am.
1159 AM_CONDITIONAL([CVC4_FALSE], [false])
1160
1161 # set up substitutions for src/util/{rational,integer}.h.in
1162 if test $cvc4_cln_or_gmp = cln; then
1163   CVC4_USE_CLN_IMP=1
1164   CVC4_USE_GMP_IMP=0
1165 else
1166   CVC4_USE_CLN_IMP=0
1167   CVC4_USE_GMP_IMP=1
1168 fi
1169 AC_SUBST(CVC4_USE_CLN_IMP)
1170 AC_SUBST(CVC4_USE_GMP_IMP)
1171
1172 # month/year for man pages
1173 MAN_DATE=`date '+%B %Y'`
1174 AC_SUBST(MAN_DATE)
1175
1176 AC_CONFIG_FILES([
1177   Makefile.builds
1178   Makefile]
1179   m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^src/prop/cryptominisat/' | sort | sed 's,\.am$,,'])
1180 )
1181
1182 if test $cvc4_has_threads = yes; then
1183   support_multithreaded='with boost threading library'
1184   AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1185   AC_SUBST([CVC4_HAS_THREADS], 1)
1186 else
1187   support_multithreaded='no'
1188   AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1189   AC_SUBST([CVC4_HAS_THREADS], 0)
1190 fi
1191
1192 AM_CONDITIONAL([CVC4_NEEDS_REPLACEMENT_FUNCTIONS], [test -n "$LIBOBJS"])
1193
1194 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1195 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1196 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
1197
1198 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
1199 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1200 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
1201 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
1202 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
1203 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1204 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
1205
1206 # AC_CONFIG_SUBDIRS([src/prop/cryptominisat])
1207
1208 AC_OUTPUT
1209
1210 # Final information to the user
1211 licensewarn=
1212
1213 if test "$custom_build_profile" = yes; then
1214   if test "$with_build" = default; then
1215     with_build=custom
1216   else
1217     with_build="$with_build (customized)"
1218   fi
1219 fi
1220
1221 support_unit_tests='cxxtest not found; unit tests not supported'
1222 if test -n "$CXXTEST"; then
1223   support_unit_tests='unit testing infrastructure enabled in build directory'
1224 elif test "$enable_unit_testing" = no; then
1225   support_unit_tests='unit testing disabled by user'
1226 fi
1227
1228 if test "$enable_optimized" = yes; then
1229   optimized="yes, at level $OPTLEVEL"
1230 else
1231   optimized="no"
1232 fi
1233
1234 if test $cvc4_cln_or_gmp = cln; then
1235   mplibrary='cln (GPL)'
1236   licensewarn="${licensewarn}Please note that CVC4 will be built against the Class Library for
1237 Numbers (CLN).  This library is covered under the GPL, so use of this
1238 build of CVC4 will be more restrictive than CVC4's license would
1239 normally suggest.  For full details of CLN and its license, please visit
1240   http://www.ginac.de/CLN/
1241 To build CVC4 with GMP instead (which is covered under the more permissive
1242 LGPL), configure --without-cln.
1243
1244 "
1245   if test $with_portfolio = yes; then
1246     licensewarn="${licensewarn}
1247 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1248 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1249
1250 Note that CLN is UNSAFE FOR USE in parallel contexts!
1251 This build of CVC4 cannot be used safely as a portfolio solver.
1252 since the result of building with CLN will include numerous race
1253 conditions on the refcounts internal to CLN.
1254
1255 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1256 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1257
1258 "
1259   fi
1260 else
1261   mplibrary='gmp (LGPL)'
1262 fi
1263
1264 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
1265 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1266 if test "$CVC4_BUILD_LIBCOMPAT" = no; then
1267   CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="N/A"
1268 fi
1269 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1270   CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1271 fi
1272
1273 bindings_to_be_built=none
1274 if test -n "$CVC4_LANGUAGE_BINDINGS"; then
1275   bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS"
1276   if test -z "$SWIG"; then
1277     bindings_to_be_built="$bindings_to_be_built (for CVC3 compatibility layer only; SWIG not found)"
1278   fi
1279 fi
1280
1281 cat <<EOF
1282
1283 CVC4 $VERSION
1284
1285 Build profile: $with_build
1286 Build ID     : $build_type
1287 Optimized    : $optimized
1288 Debug symbols: $enable_debug_symbols
1289 Proof        : $enable_proof
1290 Statistics   : $enable_statistics
1291 Replay       : $enable_replay
1292 Assertions   : $enable_assertions
1293 Tracing      : $enable_tracing
1294 Dumping      : $enable_dumping
1295 Muzzle       : $enable_muzzle
1296
1297 Unit tests   : $support_unit_tests
1298 Proof tests  : $support_proof_tests
1299 gcov support : $enable_coverage
1300 gprof support: $enable_profiling
1301 CUDD         : $cvc4cudd
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