From 464bbe3b057bde32b9e0e1aa1f989818dba585db Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 17 Dec 2013 12:40:50 -0500 Subject: [PATCH] some config changes: new --bsd option, readline gives warning, default build is now production. --- COPYING | 50 +++++---- INSTALL | 7 +- NEWS | 7 ++ README | 4 +- config/cvc4.m4 | 3 +- config/readline.m4 | 3 + configure.ac | 175 ++++++++++++++++--------------- src/main/options | 1 + src/util/configuration.h | 4 + src/util/configuration_private.h | 34 +++--- 10 files changed, 165 insertions(+), 123 deletions(-) diff --git a/COPYING b/COPYING index 40cbdaa6b..8babef432 100644 --- a/COPYING +++ b/COPYING @@ -1,11 +1,15 @@ CVC4 is copyright (C) 2009, 2010, 2011, 2012, 2013 New York University and The University of Iowa. All rights reserved. -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 GLPK, and how to ensure -you have a build that doesn't link against GPLed libraries. +The source code of CVC4 is open and available to students, researchers, +software companies, and everyone else to study, to modify, and to +redistribute original or modified versions; distribution is under the +terms of the modified BSD license. However, CVC4 can be configured (and +is, by default) to link against some GPLed libraries, and therefore the +use of these builds may be restricted in non-GPL-compatible projects. +See below for a discussion of CLN, GLPK, and Readline (the three GPLed +optional library dependences for CVC4), 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 @@ -19,7 +23,7 @@ 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. --- Morgan Deters Thu, 05 Dec 2013 14:22:26 -0500 +-- Morgan Deters Tue, 17 Dec 2013 14:35:55 -0500 CVC4 incorporates MiniSat code, excluded from the above copyright. See src/sat/minisat. Its copyright: @@ -232,28 +236,38 @@ Their copyright: (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: +CVC4 can be optionally configured to link against CLN, the Class Library for +Numbers, available here: http://www.ginac.de/CLN/ Please be advised that as this library is covered under the GPLv3, if you choose to use the combined work, "CVC4+CLN," by building CVC4 with CLN, then it is also covered under the GPLv3. If you want to make sure you build -a version of CVC4 that uses libgmp, the GNU Multiple Precision Arithmetic -Library, configure CVC4 with "--with-gmp" before building (though that is the -default). It can then be used in contexts where you want to license CVC4 -under the (modified) BSD license. +a version of CVC4 that uses no GPLed libraries, configure CVC4 with the +"--bsd" option before building. CVC4 can then be used in contexts where you +want to license CVC4 under the (modified) BSD license. -Certain builds of CVC4 link against a GPLed library, GLPK, the GNU Linear +CVC4 can be optionally configured to link against GLPK, the GNU Linear Programming Kit, available here: http://www.gnu.org/software/glpk/ Please be advised that as this library is covered under the GPLv3, if you choose to use the combined work, "CVC4+GLPK," by building CVC4 with -GLPK, then it is also covered under the GPLv3. If you want to make sure -you build a version of CVC4 that does not use GLPK, configure CVC4 with -"--without-glpk" before building (though that is the default). It can -then be used in contexts where you want to license CVC4 under the -(modified) BSD license. +GLPK, then it is also covered under the GPLv3. If you want to make sure you +build a version of CVC4 that uses no GPLed libraries, configure CVC4 with the +"--bsd" option before building. CVC4 can then be used in contexts where you +want to license CVC4 under the (modified) BSD license. + +CVC4 can be optionally configured to link against GNU Readline for improved +text-editing support in interactive mode. GNU Readline is available here: + + http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html + +Please be advised that as this library is covered under the GPLv3, if +you choose to use the combined work, "CVC4+Readline," by building CVC4 with +Readline, then it is also covered under the GPLv3. If you want to make sure +you build a version of CVC4 that uses no GPLed libraries, configure CVC4 with +the "--bsd" option before building. CVC4 can then be used in contexts where +you want to license CVC4 under the (modified) BSD license. diff --git a/INSTALL b/INSTALL index f0e1f6cc6..d8634f3e8 100644 --- a/INSTALL +++ b/INSTALL @@ -126,7 +126,12 @@ GLPK. The GNU Readline library is optionally used to provide command editing, tab completion, and history functionality at the CVC prompt (when running in interactive mode). Check your distribution for a -package named "libreadline-dev" or "readline-devel" or similar. +package named "libreadline-dev" or "readline-devel" or similar. This +library is covered by the GNU General Public License, version 3. Like +the above-mentioned libraries, if you choose to use CVC4 with readline +support, you are licensing CVC4 under that same license. (Please visit +http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html for more +details about readline.) The Boost C++ threading library (often packaged independently of the Boost base library) is needed to run CVC4 in "portfolio" diff --git a/NEWS b/NEWS index 46f5deee2..5c42481b4 100644 --- a/NEWS +++ b/NEWS @@ -4,6 +4,13 @@ Changes since 1.3 ================= * Timed statistics are now properly updated even on process abort. +* By default, CVC4 builds in "production" mode (optimized, with fewer + internal checks on). The common alternative is a "debug" build, which + is much slower. CVC4 also builds with GPL dependences by default now + (if those libraries are available), as this is the best-performing + version of CVC4. However, the new configure option "--bsd" disables + these GPL dependences and builds the best-performing BSD-licenced version + of CVC4. Changes since 1.2 ================= diff --git a/README b/README index c09fe979c..c5b751d0a 100644 --- a/README +++ b/README @@ -17,8 +17,8 @@ from any previous version. CVC4 is intended to be an open and extensible SMT engine. It can be used as a stand-alone tool or as a library. It has been designed to increase the performance and reduce the memory overhead of its -predecessors. It is written entirely in C++ and is released under a -free software license (see the file COPYING in the source +predecessors. It is written entirely in C++ and is released under an +open-source software license (see the file COPYING in the source distribution). *** Getting started with CVC4 diff --git a/config/cvc4.m4 b/config/cvc4.m4 index aefce193a..4b8b2e342 100644 --- a/config/cvc4.m4 +++ b/config/cvc4.m4 @@ -16,8 +16,9 @@ AC_DEFUN([CVC4_REWRITE_ARGS_FOR_BUILD_PROFILE], handle_option() { ac_option="$[]1" case $ac_option in + --bsd) ac_option='CVC4_BSD_LICENSED_CODE_ONLY=1' ;; -*|*=*) ;; - production|production-*|debug|debug-*|default|default-*|competition|competition-*) + production|production-*|debug|debug-*|competition|competition-*) # regexp `\?' not supported on Mac OS X ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'` ac_cvc4_build_profile_set=yes diff --git a/config/readline.m4 b/config/readline.m4 index 44be9ff41..c298f3db4 100644 --- a/config/readline.m4 +++ b/config/readline.m4 @@ -9,6 +9,9 @@ readline_compentry_func_returns_charp=0 READLINE_LIBS= if test "$with_readline" = no; then AC_MSG_RESULT([no, readline disabled by user]) +elif test "$with_readline" = check -a -n "$CVC4_BSD_LICENSED_CODE_ONLY"; then + AC_MSG_RESULT([no, user requested BSD-compatible dependences only]) + with_readline=no else if test "$with_readline" = check; then AC_MSG_RESULT([no preference by user, will auto-detect]) diff --git a/configure.ac b/configure.ac index bbc9169f0..80174b299 100644 --- a/configure.ac +++ b/configure.ac @@ -107,10 +107,10 @@ fi AC_MSG_CHECKING([for requested build profile]) AC_ARG_WITH([build], [AS_HELP_STRING([--with-build=profile], - [for profile in {production,debug,default,competition,personal}])]) + [for profile in {production,debug,competition,personal}])]) -if test -z "${with_build+set}" -o "$with_build" = default; then - with_build=default +if test -z "${with_build+set}"; then + with_build=production 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_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}"; then custom_build_profile=no @@ -237,11 +237,8 @@ AC_PROG_INSTALL CVC4_GCC_VERSION -# [chris 8/24/2010] The user *must* specify --with-cln to get CLN -# (and, thus, opt in to the GPL dependency). - -cvc4_use_gmp=0 -cvc4_use_cln=0 +cvc4_use_gmp=2 +cvc4_use_cln=2 AC_ARG_WITH( [cln], @@ -249,41 +246,49 @@ AC_ARG_WITH( [--with-cln], [use CLN instead of GMP] ), - [if test "$withval" != no; then - cvc4_use_cln=1 - fi + [case "$withval" in + y|ye|yes|Y|YE|YES) cvc4_use_cln=1 ;; + n|no|N|NO) cvc4_use_cln=0 ;; + esac ] ) -# [chris 8/24/2010] --with-gmp has no practical effect, since GMP is -# the default. Could be useful if other options are added later. - AC_ARG_WITH( [gmp], AS_HELP_STRING( [--with-gmp], - [use GMP instead of CLN (default)] + [use GMP instead of CLN] ), - [if test "$withval" = no; then - if test $cvc4_use_cln = 0; then - AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.]) - fi - else - cvc4_use_gmp=1 - fi + [case "$withval" in + y|ye|yes|Y|YE|YES) cvc4_use_gmp=1 ;; + n|no|N|NO) cvc4_use_gmp=0 ;; + esac ] ) -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.]) +if test $cvc4_use_cln = 1 -a $cvc4_use_gmp = 1 || test $cvc4_use_cln = 0 -a $cvc4_use_gmp = 0; then + AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.]) +fi +if test $cvc4_use_gmp = 1; then + cvc4_use_cln=0 +elif test $cvc4_use_gmp = 0; then + cvc4_use_cln=1 +elif test $cvc4_use_cln = 1; then + cvc4_use_gmp=0 +elif test $cvc4_use_cln = 0; then + cvc4_use_gmp=1 fi # try GMP, fail if not found; GMP is required for both CLN and for GMP # versions of CVC4 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])]) -if test $cvc4_use_cln = 1; then +if test $cvc4_use_cln = 2 -a -n "$CVC4_BSD_LICENSED_CODE_ONLY"; then + cvc4_use_cln=0 + cvc4_use_gmp=1 +fi + +if test $cvc4_use_cln != 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 @@ -295,12 +300,12 @@ if test $cvc4_use_cln = 1; then AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include ]], [[cln::cl_F pi = "3.1415926";]])]) AC_LANG_POP([C++]) ], - [if test $cvc4_use_cln = 0; then - # fall back to GMP - AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp]) - else + [if test $cvc4_use_cln = 1; then # fail AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing]) + else + # fall back to GMP + AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp]) fi ] ) @@ -331,11 +336,6 @@ if test -z "$ac_confdir"; then ac_confdir="$srcdir" fi 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 $cvc4_cln_or_gmp` - fi -fi AC_MSG_RESULT($build_type) # Require building in target and build-specific build directory: @@ -897,7 +897,7 @@ if test -z "$LFSC"; then elif test "$enable_proof" = yes; then support_proof_tests='yes, proof regression tests enabled' else - support_proof_tests='no, proof generation disabled for this build' + support_proof_tests='no, proof-generation disabled for this build' fi AC_SUBST([LFSC]) AC_SUBST([LFSCARGS]) @@ -1288,29 +1288,12 @@ fi AM_CONDITIONAL([CVC4_NEEDS_REPLACEMENT_FUNCTIONS], [test -n "$LIBOBJS"]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h]) - -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3]) - -AC_OUTPUT - # Final information to the user +gpl=no licensewarn= if test "$custom_build_profile" = yes; then - if test "$with_build" = default; then - with_build=custom - else - with_build="$with_build (customized)" - fi + with_build="$with_build (customized)" fi support_unit_tests='cxxtest not found; unit tests not supported' @@ -1327,46 +1310,50 @@ else fi if test $have_libglpk -eq 1; then - licensewarn="${licensewarn}Please note that CVC4 will be built against the GNU Linear Programming -Kit (GLPK). 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 GLPK and its license, please visit - http://www.gnu.org/software/glpk/ -To build CVC4 without GLPK, configure --without-glpk (which is the default). + gpl=yes + gpllibs="${gpllibs} glpk" +fi -" +if test $have_libreadline -eq 1; then + gpl=yes + gpllibs="${gpllibs} readline" 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. - -" + gpl=yes + gpllibs="${gpllibs} cln" if test $with_portfolio = yes; then - licensewarn="${licensewarn} -WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING -WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING - -Note that CLN is UNSAFE FOR USE in parallel contexts! -This build of CVC4 cannot be used safely as a portfolio solver. -since the result of building with CLN will include numerous race -conditions on the refcounts internal to CLN. - -WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING -WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING + AC_ERROR([Bad configuration detected: cannot build portfolio with CLN. +Please specify only one of --with-portfolio and --with-cln.]) + fi +else + mplibrary='gmp' +fi -" +if test "$gpl" = yes; then + if test -n "$CVC4_BSD_LICENSED_CODE_ONLY"; then + AC_ERROR([Bad configuration detected: user requested BSD-licensed code only, but also requested GPLed libraries:$gpllibs]) fi + + licensewarn="${licensewarn}"'**************************************************************************** +Please note that CVC4 will be built against the following GPLed libraries: + '"$gpllibs"' +As these libraries are covered under the GPLv3, so is this build of CVC4. +CVC4 is also available to you under the terms of the (modified) BSD license. +If you prefer to license CVC4 under those terms, please configure with the +option "--bsd". +**************************************************************************** + +' + license="GPLv3 (due to optional libraries; see below)" else - mplibrary='gmp (LGPL)' + license="modified BSD" fi +if test "$gpl" = yes; then isgpl=1; else isgpl=0; fi +AC_DEFINE_UNQUOTED(CVC4_GPL_DEPS, $isgpl, [Whether CVC4 is built with the (optional) GPLed library dependences.]) + CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION" CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION" if test "$CVC4_BUILD_LIBCOMPAT" = no; then @@ -1384,6 +1371,20 @@ if test -n "$CVC4_LANGUAGE_BINDINGS"; then fi fi +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h]) + +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3]) + +AC_OUTPUT + cat <