From: Morgan Deters Date: Thu, 11 Oct 2012 13:19:09 +0000 (+0000) Subject: Fix wording on GPL in legal notices; also remove an unnecessary source dependence. X-Git-Tag: cvc5-1.0.0~7707 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ee65bafc737d36eaabb871c016e6756aef5bd115;p=cvc5.git Fix wording on GPL in legal notices; also remove an unnecessary source dependence. (this commit was certified error- and warning-free by the test-and-commit script.) --- diff --git a/COPYING b/COPYING index 5c6be04c2..df32895e7 100644 --- a/COPYING +++ b/COPYING @@ -238,10 +238,10 @@ 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". +Please be advised that as this class 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. diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 8e61415e8..89e9ee316 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -39,7 +39,6 @@ #include "expr/node_value.h" #include "context/context.h" #include "util/subrange_bound.h" -#include "util/configuration_private.h" #include "util/tls.h" #include "options/options.h" diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index b93a6dd5e..dec982e32 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -131,10 +131,10 @@ Copyright (C) 2009, 2010, 2011, 2012\n\ ( IS_CLN_BUILD ? "\ 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" : \ +However, CLN, the Class Library for Numbers, is covered by the GPLv3,\n\ +and so this \"combined\" work, CVC4+CLN, is covered by the GPLv3 as well\n\ +Please consult the CVC4 documentation for instructions about building\n\ +without CLN if you want to license CVC4 under the (modified) BSD license.\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\n\ THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE IT AT YOUR OWN RISK.\n" ) )