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.

1 files changed, 86 insertions, 55 deletions

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);
       }