From: Aina Niemetz Date: Tue, 10 Oct 2017 22:36:09 +0000 (-0700) Subject: Add copyright information. (#1201) X-Git-Tag: cvc5-1.0.0~5568 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dd979fcdb5a952462e4d6702999b5354de5a7be8;p=cvc5.git 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. --- 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 */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index cad662d90..8ffb47e40 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -304,7 +304,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") << " assertions:" << (Configuration::isAssertionBuild() ? "on" : "off") - << endl; + << endl << endl; + Message() << Configuration::copyright() << endl; } if(replayParser) { // have the replay parser use the declarations input interactively diff --git a/src/options/main_options b/src/options/main_options index 0fa799df2..e47f55746 100644 --- a/src/options/main_options +++ b/src/options/main_options @@ -15,6 +15,9 @@ common-option help -h --help/ bool common-option - --show-config void :handler showConfiguration show CVC4 static configuration +common-option - --copyright void :handler copyright + show CVC4 copyright information + option - --show-debug-tags void :handler showDebugTags show all available tags for debugging option - --show-trace-tags void :handler showTraceTags diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 9adff0d3d..a3617ef6f 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -23,11 +23,13 @@ #include "cvc4autoconfig.h" #include "base/configuration.h" +#include "base/configuration_private.h" #include "base/cvc4_assert.h" #include "base/exception.h" #include "base/modal_exception.h" #include "base/output.h" #include "lib/strtok_r.h" +#include "gmp.h" #include "options/arith_heuristic_pivot_rule.h" #include "options/arith_propagation_mode.h" #include "options/arith_unate_lemma_mode.h" @@ -1368,67 +1370,96 @@ void OptionsHandler::notifySetPrintExprTypes(std::string option) { // main/options_handlers.h + +static void print_config (const char * str, std::string config) { + std::string s(str); + unsigned sz = 14; + if (s.size() < sz) s.resize(sz, ' '); + std::cout << s << ": " << config << std::endl; +} + +static void print_config_cond (const char * str, bool cond = false) { + print_config(str, cond ? "yes" : "no"); +} + +void OptionsHandler::copyright(std::string option) { + std::cout << Configuration::copyright() << std::endl; + exit(0); +} + void OptionsHandler::showConfiguration(std::string option) { - fputs(Configuration::about().c_str(), stdout); - printf("\n"); - printf("version : %s\n", Configuration::getVersionString().c_str()); + std::cout << Configuration::about() << std::endl; + + print_config ("version", Configuration::getVersionString()); + if(Configuration::isGitBuild()) { const char* branchName = Configuration::getGitBranchName(); - if(*branchName == '\0') { - branchName = "-"; - } - printf("scm : git [%s %s%s]\n", - branchName, - std::string(Configuration::getGitCommit()).substr(0, 8).c_str(), - Configuration::hasGitModifications() ? - " (with modifications)" : ""); + if(*branchName == '\0') { branchName = "-"; } + std::stringstream ss; + ss << "git [" + << branchName << " " + << std::string(Configuration::getGitCommit()).substr(0, 8) + << (Configuration::hasGitModifications() ? " (with modifications)" : "") + << "]"; + print_config("scm", ss.str()); } else if(Configuration::isSubversionBuild()) { - printf("scm : svn [%s r%u%s]\n", - Configuration::getSubversionBranchName(), - Configuration::getSubversionRevision(), - Configuration::hasSubversionModifications() ? - " (with modifications)" : ""); + std::stringstream ss; + ss << "svn [" + << Configuration::getSubversionBranchName() << " r" + << Configuration::getSubversionRevision() + << (Configuration::hasSubversionModifications() + ? " (with modifications)" : "") + << "]"; + print_config("scm", ss.str()); } else { - printf("scm : no\n"); + print_config_cond("scm", false); } - printf("\n"); - printf("library : %u.%u.%u\n", - Configuration::getVersionMajor(), - Configuration::getVersionMinor(), - Configuration::getVersionRelease()); - printf("\n"); - printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no"); - printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no"); - printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no"); - printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no"); - printf("dumping : %s\n", Configuration::isDumpingBuild() ? "yes" : "no"); - printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no"); - printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no"); - printf("proof : %s\n", Configuration::isProofBuild() ? "yes" : "no"); - printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no"); - printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no"); - printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no"); - printf("\n"); - printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no"); - printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no"); - printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no"); - printf("cryptominisat: %s\n", Configuration::isBuiltWithCryptominisat() ? "yes" : "no"); - printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no"); - printf("lfsc : %s\n", Configuration::isBuiltWithLfsc() ? "yes" : "no"); - printf("readline : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no"); - printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); + + std::cout << std::endl; + + std::stringstream ss; + ss << Configuration::getVersionMajor() << "." + << Configuration::getVersionMinor() << "." + << Configuration::getVersionRelease(); + print_config("library", ss.str()); + + std::cout << std::endl; + + print_config_cond("debug code", Configuration::isDebugBuild()); + print_config_cond("statistics", Configuration::isStatisticsBuild()); + print_config_cond("replay", Configuration::isReplayBuild()); + print_config_cond("tracing", Configuration::isTracingBuild()); + print_config_cond("dumping", Configuration::isDumpingBuild()); + print_config_cond("muzzled", Configuration::isMuzzledBuild()); + print_config_cond("assertions", Configuration::isAssertionBuild()); + print_config_cond("proof", Configuration::isProofBuild()); + print_config_cond("coverage", Configuration::isCoverageBuild()); + print_config_cond("profiling", Configuration::isProfilingBuild()); + print_config_cond("competition", Configuration::isCompetitionBuild()); + + std::cout << std::endl; + + print_config_cond("abc", Configuration::isBuiltWithAbc()); + print_config_cond("cln", Configuration::isBuiltWithCln()); + print_config_cond("glpk", Configuration::isBuiltWithGlpk()); + print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat()); + print_config_cond("gmp", Configuration::isBuiltWithGmp()); + print_config_cond("lfsc", Configuration::isBuiltWithLfsc()); + print_config_cond("readline", Configuration::isBuiltWithReadline()); + print_config_cond("tls", Configuration::isBuiltWithTlsSupport()); + exit(0); } void OptionsHandler::showDebugTags(std::string option) { if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { - printf("available tags:"); + std::cout << "available tags:"; unsigned ntags = Configuration::getNumDebugTags(); char const* const* tags = Configuration::getDebugTags(); for(unsigned i = 0; i < ntags; ++ i) { - printf(" %s", tags[i]); + std::cout << tags[i]; } - printf("\n"); + std::cout << std::endl; } else if(! Configuration::isDebugBuild()) { throw OptionException("debug tags not available in non-debug builds"); } else { @@ -1439,13 +1470,13 @@ void OptionsHandler::showDebugTags(std::string option) { void OptionsHandler::showTraceTags(std::string option) { if(Configuration::isTracingBuild()) { - printf("available tags:"); + std::cout << "available tags:"; unsigned ntags = Configuration::getNumTraceTags(); char const* const* tags = Configuration::getTraceTags(); for (unsigned i = 0; i < ntags; ++ i) { - printf(" %s", tags[i]); + std::cout << tags[i]; } - printf("\n"); + std::cout << std::endl; } else { throw OptionException("trace tags not available in non-tracing build"); } @@ -1530,13 +1561,13 @@ void OptionsHandler::addTraceTag(std::string option, std::string optarg) { if(!Configuration::isTraceTag(optarg.c_str())) { if(optarg == "help") { - printf("available tags:"); + std::cout << "available tags:"; unsigned ntags = Configuration::getNumTraceTags(); char const* const* tags = Configuration::getTraceTags(); for(unsigned i = 0; i < ntags; ++ i) { - printf(" %s", tags[i]); + std::cout << tags[i]; } - printf("\n"); + std::cout << std::endl; exit(0); } @@ -1556,13 +1587,13 @@ void OptionsHandler::addDebugTag(std::string option, std::string optarg) { !Configuration::isTraceTag(optarg.c_str())) { if(optarg == "help") { - printf("available tags:"); + std::cout << "available tags:"; unsigned ntags = Configuration::getNumDebugTags(); char const* const* tags = Configuration::getDebugTags(); for(unsigned i = 0; i < ntags; ++ i) { - printf(" %s", tags[i]); + std::cout << tags[i]; } - printf("\n"); + std::cout << std::endl; exit(0); } diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 923a87d3a..e534d8e58 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -171,6 +171,7 @@ public: void notifySetPrintExprTypes(std::string option); /* main/options_handlers.h */ + void copyright(std::string option); void showConfiguration(std::string option); void showDebugTags(std::string option); void showTraceTags(std::string option);