Mina Jeong <mjeong@cs.nyu.edu>, New York University
Dejan Jovanovic <dejan@cs.nyu.edu>, New York University
-The following individuals contributed code to CVC3 that may have been incorporated into CVC4:
+The following individuals contributed code to CVC3 that may have been
+incorporated into CVC4:
Clark Barrett, New York University
Christopher Conway <cconway@cs.nyu.edu>, New York University
George Hagen, University of Iowa
Dejan Jovanovic <dejan@cs.nyu.edu>, New York University
-The following individuals contributed code to CVC Lite that may have been incorporated in CVC4:
+The following individuals contributed code to CVC Lite that may have been
+incorporated in CVC4:
Clark Barrett, New York University
Sergey Berezin, Stanford University
Jim Zhuang, Stanford University
CVC4 contains MiniSAT code by Niklas Een and Niklas Sorensson
+
+The CVC4 parser incorporates some code from ANTLR3, by Jim Idle,
+Temporal Wave LLC.
+
+CVC4 contains the doxygen.m4 autoconf module by Oren Ben-Kiki.
+
+CVC4 maintainer versions contain the script autogen.sh, by the
+U.S. Army Research Laboratory
Institute for Mathematical Sciences, New York University.
All rights reserved.
-This is a prerelease version; distribution is restricted.
+CVC4 is open-source; distribution is under the terms of the modified BSD
+license. However, certain builds of CVC4 link against GPLed libraries,
+and therefore the use of these builds is restricted in non-open-source
+projects. See below for a discussion of CLN and how to ensure you have
+a build that doesn't link against GPLed libraries.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
''AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+Certain builds of CVC4 link against a GPLed library, CLN, the Class Library
+for Numbers, available here:
+
+ http://www.ginac.de/CLN/
+
+Please be advised that as this class library is covered under the GPL, the
+combined work, CVC4+CLN, is also covered under the GPL and cannot be used
+by proprietary software projects. For the full text of the GPL, please
+consult the CLN website. CVC4 does not require CLN; it can be built against
+libgmp, the GNU Multiple Precision Arithmetic Library, which is covered by
+the more permissive LGPL. To ensure that CLN is not used in the build,
+configure CVC4 with "--without-cln".
# coverage
# profiling
#
+# Also you can specify "cln" or "gmp". If "gmp", the build dir
+# contains the string "gmp". (cln is considered the default.)
+#
if [ $# -eq 0 ]; then
echo "usage: build-type profile [ overrides... ]" >&2
while [ $# -gt 0 ]; do
case "$1" in
+ cln) ;;
+ gmp) gmp=1 ;;
no*) eval `expr "$1" : 'no\(.*\)'`=0 ;;
*) eval $1=1 ;;
esac
done
build_type_suffix=
-for arg in staticbinary optimized debugsymbols statistics assertions tracing muzzle coverage profiling; do
+for arg in gmp staticbinary optimized debugsymbols statistics assertions tracing muzzle coverage profiling; do
if eval [ -n '"${'$arg'+set}"' ]; then
if eval [ '"${'$arg'}"' -eq 0 ]; then
build_type_suffix=$build_type_suffix-no$arg
if expr "$ac_option" : '.*-debugsymbols-\|.*-debugsymbols$' >/dev/null; then
eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-debug-symbols\""'
fi
+ for x in cln gmp; do
+ if expr "$ac_option" : '.*-no'$x'-\|.*-no'$x'$' >/dev/null; then
+ eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--without-$x\""'
+ fi
+ if expr "$ac_option" : '.*-'$x'-\|.*-'$x'$' >/dev/null; then
+ eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--with-$x\""'
+ fi
+ done
ac_option="--with-build=$ac_option_build"
esac
eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"$ac_option\""'
user_specified_enable_or_disable_static=${enable_static+yes}
user_specified_enable_or_disable_shared=${enable_shared+yes}
+if test -e src/include/cvc4_public.h; then
+ CVC4_CONFIGURE_AT_TOP_LEVEL=yes
+else
+ CVC4_CONFIGURE_AT_TOP_LEVEL=no
+fi
+
# turn off static lib building by default
AC_ENABLE_SHARED
AC_DISABLE_STATIC
if test -z "${with_build+set}" -o "$with_build" = default; then
with_build=default
fi
-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_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}"; then
+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_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}"; then
custom_build_profile=no
else
custom_build_profile=yes
fi
AC_MSG_RESULT([$with_build])
+AM_INIT_AUTOMAKE([1.11 no-define parallel-tests color-tests])
+AC_CONFIG_HEADERS([cvc4autoconfig.h])
+
+# Initialize libtool's configuration options.
+_LT_SET_OPTION([LT_INIT],[win32-dll])
+LT_INIT
+
+# Checks for programs.
+AC_PROG_CC
+AC_PROG_CXX
+AC_PROG_INSTALL
+
+# determine whether to use CLN or GMP.
+# we do this here so it can affect the build directory
+
+cvc4_use_gmp=0
+cvc4_use_cln=0
+
+AC_ARG_WITH(
+ [cln],
+ AS_HELP_STRING(
+ [--with-cln],
+ [use CLN instead of GMP (default, if CLN found)]
+ ),
+ [if test "$withval" = no; then
+ cvc4_use_gmp=1
+ else
+ cvc4_use_cln=1
+ fi
+ ]
+)
+
+AC_ARG_WITH(
+ [gmp],
+ AS_HELP_STRING(
+ [--with-gmp],
+ [use GMP instead of CLN]
+ ),
+ [if test "$withval" = no; then
+ cvc4_use_cln=1
+ else
+ cvc4_use_gmp=1
+ fi
+ ]
+)
+
+if test $cvc4_use_cln = 1 && test $cvc4_use_gmp = 1; then
+ # error
+ AC_MSG_ERROR([You cannot use both CLN and GMP. Please pick one.])
+fi
+
+if test $cvc4_use_cln = 1 || test $cvc4_use_cln = 0 -a $cvc4_use_gmp = 0; then
+ # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
+ # gracefully. You can only specify it once for a given library name. That
+ # is, even on separate if/else branches, you can't put
+ # PKG_CHECK_MODULES([CLN], ...). That's why things are so convoluted here,
+ # we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
+ PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
+ [cvc4_use_cln=1],
+ [if test $cvc4_use_cln = 0; then
+ # fall back to GMP
+ AC_MSG_NOTICE([CLN not installed (or too old), will use gmp])
+ else
+ # fail
+ AC_MSG_ERROR([CLN not installed (or too old)])
+ fi
+ ]
+ )
+fi
+if test $cvc4_use_cln = 0; then
+ # try GMP, fail if not found
+ 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/])])
+ cvc4_cln_or_gmp=gmp
+else
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
+ CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
+ CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
+ LIBS="${LIBS:+$LIBS }$CLN_LIBS"
+ cvc4_cln_or_gmp=cln
+fi
+
+if test $cvc4_cln_or_gmp = cln; then
+ AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.])
+else
+ AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.])
+fi
+AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln])
+AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
+
+# construct the build string
AC_MSG_CHECKING([for appropriate build string])
-build_type=`$ac_confdir/config/build-type $with_build $btargs`
+build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
if test "$custom_build_profile" = yes; then
if test "$with_build" = default; then
- build_type=`$ac_confdir/config/build-type custom $btargs`
+ build_type=`$ac_confdir/config/build-type custom $btargs $cvc4_cln_or_gmp`
fi
fi
AC_MSG_RESULT($build_type)
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_public.h; then
+elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
AC_MSG_RESULT([builds/$target/$build_type])
echo
if test -z "$ac_srcdir"; then
AC_MSG_RESULT([$enable_statistics])
if test "$enable_statistics" = yes; then
- CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-DCVC4_STATISTICS_ON"
- CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-DCVC4_STATISTICS_ON"
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
fi
AC_MSG_CHECKING([whether to include assertions in build])
CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
fi
-AM_INIT_AUTOMAKE([1.11 no-define parallel-tests color-tests])
-AC_CONFIG_HEADERS([cvc4autoconfig.h])
-
-# Initialize libtool's configuration options.
-_LT_SET_OPTION([LT_INIT],[win32-dll])
-LT_INIT
-
-# Checks for programs.
-AC_PROG_CC
-AC_PROG_CXX
-AC_PROG_INSTALL
# Check for ANTLR runantlr script (defined in config/antlr.m4)
AC_PROG_ANTLR
fi
# Checks for libraries.
-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/])])
-
-PKG_CHECK_MODULES([CLN], [cln >= 1.2.2])
-
-CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS -D__CVC4__USE_CLN_IMP"
-CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
-CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
-CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }$CLN_LIBS"
# Check for antlr C++ runtime (defined in config/antlr.m4)
AC_LIB_ANTLR
# Checks for typedefs, structures, and compiler characteristics.
#AC_HEADER_STDBOOL
-AC_TYPE_UINT16_T
-AC_TYPE_UINT32_T
-AC_TYPE_UINT64_T
-AC_TYPE_SIZE_T
+# these are bad macros, they clash with system header <stdint.h> !!
+#AC_TYPE_UINT16_T
+#AC_TYPE_UINT32_T
+#AC_TYPE_UINT64_T
+#AC_TYPE_SIZE_T
# Checks for library functions.
# (empty)
# still trigger certain automake behavior; see test/unit/Makefile.am.
AM_CONDITIONAL([CVC4_FALSE], [false])
+# set up substitutions for src/util/{rational,integer}.h.in
+if test $cvc4_cln_or_gmp = cln; then
+ CVC4_USE_CLN_IMP=1
+ CVC4_USE_GMP_IMP=0
+else
+ CVC4_USE_CLN_IMP=0
+ CVC4_USE_GMP_IMP=1
+fi
+AC_SUBST(CVC4_USE_CLN_IMP)
+AC_SUBST(CVC4_USE_GMP_IMP)
+
AC_CONFIG_FILES([
Makefile.builds
Makefile]
m4_esyscmd([find contrib/ src/ test/ -name Makefile.am | sort | sed 's,\.am$,,'])
+ src/util/rational.h
+ src/util/integer.h
)
AC_OUTPUT
# Final information to the user
+licensewarn=
if test "$custom_build_profile" = yes; then
if test "$with_build" = default; then
optimized="no"
fi
+if test $cvc4_cln_or_gmp = cln; then
+ mplibrary='cln (GPL)'
+ licensewarn="${licensewarn}Please note that CVC4 will be built against the Class Library for
+Numbers (CLN). This library is covered under the GPL, so use of this
+build of CVC4 will be more restrictive than CVC4's license would
+normally suggest. For full details of CLN and its license, please visit
+ http://www.ginac.de/CLN/
+To build CVC4 with GMP instead (which is covered under the more permissive
+LGPL), configure --without-cln.
+
+"
+else
+ mplibrary='gmp (LGPL)'
+fi
+
cat <<EOF
CVC4 $VERSION
Shared libs : $enable_shared
Static binary: $enable_static_binary
+MP library : $mplibrary
+
CPPFLAGS : $CPPFLAGS
CXXFLAGS : $CXXFLAGS
CFLAGS : $CFLAGS
libcvc4 version : $CVC4_LIBRARY_VERSION
libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION
-Now just type make, followed by make check or make install, as you like.
+${licensewarn}Now just type make, followed by make check or make install, as you like.
EOF
clibtarget="lib${clibbase}_la"
cat >"$srcdir/Makefile.am" <<EOF
AM_CPPFLAGS = \\
-$definitions -I@srcdir@/$topsrcdir/include -I@srcdir@/$topsrcdir
+$definitions -I@srcdir@/$topsrcdir/include -I@srcdir@/$topsrcdir -I@builddir@/$topsrcdir
AM_CXXFLAGS = -Wall$visibility
noinst_LTLIBRARIES = $clibname
--- /dev/null
+#!/bin/bash
+#
+# usage: switch-config [configuration]
+# switch-config -l
+#
+# Script to switch the "current" configuration of the CVC4 builds directory
+# to another one. Without an argument, it switches to the next alphabetically.
+# With an argument, it switches to that configuration. With -l, it lists the
+# available configurations.
+#
+# Only configurations in the "current" architecture (that for which the build directory is currently
+# configured) are considered.
+#
+# This script is useful because it's faster that re-configuring.
+#
+# Script assumes it lives under contrib/ in the root of the CVC4 source
+# tree.
+
+function usage {
+ echo "usage: `basename \"$0\"` [configuration]"
+ echo " `basename \"$0\"` -l"
+}
+
+if [ $# -gt 1 ]; then
+ usage
+ exit 1
+fi
+
+cd `dirname "$0"`/..
+
+if ! [ -d builds ]; then
+ echo "No configurations are available (no builds/ directory)."
+ exit
+fi
+
+if ! [ -e builds/current ]; then
+ echo "Cannot get current configuration."
+ exit 1
+fi
+
+current=(`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]\+\)/\(.*\),\1 \2,'`)
+arch=${current[0]}
+build=${current[1]}
+
+builds=(`ls "builds/$arch/"`)
+
+if ! [ -d "builds/$arch" ] || ! [ -d "builds/$arch/$build" ] || [ ${#builds[@]} -eq 0 ]; then
+ echo "builds/ directory in malformed state."
+ echo "You might want to blow it away and start from scratch."
+ exit 1
+fi
+
+function switchto {
+ perl -pi -e 's,^CURRENT_BUILD *= *.*,CURRENT_BUILD = '$arch/$1',' builds/current
+ echo "Current build switched to \`$1'."
+}
+
+if [ $# -eq 0 ]; then
+ first=
+ last=
+ setbuild=
+ for d in `ls "builds/$arch/"`; do
+ if [ -z "$first" ]; then first=$d; fi
+ if [ "$last" = "$build" ]; then setbuild=$d; break; fi
+ last=$d
+ done
+ if [ -z "$setbuild" ]; then setbuild=$first; fi
+ if [ "$setbuild" = "$build" ]; then
+ echo "There is only one build profile (\`$build'), and it is current."
+ else
+ switchto "$setbuild"
+ fi
+else
+ case $1 in
+ -l) for config in `ls -1 "builds/$arch/"`; do
+ if [ "$config" = "$build" ]; then
+ echo "$config" '*'
+ else
+ echo "$config"
+ fi
+ done ;;
+ -*) usage; exit 1 ;;
+ *) if ! [ -d "builds/$arch/$1" ]; then
+ echo "Build \`$1' does not exist."
+ exit 1
+ else
+ if [ "$1" = "$build" ]; then
+ echo "Build \`$1' is already the current build profile."
+ else
+ switchto "$1"
+ fi
+ fi ;;
+ esac
+fi
+
AM_CPPFLAGS =
-D__BUILDING_CVC4LIB \
- -I@srcdir@/include -I@srcdir@
+ -I@srcdir@/include -I@srcdir@ -I@builddir@
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
SUBDIRS = expr util context theory prop smt . parser main
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../include -I@srcdir@/..
+ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libcontext.la
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../include -I@srcdir@/..
+ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libexpr.la
#ifndef __CVC4_PUBLIC_H
#define __CVC4_PUBLIC_H
+#include <stdint.h>
+
#if defined _WIN32 || defined __CYGWIN__
# ifdef BUILDING_DLL
# ifdef __GNUC__
AM_CPPFLAGS = \
- -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
+ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES)
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas
bin_PROGRAMS = cvc4
AM_CPPFLAGS = \
-D__BUILDING_CVC4PARSERLIB \
- -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
+ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES)
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
SUBDIRS = smt smt2 cvc
AM_CPPFLAGS = \
-D__BUILDING_CVC4PARSERLIB \
- -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
+ -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. $(ANTLR_INCLUDES)
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable
# Compile generated C files using C++ compiler
AM_CPPFLAGS = \
-D__BUILDING_CVC4PARSERLIB \
- -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
+ -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. $(ANTLR_INCLUDES)
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable
# Compile generated C files using C++ compiler
AM_CPPFLAGS = \
-D__BUILDING_CVC4PARSERLIB \
- -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
+ -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. $(ANTLR_INCLUDES)
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable
# Compile generated C files using C++ compiler
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../include -I@srcdir@/..
+ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libprop.la
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../.. -I@srcdir@/../../include
+ -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../.. -I@builddir@/../.. -I@srcdir@/../../include
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -DNDEBUG
noinst_LTLIBRARIES = libminisat.la
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../include -I@srcdir@/..
+ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libsmt.la
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../include -I@srcdir@/..
+ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libtheory.la
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../../include -I@srcdir@/../..
+ -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libarith.la
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../../include -I@srcdir@/../..
+ -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libarrays.la
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../../include -I@srcdir@/../..
+ -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libbooleans.la
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../../include -I@srcdir@/../..
+ -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libbuiltin.la
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../../include -I@srcdir@/../..
+ -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libbv.la
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../../include -I@srcdir@/../..
+ -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libuf.la
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../include -I@srcdir@/..
+ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libutil.la
configuration.cpp \
rational.h \
integer.h \
+ bitvector.h \
+ bitvector.cpp \
+ gmp_util.h \
+ sexpr.h \
+ stats.h \
+ stats.cpp \
+ triple.h
+
+BUILT_SOURCES = \
+ rational.h \
+ integer.h
+
+if CVC4_CLN_IMP
+libutil_la_SOURCES += \
+ integer_cln_imp.cpp \
+ rational_cln_imp.cpp
+endif
+if CVC4_GMP_IMP
+libutil_la_SOURCES += \
+ integer_gmp_imp.cpp \
+ rational_gmp_imp.cpp
+endif
+
+EXTRA_DIST = \
rational_cln_imp.h \
integer_cln_imp.h \
rational_cln_imp.cpp \
integer_gmp_imp.h \
rational_gmp_imp.cpp \
integer_gmp_imp.cpp \
- bitvector.h \
- bitvector.cpp \
- gmp_util.h \
- sexpr.h \
- stats.h \
- stats.cpp \
- triple.h
+ rational.h.in \
+ integer.h.in
** \verbatim
** Original author: dejan
** Major contributors: cconway
- ** Minor contributors (to current version): taking, mdeters
+ ** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
#include <iostream>
#include "util/Assert.h"
-#include "util/gmp_util.h"
#include "util/integer.h"
namespace CVC4 {
The ACSys Group\n\
Courant Institute of Mathematical Sciences\n\
New York University\n\
- New York, NY 10012 USA\n");
+ New York, NY 10012 USA\n\n") +
+ (isBuiltWithCln() ? "\
+This CVC4 library uses CLN as its multi-precision arithmetic library.\n\n\
+CVC4 is open-source and is covered by the BSD license (modified).\n\
+However, CLN, the Class Library for Numbers, is covered by the GPL. Thus\n\
+this CVC4 library cannot be used in proprietary applications. Please\n\
+consult the CVC4 documentation for instructions about building a version\n\
+of CVC4 that links against GMP, and can be used in such applications.\n" :
+"This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\
+CVC4 is open-source and is covered by the BSD license (modified).\n");
+}
+
+bool Configuration::isBuiltWithGmp() {
+#ifdef CVC4_GMP_IMP
+ return true;
+#else /* CVC4_GMP_IMP */
+ return false;
+#endif /* CVC4_GMP_IMP */
+}
+
+bool Configuration::isBuiltWithCln() {
+#ifdef CVC4_CLN_IMP
+ return true;
+#else /* CVC4_CLN_IMP */
+ return false;
+#endif /* CVC4_CLN_IMP */
}
}/* CVC4 namespace */
static unsigned getVersionRelease();
static std::string about();
+
+ static bool isBuiltWithGmp();
+
+ static bool isBuiltWithCln();
};
}/* CVC4 namespace */
** \todo document this file
**/
-#ifndef __CVC4__GMP_H_
-#define __CVC4__GMP_H_
+#ifndef __CVC4__GMP_UTIL_H
+#define __CVC4__GMP_UTIL_H
#include <gmpxx.h>
namespace CVC4 {
- /** Hashes the gmp integer primitive in a word by word fashion. */
- inline size_t gmpz_hash(const mpz_t toHash) {
- size_t hash = 0;
- for (int i=0, n=mpz_size(toHash); i<n; ++i){
- mp_limb_t limb = mpz_getlimbn(toHash, i);
- hash = hash * 2;
- hash = hash xor limb;
- }
- return hash;
+/** Hashes the gmp integer primitive in a word by word fashion. */
+inline size_t gmpz_hash(const mpz_t toHash) {
+ size_t hash = 0;
+ for (int i = 0, n = mpz_size(toHash); i < n; ++i){
+ mp_limb_t limb = mpz_getlimbn(toHash, i);
+ hash = hash * 2;
+ hash = hash xor limb;
}
+ return hash;
+}/* gmpz_hash() */
-}
+}/* CVC4 namespace */
-#endif /* __CVC4__GMP_H_ */
+#endif /* __CVC4__GMP_UTIL_H */
+++ /dev/null
-/********************* */
-/*! \file integer.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, cconway, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief A multiprecision integer constant.
- **
- ** A multiprecision integer constant.
- **/
-
-#ifdef __CVC4__USE_GMP_IMP
-#include "util/integer_gmp_imp.h"
-#endif
-#ifdef __CVC4__USE_CLN_IMP
-#include "util/integer_cln_imp.h"
-#endif
--- /dev/null
+/********************* */
+/*! \file integer.h.in
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, cconway, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A multiprecision integer constant.
+ **
+ ** A multiprecision integer constant.
+ **/
+
+// this is used to avoid a public header dependence on cvc4autoconfig.h
+#if /* use CLN */ @CVC4_USE_CLN_IMP@
+# define CVC4_CLN_IMP
+#endif /* @CVC4_USE_CLN_IMP@ */
+#if /* use GMP */ @CVC4_USE_GMP_IMP@
+# define CVC4_GMP_IMP
+#endif /* @CVC4_USE_GMP_IMP@ */
+
+#ifdef CVC4_CLN_IMP
+# include "util/integer_cln_imp.h"
+#endif /* CVC4_CLN_IMP */
+
+#ifdef CVC4_GMP_IMP
+# include "util/integer_gmp_imp.h"
+#endif /* CVC4_GMP_IMP */
/********************* */
-/*! \file integer.cpp
+/*! \file integer_cln_imp.cpp
** \verbatim
** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** literature.) A consquence is that that the numerator and denominator may be
** different than the values used to construct the Rational.
**/
-#ifdef __CVC4__USE_CLN_IMP
+#include "cvc4autoconfig.h"
#include "util/integer.h"
+#ifndef CVC4_CLN_IMP
+# error "This source should only ever be built if CVC4_CLN_IMP is on !"
+#endif /* CVC4_CLN_IMP */
+
using namespace CVC4;
std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
return os << n.toString();
}
-#endif /* __CVC4__USE_CLN_IMP */
/********************* */
-/*! \file integer.h
+/*! \file integer_cln_imp.h
** \verbatim
** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan, cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief A multiprecision integer constant.
+ ** \brief A multiprecision integer constant; wraps a CLN multiprecision
+ ** integer.
**
- ** A multiprecision integer constant.
+ ** A multiprecision integer constant; wraps a CLN multiprecision integer.
**/
-#ifdef __CVC4__USE_CLN_IMP
-
#include "cvc4_public.h"
#ifndef __CVC4__INTEGER_H
#include <cln/input.h>
#include <cln/integer_io.h>
#include "util/Assert.h"
-#include "util/gmp_util.h"
namespace CVC4 {
#endif /* __CVC4__INTEGER_H */
-#endif /* __CVC4__USE_CLN_IMP */
/********************* */
-/*! \file integer.cpp
+/*! \file integer_gmp_imp.cpp
** \verbatim
** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** different than the values used to construct the Rational.
**/
-#ifdef __CVC4__USE_GMP_IMP
+#include "cvc4autoconfig.h"
#include "util/integer.h"
+#ifndef CVC4_GMP_IMP
+# error "This source should only ever be built if CVC4_GMP_IMP is on !"
+#endif /* CVC4_GMP_IMP */
+
using namespace CVC4;
std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
return os << n.toString();
}
-#endif /* __CVC4__USE_GMP_IMP */
+
/********************* */
-/*! \file integer.h
+/*! \file integer_gmp_imp.h
** \verbatim
** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan, cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief A multiprecision integer constant.
+ ** \brief A multiprecision integer constant; wraps a GMP multiprecision
+ ** integer.
**
- ** A multiprecision integer constant.
+ ** A multiprecision integer constant; wraps a GMP multiprecision integer.
**/
-#ifdef __CVC4__USE_GMP_IMP
#include "cvc4_public.h"
#ifndef __CVC4__INTEGER_H
}/* CVC4 namespace */
#endif /* __CVC4__INTEGER_H */
-#endif /* __CVC4__USE_GMP_IMP */
+
+++ /dev/null
-/********************* */
-/*! \file rational.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters, cconway
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Multi-precision rational constants.
- **
- ** Multi-precision rational constants.
- **/
-
-#ifdef __CVC4__USE_GMP_IMP
-#include "util/rational_gmp_imp.h"
-#endif
-#ifdef __CVC4__USE_CLN_IMP
-#include "util/rational_cln_imp.h"
-#endif
--- /dev/null
+/********************* */
+/*! \file rational.h.in
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, mdeters, cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Multi-precision rational constants.
+ **
+ ** Multi-precision rational constants.
+ **/
+
+// this is used to avoid a public header dependence on cvc4autoconfig.h
+#if /* use CLN */ @CVC4_USE_CLN_IMP@
+# define CVC4_CLN_IMP
+#endif /* @CVC4_USE_CLN_IMP@ */
+#if /* use GMP */ @CVC4_USE_GMP_IMP@
+# define CVC4_GMP_IMP
+#endif /* @CVC4_USE_GMP_IMP@ */
+
+#ifdef CVC4_CLN_IMP
+# include "util/rational_cln_imp.h"
+#endif /* CVC4_CLN_IMP */
+
+#ifdef CVC4_GMP_IMP
+# include "util/rational_gmp_imp.h"
+#endif /* CVC4_GMP_IMP */
/*! \file rational_cln_imp.cpp
** \verbatim
** Original author: taking
- ** Major contributors: mdeters, cconway
+ ** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** A multi-precision rational constant.
**/
-#ifdef __CVC4__USE_CLN_IMP
-
-
-#include "util/integer.h"
+#include "cvc4autoconfig.h"
#include "util/rational.h"
+#include "util/integer.h"
#include <string>
+#ifndef CVC4_CLN_IMP
+# error "This source should only ever be built if CVC4_CLN_IMP is on !"
+#endif /* CVC4_CLN_IMP */
+
using namespace std;
using namespace CVC4;
return os << q.toString();
}
-#endif /* __CVC4__USE_CLN_IMP */
/********************* */
-/*! \file rational.h
+/*! \file rational_cln_imp.h
** \verbatim
** Original author: taking
** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters, cconway
+ ** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Multi-precision rational constants.
+ ** \brief Multiprecision rational constants; wraps a CLN multiprecision
+ ** rational.
**
- ** Multi-precision rational constants.
+ ** Multiprecision rational constants; wraps a CLN multiprecision rational.
**/
-#ifdef __CVC4__USE_CLN_IMP
-
#include "cvc4_public.h"
#ifndef __CVC4__RATIONAL_H
#endif /* __CVC4__RATIONAL_H */
-#endif /* __CVC4__USE_CLN_IMP */
/********************* */
-/*! \file rational.cpp
+/*! \file rational_gmp_imp.cpp
** \verbatim
** Original author: taking
- ** Major contributors: mdeters, cconway
+ ** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
**
** A multi-precision rational constant.
**/
-#ifdef __CVC4__USE_GMP_IMP
-#include "util/integer.h"
+#include "cvc4autoconfig.h"
#include "util/rational.h"
+#include "util/integer.h"
#include <string>
+#ifndef CVC4_GMP_IMP
+# error "This source should only ever be built if CVC4_GMP_IMP is on !"
+#endif /* CVC4_GMP_IMP */
+
using namespace std;
using namespace CVC4;
return os << q.toString();
}
-#endif /* __CVC4__USE_GMP_IMP */
/********************* */
-/*! \file rational.h
+/*! \file rational_gmp_imp.h
** \verbatim
** Original author: taking
** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters, cconway
+ ** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Multi-precision rational constants.
+ ** \brief Multiprecision rational constants; wraps a GMP multiprecision
+ ** rational.
**
- ** Multi-precision rational constants.
+ ** Multiprecision rational constants; wraps a GMP multiprecision rational.
**/
-#ifdef __CVC4__USE_GMP_IMP
#include "cvc4_public.h"
}/* CVC4 namespace */
#endif /* __CVC4__RATIONAL_H */
-#endif /* __CVC4__USE_GMP_IMP */
+
** \verbatim
** Original author: cconway
** Major contributors: none
- ** Minor contributors (to current version): taking, mdeters
+ ** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
if HAVE_CXXTESTGEN
AM_CPPFLAGS = \
- -I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" \
+ -I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" \
+ "-I@top_srcdir@/src" "-I@top_builddir@/src" \
$(ANTLR_INCLUDES) $(TEST_CPPFLAGS)
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(TEST_CXXFLAGS)
AM_LDFLAGS = $(TEST_LDFLAGS)
projects / cvc5.git / commitdiff