From: Morgan Deters Date: Sat, 3 Jul 2010 17:59:19 +0000 (+0000) Subject: With this commit come a number of changes to build system to support X-Git-Tag: cvc5-1.0.0~8960 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6759aa95d4057a2a058974991bf7c9858899a477;p=cvc5.git With this commit come a number of changes to build system to support building with CLN or with GMP, the contrib/switch-config script (enabling "fast switching" of different configurations in the same builds/ directory), and also some minor changes. ./configure --with-gmp (or --without-cln) forces building with GMP and doesn't even look for CLN. Configure fails if GMP isn't installed. ./configure --with-cln (or --without-gmp) forces building with CLN and doesn't even look for GMP. Configure fails if CLN isn't installed. ./configure [no arguments] will detect what's installed. CLN is default, if it isn't installed, or is too old, GMP is looked for (and configure fails if neither is available). It is an error to specify --with-gmp --with-cln (or --without-* for both) at the same time. Building with CLN (whether forced or detected) adds a note to the configure output mentioning the fact that the build of CVC4 will be linked against a GPLed library and notifying the user of the --without-cln option. Building with GMP (whether forced or detected) affects the build directory, so CLN and GMP builds are kept separate. ./configure --with-cln debug builds in builds/$arch/debug ./configure --with-gmp debug builds in builds/$arch/debug-gmp The final binaries are linked explicitly against either gmp or cln, but not both. If linked against cln, cln pulls in gmp as a dependency, so the result will be linked against both. === Details that you probably don't care about === The headers src/util/{integer,rational}.h are generated from the corresponding .in versions. A user installing a CVC4-devel package will get the headers for rational and integer that match the library that s/he installs. The preprocessor #defines CVC4_GMP_IMP and CVC4_CLN_IMP are added to cvc4autoconfig.h. Only one is ever #defined. cvc4autoconfig.h doesn't need to be #included directly; you get it through #including cvc4_private.h (or the parser version). AM_CONDITIONALs are also defined so that Makefiles get the cln/gmp configuration. AC_SUBSTs are defined so that public headers (see src/util/{integer,rational}.h.in) can use the setting. *Public* headers that need to depend on the cln/gmp configuration can't use cvc4autoconfig.h, because we're keeping that in the private, internal-only space, never to be installed on users' machines. Here, something special is required, like the configure-level generation of headers that I used for src/util/{integer,rational}.h.in. Tim's Integer and Rational wrappers are the only bits of code that should care which library is used (and also src/util/configuration.h, which gives the user of the library information about how CVC4 is built), and possibly some unit tests (?). --- diff --git a/AUTHORS b/AUTHORS index 4f94f7c01..21217b578 100644 --- a/AUTHORS +++ b/AUTHORS @@ -9,7 +9,8 @@ The core authors and designers of CVC4 are: Mina Jeong , New York University Dejan Jovanovic , 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 , 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 , 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 diff --git a/COPYING b/COPYING index 7008c8d90..02132ec28 100644 --- a/COPYING +++ b/COPYING @@ -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 !! +#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 <"$srcdir/Makefile.am" < + #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 #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 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 #include #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 deleted file mode 100644 index 73fcb73a3..000000000 --- a/src/util/rational.h +++ /dev/null @@ -1,24 +0,0 @@ -/********************* */ -/*! \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 diff --git a/src/util/rational.h.in b/src/util/rational.h.in new file mode 100644 index 000000000..88c488290 --- /dev/null +++ b/src/util/rational.h.in @@ -0,0 +1,33 @@ +/********************* */ +/*! \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 */ 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 +#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 +#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)