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.

7 files changed, 189 insertions, 85 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 */
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);