# -*- Autoconf -*-
# Process this file with autoconf to produce a configure script.
+m4_define(_CVC4_MAJOR, 0 ) dnl version (major)
+m4_define(_CVC4_MINOR, 0 ) dnl version (minor)
+m4_define(_CVC4_RELEASE, 0 ) dnl version (alpha)
+m4_define(_CVC4_RELEASE_STRING, [prerelease]) dnl version string
+
dnl Preprocess CL args. Defined in config/cvc4.m4
CVC4_AC_INIT
-AC_PREREQ(2.64)
-AC_INIT
-AC_CONFIG_SRCDIR([src/include/cvc4_config.h])
+AC_PREREQ(2.61)
+AC_INIT([cvc4], _CVC4_RELEASE_STRING)
+AC_CONFIG_SRCDIR([src/include/cvc4_public.h])
AC_CONFIG_AUX_DIR([config])
AC_CONFIG_MACRO_DIR([config])
-CVC4_RELEASE=prerelease
+m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])])
+
+CVC4_MAJOR=_CVC4_MAJOR
+CVC4_MINOR=_CVC4_MINOR
+CVC4_RELEASE=_CVC4_RELEASE
+CVC4_RELEASE_STRING=_CVC4_RELEASE_STRING
# Libtool version numbers for libraries
# Version numbers are in the form current:revision:age
#
# For more information, see:
# http://www.gnu.org/software/libtool/manual/libtool.html#Versioning
-# For guidance on when to change the version number, refer to the
+# For guidance on when to change the version number, refer to the
# developer's guide.
-CVC4_LIBRARY_VERSION=0:0:0
-CVC4_PARSER_LIBRARY_VERSION=0:0:0
+CVC4_LIBRARY_VERSION=$CVC4_MAJOR:$CVC4_MINOR:$CVC4_RELEASE
+CVC4_PARSER_LIBRARY_VERSION=$CVC4_MAJOR:$CVC4_MINOR:$CVC4_RELEASE
# Using the AC_CANONICAL_* macros destroy the command line you get
# from $@, which we want later for determining the build profile. So
AC_MSG_CHECKING([what dir to configure])
if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
AC_MSG_RESULT([this one (in builds/)])
-elif test -e src/include/cvc4_config.h; then
+elif test -e src/include/cvc4_public.h; then
AC_MSG_RESULT([builds/$target/$build_type])
echo
if test -z "$ac_srcdir"; then
# Unpack standard build types. Any particular options can be overriden with
# --enable/disable-X options
+if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
+# our defaults for CXXFLAGS are better than autoconf's
+if test -z "${CXXFLAGS+set}"; then CXXFLAGS=; fi
case "$with_build" in
production) # highly optimized, no assertions, no tracing
CVC4CPPFLAGS=
- CVC4CXXFLAGS=-O3
+ CVC4CXXFLAGS=
+ CVC4CFLAGS=
CVC4LDFLAGS=
- if test -z "${enable_assertions+set}"; then enable_assertions=no ; fi
- if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
- if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
+ if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi
+ if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
+ if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
+ if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
+ if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
+ if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
;;
- debug) # Unoptimized, debug symbols, assertions, tracing
+ debug) # unoptimized, debug symbols, assertions, tracing
CVC4CPPFLAGS=-DCVC4_DEBUG
- CVC4CXXFLAGS='-O0 -fno-inline -ggdb3'
+ CVC4CXXFLAGS='-fno-inline'
+ CVC4CFLAGS='-fno-inline'
CVC4LDFLAGS=
- if test -z "${enable_assertions+set}"; then enable_assertions=yes ; fi
- if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
- if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
+ if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi
+ if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
+ if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
+ if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
+ if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
;;
default) # moderately optimized, assertions, tracing
CVC4CPPFLAGS=
- CVC4CXXFLAGS=-O2
+ CVC4CXXFLAGS=
+ CVC4CFLAGS=
CVC4LDFLAGS=
- if test -z "${enable_assertions+set}"; then enable_assertions=yes ; fi
- if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
- if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
+ if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=2 ; fi
+ if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
+ if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
+ if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
+ if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
+ if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
;;
competition) # maximally optimized, no assertions, no tracing, muzzled
CVC4CPPFLAGS=
- CVC4CXXFLAGS='-O9 -funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
+ CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
+ CVC4CFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
CVC4LDFLAGS=
- if test -z "${enable_assertions+set}"; then enable_assertions=no ; fi
- if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
- if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi
+ if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=9 ; fi
+ if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
+ if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
+ if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
+ if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
+ if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi
;;
*)
AC_MSG_FAILURE([unknown build profile: $with_build])
;;
esac
+# permit a static binary
+AC_MSG_CHECKING([whether to build a static binary])
+AC_ARG_ENABLE([static-binary],
+ [AS_HELP_STRING([--enable-static-binary],
+ [build a statically-linked binary [default=no]])])
+if test -z "${enable_static_binary+set}"; then
+ enable_static_binary=no
+fi
+AC_MSG_RESULT([$enable_static_binary])
+if test "${enable_static_binary}" = yes -a "${enable_static}" != yes; then
+ enable_static=yes
+ AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
+fi
+
AC_MSG_CHECKING([whether to optimize libcvc4])
AC_ARG_ENABLE([optimized],
- [AS_HELP_STRING([--enable-optimized],
+ [AS_HELP_STRING([--enable-optimized],
[optimize the build])])
if test -z "${enable_optimized+set}"; then
AC_MSG_RESULT([$enable_optimized])
if test "$enable_optimized" = yes; then
- CVC4CXXFLAGS="$CVC4CXXFLAGS -O3"
+ CVC4CXXFLAGS="$CVC4CXXFLAGS -O$OPTLEVEL"
+ CVC4CFLAGS="$CVC4CFLAGS -O$OPTLEVEL"
+else
+ CVC4CXXFLAGS="$CVC4CXXFLAGS -O0"
+ CVC4CFLAGS="$CVC4CFLAGS -O0"
fi
AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
-AC_ARG_ENABLE([debug-symbols],
- [AS_HELP_STRING([--disable-debug-symbols],
+AC_ARG_ENABLE([debug-symbols],
+ [AS_HELP_STRING([--disable-debug-symbols],
[do not include debug symbols in libcvc4])])
if test -z "${enable_debug_symbols+set}"; then
if test "$enable_debug_symbols" = yes; then
CVC4CXXFLAGS="$CVC4CXXFLAGS -ggdb3"
+ CVC4CFLAGS="$CVC4CFLAGS -ggdb3"
fi
AC_MSG_CHECKING([whether to include assertions in build])
-AC_ARG_ENABLE([assertions],
- [AS_HELP_STRING([--disable-assertions],
+AC_ARG_ENABLE([assertions],
+ [AS_HELP_STRING([--disable-assertions],
[turn off assertions in build])])
if test -z "${enable_assertions+set}"; then
fi
AC_MSG_CHECKING([whether to do a traceable build of CVC4])
-AC_ARG_ENABLE([tracing],
- [AS_HELP_STRING([--disable-tracing],
+AC_ARG_ENABLE([tracing],
+ [AS_HELP_STRING([--disable-tracing],
[remove all tracing code from CVC4])])
if test -z "${enable_tracing+set}"; then
fi
AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
-AC_ARG_ENABLE([muzzle],
- [AS_HELP_STRING([--enable-muzzle],
+AC_ARG_ENABLE([muzzle],
+ [AS_HELP_STRING([--enable-muzzle],
[completely silence CVC4; remove ALL non-result output from build])])
if test -z "${enable_muzzle+set}"; then
fi
AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
-AC_ARG_ENABLE([coverage],
- [AS_HELP_STRING([--enable-coverage],
+AC_ARG_ENABLE([coverage],
+ [AS_HELP_STRING([--enable-coverage],
[build with support for gcov coverage testing])])
if test -z "${enable_coverage+set}"; then
AC_MSG_RESULT([$enable_coverage])
if test "$enable_coverage" = yes; then
+dnl TODO: Is there someway to detect if enable_shared is set by default,
+dnl so that we can automatically disable shared and enable static?
+ if test "$enable_shared" = yes; then
+ AC_MSG_ERROR([Gcov requires static libraries. Use --disable-shared.])
+ fi
+
+ CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_COVERAGE"
CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage"
+ CVC4CFLAGS="$CVC4CFLAGS --coverage"
CVC4LDFLAGS="$CVC4LDFLAGS --coverage"
fi
AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
-AC_ARG_ENABLE([profiling],
- [AS_HELP_STRING([--enable-profiling],
+AC_ARG_ENABLE([profiling],
+ [AS_HELP_STRING([--enable-profiling],
[build with support for gprof profiling])])
if test -z "${enable_profiling+set}"; then
AC_MSG_RESULT([$enable_profiling])
if test "$enable_profiling" = yes; then
+ CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_PROFILING"
CVC4CXXFLAGS="$CVC4CXXFLAGS -pg"
+ CVC4CFLAGS="$CVC4CFLAGS -pg"
CVC4LDFLAGS="$CVC4LDFLAGS -pg"
fi
-AM_INIT_AUTOMAKE(cvc4, $CVC4_RELEASE)
-AC_CONFIG_HEADERS([config.h])
+AM_INIT_AUTOMAKE([1.11 no-define])
+AC_CONFIG_HEADERS([cvc4autoconfig.h])
# Initialize libtool's configuration options.
_LT_SET_OPTION([LT_INIT],[win32-dll])
# Check for ANTLR runantlr script (defined in config/antlr.m4)
AC_PROG_ANTLR
-AC_CHECK_PROG(DOXYGEN, doxygen, doxygen, [])
+DX_PDF_FEATURE(OFF)
+DX_PS_FEATURE(OFF)
+DX_DOT_FEATURE(OFF)
+DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc)
-if test -z "$DOXYGEN"; then
- AC_MSG_WARN([documentation targets require doxygen. Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.])
-fi
-
-AC_ARG_VAR(DOXYGEN, [location of doxygen binary])
+AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
AC_SUBST([CXXTEST])
-AC_ARG_WITH([cxxtest-dir],
+AC_ARG_WITH([cxxtest-dir],
[AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
[CXXTEST="$withval"])
+# In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
+# relative path) and having switched the configure directory (see above),
+# search with respect to the top source dir, not the build dir
+if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
+ case "$CXXTEST" in
+ /*) ;;
+ *) CXXTEST="$srcdir/$CXXTEST" ;;
+ esac
+fi
+
CXXTESTGEN=
AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
if test -z "$CXXTESTGEN"; then
AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
-AC_ARG_VAR(TEST_CPPFLAGS, [CXXFLAGS to use when testing (default=$CPPFLAGS)])
+AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)])
fi
# Checks for libraries.
-AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])])
+AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
+AC_CHECK_LIB(gmpxx, __gmpz_init, , [AC_MSG_ERROR([GNU MP C++ library (libgmpxx) not found, see http://gmplib.org/])])
+
# Check for antlr C++ runtime (defined in config/antlr.m4)
AC_LIB_ANTLR
AC_CHECK_HEADERS([getopt.h unistd.h])
# Checks for typedefs, structures, and compiler characteristics.
-AC_HEADER_STDBOOL
+#AC_HEADER_STDBOOL
AC_TYPE_UINT16_T
AC_TYPE_UINT32_T
AC_TYPE_UINT64_T
if test "$enable_static" = yes; then BUILDING_STATIC=1; fi
AC_SUBST(BUILDING_SHARED)
AC_SUBST(BUILDING_STATIC)
+AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
AC_SUBST(CVC4_LIBRARY_VERSION)
AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
+AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
+AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
+AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
+AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
+
CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS"
-CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS"
+CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
+CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated"
LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
# mk_include
mk_include=include
AC_SUBST(mk_include)
+# CVC4_FALSE
+#
+# This is used to _always_ comment out rules in automake makefiles, but
+# still trigger certain automake behavior; see test/unit/Makefile.am.
+AM_CONDITIONAL([CVC4_FALSE], [false])
+
AC_CONFIG_FILES([
Makefile.builds
- Makefile
- contrib/Makefile
- doc/Makefile
- src/Makefile
- src/expr/Makefile
- src/smt/Makefile
- src/main/Makefile
- src/prop/minisat/Makefile
- src/prop/Makefile
- src/util/Makefile
- src/context/Makefile
- src/parser/Makefile
- src/parser/cvc/Makefile
- src/parser/smt/Makefile
- src/theory/Makefile
- src/theory/bool/Makefile
- src/theory/uf/Makefile
- src/theory/arith/Makefile
- test/Makefile
- test/regress/Makefile
- test/system/Makefile
- test/unit/Makefile
-])
+ Makefile]
+ m4_esyscmd([find contrib/ src/ test/ -name Makefile.am | sort | sed 's,\.am$,,'])
+)
AC_OUTPUT
support_unit_tests='unit testing infrastructure enabled in build directory'
fi
+if test "$enable_optimized" = yes; then
+ optimized="yes, at level $OPTLEVEL"
+else
+ optimized="no"
+fi
+
cat <<EOF
CVC4 $VERSION
Build profile: $with_build
Build ID : $build_type
-Optimized : $enable_optimized
+Optimized : $optimized
Debug symbols: $enable_debug_symbols
Assertions : $enable_assertions
Tracing : $enable_tracing
gprof support: $enable_profiling
unit tests : $support_unit_tests
+static libs : $enable_static
+shared libs : $enable_shared
+static binary: $enable_static_binary
+
CPPFLAGS : $CPPFLAGS
CXXFLAGS : $CXXFLAGS
+CFLAGS : $CFLAGS
LDFLAGS : $LDFLAGS
libcvc4 version : $CVC4_LIBRARY_VERSION
projects / cvc5.git / blobdiff