diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-10-10 15:36:09 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-10 15:36:09 -0700 |
commit | dd979fcdb5a952462e4d6702999b5354de5a7be8 (patch) | |
tree | cb4d590f0cba3ec2408633d7e2c70808167b2ad2 /src/base | |
parent | b7d0c09bd12b9d0f46deab199714ce3441206d7f (diff) |
Add copyright information. (#1201)
This adds option --copyright which displays copyright information for CVC4. It further extends --show-config with copyright information and adds a banner with copyright information in interactive mode.
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/configuration.cpp | 96 | ||||
-rw-r--r-- | src/base/configuration.h | 2 | ||||
-rw-r--r-- | src/base/configuration_private.h | 28 |
3 files changed, 97 insertions, 29 deletions
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 196290b53..7e7da1500 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -110,8 +110,102 @@ std::string Configuration::getVersionExtra() { return CVC4_EXTRAVERSION; } +std::string Configuration::copyright() { + std::stringstream ss; + ss << "Copyright (c) 2009-2017 by the authors and their institutional\n" + << "affiliations listed at http://cvc4.cs.stanford.edu/authors\n\n"; + + if (Configuration::licenseIsGpl()) { + ss << "This build of CVC4 uses GPLed libraries, and is thus covered by\n" + << "the GNU General Public License (GPL) version 3. Versions of CVC4\n" + << "are available that are covered by the (modified) BSD license. If\n" + << "you want to license CVC4 under this license, please configure CVC4\n" + << "with the \"--bsd\" option before building from sources.\n\n"; + } else { + ss << "CVC4 is open-source and is covered by the BSD license (modified)." + << "\n\n"; + } + + ss << "THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES.\n" + << "USE AT YOUR OWN RISK.\n\n"; + + ss << "CVC4 incorporates code from ANTLR3 (http://www.antlr.org).\n" + << "See licenses/antlr3-LICENSE for copyright and licensing information." + << "\n\n"; + + if (Configuration::isBuiltWithAbc() + || Configuration::isBuiltWithLfsc()) { + ss << "This version of CVC4 is linked against the following non-(L)GPL'ed\n" + << "third party libraries.\n\n"; + if (Configuration::isBuiltWithAbc()) { + ss << " ABC - A System for Sequential Synthesis and Verification\n" + << " See http://bitbucket.org/alanmi/abc for copyright and\n" + << " licensing information.\n\n"; + } + if (Configuration::isBuiltWithLfsc()) { + ss << " LFSC Proof Checker\n" + << " See http://github.com/CVC4/LFSC for copyright and\n" + << " licensing information.\n\n"; + } + } + + if (Configuration::isBuiltWithGmp() + || Configuration::isBuiltWithCryptominisat()) { + ss << "This version of CVC4 is linked against the following third party\n" + << "libraries covered by the LGPLv3 license.\n" + << "See licenses/lgpl-3.0.txt for more information.\n\n"; + if (Configuration::isBuiltWithGmp()) { + ss << " GMP - Gnu Multi Precision Arithmetic Library\n" + << " See http://gmplib.org for copyright information.\n\n"; + } + if (Configuration::isBuiltWithCryptominisat()) { + ss << " CryptoMiniSat - An Advanced SAT Solver\n" + << " See http://github.com/msoos/cryptominisat for copyright " + << "information.\n\n"; + } + } + + if (Configuration::isBuiltWithCln() + || Configuration::isBuiltWithGlpk () + || Configuration::isBuiltWithReadline()) { + ss << "This version of CVC4 is linked against the following third party\n" + << "libraries covered by the GPLv3 license.\n" + << "See licenses/gpl-3.0.txt for more information.\n\n"; + if (Configuration::isBuiltWithCln()) { + ss << " CLN - Class Library for Numbers\n" + << " See http://www.ginac.de/CLN for copyright information.\n\n"; + } + if (Configuration::isBuiltWithGlpk()) { + ss << " glpk-cut-log - a modified version of GPLK, " + << "the GNU Linear Programming Kit\n" + << " See http://github.com/timothy-king/glpk-cut-log for copyright" + << "information\n\n"; + } + if (Configuration::isBuiltWithReadline()) { + ss << " GNU Readline\n" + << " See http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html\n" + << " for copyright information.\n\n"; + } + } + + ss << "See the file COPYING (distributed with the source code, and with\n" + << "all binaries) for the full CVC4 copyright, licensing, and (lack of)\n" + << "warranty information.\n"; + return ss.str(); +} + std::string Configuration::about() { - return CVC4_ABOUT_STRING; + std::stringstream ss; + ss << "This is CVC4 version " << CVC4_RELEASE_STRING; + if (Configuration::isGitBuild()) { + ss << " [" << Configuration::getGitId() << "]"; + } else if (CVC4::Configuration::isSubversionBuild()) { + ss << " [" << Configuration::getSubversionId() << "]"; + } + ss << "\ncompiled with " << Configuration::getCompiler() + << "\non " << Configuration::getCompiledDateTime() << "\n\n"; + ss << Configuration::copyright (); + return ss.str(); } bool Configuration::licenseIsGpl() { diff --git a/src/base/configuration.h b/src/base/configuration.h index 31c7b6547..29f23ab18 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -81,6 +81,8 @@ public: static std::string getVersionExtra(); + static std::string copyright(); + static std::string about(); static bool licenseIsGpl(); diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 472113c2e..eba45cc61 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -144,34 +144,6 @@ namespace CVC4 { # define USING_TLS false #endif /* TLS */ -#define CVC4_ABOUT_STRING ( ::std::string("\ -This is CVC4 version " CVC4_RELEASE_STRING ) + \ - ( ::CVC4::Configuration::isGitBuild() \ - ? ( ::std::string(" [") + ::CVC4::Configuration::getGitId() + "]" ) \ - : \ - ( ::CVC4::Configuration::isSubversionBuild() \ - ? ( ::std::string(" [") + ::CVC4::Configuration::getSubversionId() + "]" ) \ - : ::std::string("") \ - )) + "\n\ -compiled with " + ::CVC4::Configuration::getCompiler() + "\n\ -on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\ -Copyright (c) 2009-2017\n\ -by the authors and their institutional affiliations listed at \n\ -http://cvc4.cs.stanford.edu/authors\n\n" + \ - ( IS_GPL_BUILD ? "\ -This build of CVC4 uses GPLed libraries, and is thus covered by the GNU\n\ -General Public License (GPL) version 3. Versions of CVC4 are available\n\ -that are covered by the (modified) BSD license. If you want to license\n\ -CVC4 under this license, please configure CVC4 with the \"--bsd\" option\n\ -before building from sources.\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 AT YOUR OWN RISK.\n\n\ -See the file COPYING (distributed with the source code, and with all binaries)\n\ -for the full CVC4 copyright, licensing, and (lack of) warranty information.\n" ) - }/* CVC4 namespace */ #endif /* __CVC4__CONFIGURATION_PRIVATE_H */ |