diff options
43 files changed, 461 insertions, 144 deletions
@@ -9,7 +9,8 @@ The core authors and designers of CVC4 are: 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 @@ -18,7 +19,8 @@ The following individuals contributed code to CVC3 that may have been incorporat 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 @@ -36,3 +38,11 @@ The following individuals contributed code to CVC Lite that may have been incorp 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 @@ -2,7 +2,11 @@ CVC4 is copyright (C) 2009, 2010 the ACSys research group at the Courant 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 @@ -115,3 +119,16 @@ Their copyright: 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". diff --git a/config/build-type b/config/build-type index 15214bcf0..0449f3375 100755 --- a/config/build-type +++ b/config/build-type @@ -29,6 +29,9 @@ # 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 @@ -40,6 +43,8 @@ shift while [ $# -gt 0 ]; do case "$1" in + cln) ;; + gmp) gmp=1 ;; no*) eval `expr "$1" : 'no\(.*\)'`=0 ;; *) eval $1=1 ;; esac @@ -47,7 +52,7 @@ while [ $# -gt 0 ]; do 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 diff --git a/config/cvc4.m4 b/config/cvc4.m4 index 90f4ca093..ea7d77223 100644 --- a/config/cvc4.m4 +++ b/config/cvc4.m4 @@ -42,6 +42,14 @@ do 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\""' diff --git a/configure.ac b/configure.ac index 2fd82a925..0bced3680 100644 --- a/configure.ac +++ b/configure.ac @@ -54,6 +54,12 @@ config_cmdline="$@" 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 @@ -75,7 +81,7 @@ AC_ARG_WITH([build], 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 @@ -146,11 +152,102 @@ if test -n "${enable_statistics+set}"; then 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) @@ -165,7 +262,7 @@ 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 @@ -337,8 +434,7 @@ fi 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]) @@ -452,17 +548,6 @@ if test "$enable_profiling" = yes; then 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 @@ -529,15 +614,6 @@ if test -n "$CXXTEST"; then 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 @@ -547,10 +623,11 @@ AC_CHECK_HEADERS([getopt.h unistd.h]) # 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) @@ -606,15 +683,29 @@ AC_SUBST(mk_include) # 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 @@ -635,6 +726,21 @@ else 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 @@ -655,6 +761,8 @@ Static libs : $enable_static Shared libs : $enable_shared Static binary: $enable_static_binary +MP library : $mplibrary + CPPFLAGS : $CPPFLAGS CXXFLAGS : $CXXFLAGS CFLAGS : $CFLAGS @@ -663,6 +771,6 @@ LDFLAGS : $LDFLAGS 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 diff --git a/contrib/addsourcedir b/contrib/addsourcedir index 8c7d74d90..190864469 100644 --- a/contrib/addsourcedir +++ b/contrib/addsourcedir @@ -81,7 +81,7 @@ 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 diff --git a/contrib/switch-config b/contrib/switch-config new file mode 100755 index 000000000..ad28464e7 --- /dev/null +++ b/contrib/switch-config @@ -0,0 +1,95 @@ +#!/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 + diff --git a/src/Makefile.am b/src/Makefile.am index a805f8c85..97c66ac89 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -14,7 +14,7 @@ LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@ 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 diff --git a/src/context/Makefile.am b/src/context/Makefile.am index 3d912e685..7a40bab1b 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 225624a8b..db863440c 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h index e1b515ba5..8375f7571 100644 --- a/src/include/cvc4_public.h +++ b/src/include/cvc4_public.h @@ -21,6 +21,8 @@ #ifndef __CVC4_PUBLIC_H #define __CVC4_PUBLIC_H +#include <stdint.h> + #if defined _WIN32 || defined __CYGWIN__ # ifdef BUILDING_DLL # ifdef __GNUC__ diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 9ffa43ca0..82ff00a60 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -1,5 +1,5 @@ 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 diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index a323ec3cb..b1f265b56 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -14,7 +14,7 @@ LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ 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 diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index 9754c1063..cfe983727 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index 418b204dc..f5ea3aae3 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am index 3066f2247..aabae5352 100644 --- a/src/parser/smt2/Makefile.am +++ b/src/parser/smt2/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 48c9c3fd2..06504e73c 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am index 77d1d602e..56f61adad 100644 --- a/src/prop/minisat/Makefile.am +++ b/src/prop/minisat/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index 72dd8f3df..90d58904a 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index bb9d19b25..a2a206d40 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 541426ac3..4d299e8af 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index 0c6e9006f..8a0a180db 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index 478fca1cf..3bd8b5a39 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am index 5694dea84..d1df0e425 100644 --- a/src/theory/builtin/Makefile.am +++ b/src/theory/builtin/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index 94941d406..cab90bbdb 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 39586345b..4e399aeb7 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -1,6 +1,6 @@ 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 diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 1446412ce..b6ca5bcc6 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -1,6 +1,6 @@ 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 @@ -26,6 +26,30 @@ libutil_la_SOURCES = \ 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 \ @@ -34,10 +58,5 @@ libutil_la_SOURCES = \ 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 diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 928592d9e..0b5952481 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -3,7 +3,7 @@ ** \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 @@ -24,7 +24,6 @@ #include <iostream> #include "util/Assert.h" -#include "util/gmp_util.h" #include "util/integer.h" namespace CVC4 { diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 2a7563f82..12908c672 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -100,7 +100,32 @@ Copyright (C) 2009, 2010\n\ 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 */ diff --git a/src/util/configuration.h b/src/util/configuration.h index 00651202d..6d5ac12a1 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -60,6 +60,10 @@ public: static unsigned getVersionRelease(); static std::string about(); + + static bool isBuiltWithGmp(); + + static bool isBuiltWithCln(); }; }/* CVC4 namespace */ diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index a425690a5..87102e644 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -17,24 +17,24 @@ ** \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 */ diff --git a/src/util/integer.h b/src/util/integer.h.in index c57450d5f..7e1b9a1aa 100644 --- a/src/util/integer.h +++ b/src/util/integer.h.in @@ -1,5 +1,5 @@ /********************* */ -/*! \file integer.h +/*! \file integer.h.in ** \verbatim ** Original author: taking ** Major contributors: none @@ -16,9 +16,18 @@ ** 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 +// 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 */ diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index 35293bb84..a6cad96d1 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -1,9 +1,9 @@ /********************* */ -/*! \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 @@ -21,14 +21,17 @@ ** 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 */ diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 2154952f0..8551d0a6a 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -1,9 +1,9 @@ /********************* */ -/*! \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 @@ -11,13 +11,12 @@ ** 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 @@ -30,7 +29,6 @@ #include <cln/input.h> #include <cln/integer_io.h> #include "util/Assert.h" -#include "util/gmp_util.h" namespace CVC4 { @@ -226,4 +224,3 @@ std::ostream& operator<<(std::ostream& os, const Integer& n); #endif /* __CVC4__INTEGER_H */ -#endif /* __CVC4__USE_CLN_IMP */ diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index 7bda7f02a..112713aa5 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -1,9 +1,9 @@ /********************* */ -/*! \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 @@ -22,12 +22,16 @@ ** 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 */ + diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 7217d0c5a..b065dca23 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -1,9 +1,9 @@ /********************* */ -/*! \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 @@ -11,12 +11,12 @@ ** 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 @@ -165,4 +165,4 @@ std::ostream& operator<<(std::ostream& os, const Integer& n); }/* CVC4 namespace */ #endif /* __CVC4__INTEGER_H */ -#endif /* __CVC4__USE_GMP_IMP */ + diff --git a/src/util/rational.h b/src/util/rational.h.in index 73fcb73a3..88c488290 100644 --- a/src/util/rational.h +++ b/src/util/rational.h.in @@ -1,5 +1,5 @@ /********************* */ -/*! \file rational.h +/*! \file rational.h.in ** \verbatim ** Original author: taking ** Major contributors: none @@ -16,9 +16,18 @@ ** 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 +// 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 */ diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index 0960b79b9..7baf8d3bf 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -2,7 +2,7 @@ /*! \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) @@ -16,13 +16,15 @@ ** 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; @@ -51,4 +53,3 @@ std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){ return os << q.toString(); } -#endif /* __CVC4__USE_CLN_IMP */ diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 347c1d195..ae172f262 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -1,9 +1,9 @@ /********************* */ -/*! \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 @@ -11,13 +11,12 @@ ** 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 @@ -283,4 +282,3 @@ std::ostream& operator<<(std::ostream& os, const Rational& n); #endif /* __CVC4__RATIONAL_H */ -#endif /* __CVC4__USE_CLN_IMP */ diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index e5ff11c07..a0af69b4c 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -1,8 +1,8 @@ /********************* */ -/*! \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) @@ -15,12 +15,16 @@ ** ** 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; @@ -49,4 +53,3 @@ std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){ return os << q.toString(); } -#endif /* __CVC4__USE_GMP_IMP */ diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index ab88a0d52..ce94dfe24 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -1,9 +1,9 @@ /********************* */ -/*! \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 @@ -11,11 +11,11 @@ ** 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" @@ -259,4 +259,4 @@ std::ostream& operator<<(std::ostream& os, const Rational& n); }/* CVC4 namespace */ #endif /* __CVC4__RATIONAL_H */ -#endif /* __CVC4__USE_GMP_IMP */ + diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 6b32c46bb..607075658 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -3,7 +3,7 @@ ** \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 diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 42589d84c..e427e3506 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -45,7 +45,8 @@ TEST_DEPS_DIST = \ 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) |