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.

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 */