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() {
#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"
// 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 {
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");
}
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);
}
!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);
}
projects / cvc5.git / commitdiff