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 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.
+"--bsd" option before building (which is the default). 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 GLPK, the GNU Linear
Programming Kit, available here:
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 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.
+"--bsd" option before building (which is the default). 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:
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.
+the "--bsd" option before building (which is the default). CVC4 can then be
+used in contexts where you want to license CVC4 under the (modified) BSD
+license.
* 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.
+ is much slower. By default, CVC4 builds with no GPL'ed dependences.
+ However, this is not the best-performing version; for that, you should
+ configure with "--enable-gpl --best", which links against GPL'ed
+ libraries that improve usability and performance. For details on
+ licensing and dependences, see the README file.
* Better automatic handling of output language setting when using CVC4
via API. Previously, the "automatic" language setting was sometimes
(though not always) defaulting to the internal "AST" language; it
AC_DEFUN([CVC4_REWRITE_ARGS_FOR_BUILD_PROFILE],
[m4_divert_push([PARSE_ARGS])dnl
+CVC4_BSD_LICENSED_CODE_ONLY=1
+
+m4_divert_once([HELP_ENABLE], [[
+Licensing and performance options:
+ --bsd disable all GPL dependences (default)
+ --enable-gpl permit GPL dependences, if available
+ --best turn on dependences known to give best performance]])dnl
+
handle_option() {
ac_option="$[]1"
case $ac_option in
- --bsd) ac_option='CVC4_BSD_LICENSED_CODE_ONLY=1' ;;
- -*|*=*) ;;
+ --bsd|--disable-gpl|CVC4_BSD_LICENSED_CODE_ONLY=1)
+ if test "$CVC4_LICENSE_OPTION" = gpl; then AC_ERROR([cannot give both --bsd and --enable-gpl]); fi
+ CVC4_LICENSE_OPTION=bsd
+ ac_option="CVC4_BSD_LICENSED_CODE_ONLY=1"
+ eval $ac_option
+ ;;
+ --enable-gpl|--gpl|CVC4_BSD_LICENSED_CODE_ONLY=0)
+ if test "$CVC4_LICENSE_OPTION" = bsd; then AC_ERROR([cannot give both --bsd and --enable-gpl]); fi
+ CVC4_LICENSE_OPTION=gpl
+ ac_option="CVC4_BSD_LICENSED_CODE_ONLY=0"
+ eval $ac_option
+ ;;
+ --best)
+ # set the best configuration
+ handle_option --with-readline
+ handle_option --with-cln
+ return
+ ;;
+ -*|*=*)
+ ;;
production|production-*|debug|debug-*|competition|competition-*)
# regexp `\?' not supported on Mac OS X
ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'`
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])
+elif test "$with_readline" = check -a "$CVC4_BSD_LICENSED_CODE_ONLY" = 1; then
+ AC_MSG_RESULT([no, using BSD-compatible dependences only])
with_readline=no
else
if test "$with_readline" = check; then
AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
if test $cvc4_use_cln = 2; then
- if test -n "$CVC4_BSD_LICENSED_CODE_ONLY" -o "$with_portfolio" = yes; then
+ if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1 -o "$with_portfolio" = yes; then
cvc4_use_cln=0
cvc4_use_gmp=1
fi
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])
+ if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1; then
+ AC_ERROR([Bad configuration detected: BSD-licensed code only, but also requested GPLed libraries:$gpllibs
+To permit GPL'ed dependences, use the configure flag --enable-gpl])
fi
licensewarn="${licensewarn}"'****************************************************************************
'
license="GPLv3 (due to optional libraries; see below)"
else
+ licensewarn="${licensewarn}Please note that this configuration is NOT built against any GPL'ed
+libraries, so it is covered by the (modified) BSD license. This is,
+however, not the best-performing configuration of CVC4. To build
+against GPL'ed libraries which improve CVC4's performance, re-configure
+with '--best --enable-gpl'.
+
+"
license="modified BSD"
fi
projects / cvc5.git / commitdiff