Fix printing of stats when aborted. (#6362)

This PR improves/fixes printing of statistics when the solver has been aborted, i.e. when we use printSafe(), and a few other minor issues with the new statistics setup.

add toString() methods for TypeConstant, api::Kind to allow for automatic printing by print_safe<>()
improve kindToString() to avoid std::stringstream
fix newlines between statistics in printSafe()
make printing of histograms consistent
make --stats-all, --stats-expert and --stats-every-check automatically enable --stats (and vice versa)

9 files changed, 61 insertions, 33 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 2a8e0f4c7..5c3cbd3f5 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -762,6 +762,12 @@ std::string kindToString(Kind k)
                             : cvc5::kind::kindToString(extToIntKind(k));
 }
 
+const char* toString(Kind k)
+{
+  return k == INTERNAL_KIND ? "INTERNAL_KIND"
+                            : cvc5::kind::toString(extToIntKind(k));
+}
+
 std::ostream& operator<<(std::ostream& out, Kind k)
 {
   switch (k)
diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index 0674a61b0..da1a75499 100644
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -62,23 +62,21 @@ bool isAssociative(::cvc5::Kind k)
   }
 }
 
-std::string kindToString(::cvc5::Kind k)
-{
-  std::stringstream ss;
-  ss << k;
-  return ss.str();
-}
+std::string kindToString(::cvc5::Kind k) { return toString(k); }
 
 }  // namespace kind
 
-std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
-  switch(typeConstant) {
-${type_constant_descriptions}
-  default:
-    out << "UNKNOWN_TYPE_CONSTANT";
-    break;
+const char* toString(TypeConstant tc)
+{
+  switch (tc)
+  {
+    ${type_constant_descriptions}
+    default: return "UNKNOWN_TYPE_CONSTANT";
   }
-  return out;
+}
+std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant)
+{
+  return out << toString(typeConstant);
 }
 
 namespace theory {
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index d5fc3967c..5fa1d99ff 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -92,6 +92,7 @@ struct TypeConstantHashFunction {
   }
 };/* struct TypeConstantHashFunction */
 
+const char* toString(TypeConstant tc);
 std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant);
 
 namespace theory {
diff --git a/src/expr/mkkind b/src/expr/mkkind
index bf0da1073..53e63af6e 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -256,7 +256,7 @@ function register_sort {
 
   type_constant_list="${type_constant_list}  ${id}, /**< ${comment} */
 "
-  type_constant_descriptions="${type_constant_descriptions}  case $id:  out << \"${comment}\"; break;
+  type_constant_descriptions="${type_constant_descriptions}  case $id: return \"${comment}\";
 "
   type_constant_to_theory_id="${type_constant_to_theory_id}  case $id: return $theory_id;
 "
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 9c02a51d1..4ebb71b76 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -85,33 +85,33 @@ header = "options/base_options.h"
 
 [[option]]
   name       = "statistics"
-  smt_name   = "statistics"
+  smt_name   = "stats"
   long       = "stats"
   category   = "common"
   type       = "bool"
-  predicates = ["statsEnabledBuild"]
+  predicates = ["setStats"]
   read_only  = true
   help       = "give statistics on exit"
 
 [[option]]
-  name       = "statisticsExpert"
-  smt_name   = "stats-expert"
-  long       = "stats-expert"
+  name       = "statisticsAll"
+  smt_name   = "stats-all"
+  long       = "stats-all"
   category   = "expert"
   type       = "bool"
-  predicates = ["statsEnabledBuild"]
+  predicates = ["setStats"]
   read_only  = true
-  help       = "print expert (non-public) statistics as well"
+  help       = "print unchanged (defaulted) statistics as well"
 
 [[option]]
-  name       = "statisticsAll"
-  smt_name   = "stats-all"
-  long       = "stats-all"
+  name       = "statisticsExpert"
+  smt_name   = "stats-expert"
+  long       = "stats-expert"
   category   = "expert"
   type       = "bool"
-  predicates = ["statsEnabledBuild"]
+  predicates = ["setStats"]
   read_only  = true
-  help       = "print unchanged (defaulted) statistics as well"
+  help       = "print expert (non-public) statistics as well"
 
 [[option]]
   name       = "statisticsEveryQuery"
@@ -119,7 +119,7 @@ header = "options/base_options.h"
   long       = "stats-every-query"
   category   = "regular"
   type       = "bool"
-  predicates = ["statsEnabledBuild"]
+  predicates = ["setStats"]
   default    = "false"
   read_only  = true
   help       = "in incremental mode, print stats after every satisfiability or validity query"
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 28b8073b9..86ab9c0b3 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -259,15 +259,40 @@ void OptionsHandler::setProduceAssertions(std::string option, bool value)
   options::interactiveMode.set(value);
 }
 
-void OptionsHandler::statsEnabledBuild(std::string option, bool value)
+void OptionsHandler::setStats(const std::string& option, bool value)
 {
 #ifndef CVC5_STATISTICS_ON
-  if(value) {
+  if (value)
+  {
     std::stringstream ss;
     ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support";
     throw OptionException(ss.str());
   }
 #endif /* CVC5_STATISTICS_ON */
+  if (value)
+  {
+    if (option == options::statisticsAll.getName())
+    {
+      d_options->d_holder->statistics = true;
+    }
+    else if (option == options::statisticsEveryQuery.getName())
+    {
+      d_options->d_holder->statistics = true;
+    }
+    else if (option == options::statisticsExpert.getName())
+    {
+      d_options->d_holder->statistics = true;
+    }
+  }
+  else
+  {
+    if (option == options::statistics.getName())
+    {
+      d_options->d_holder->statisticsAll = false;
+      d_options->d_holder->statisticsEveryQuery = false;
+      d_options->d_holder->statisticsExpert = false;
+    }
+  }
 }
 
 void OptionsHandler::threadN(std::string option) {
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index f8b818f0f..6fd9a398b 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -86,7 +86,7 @@ public:
    */
   void setProduceAssertions(std::string option, bool value);
 
-  void statsEnabledBuild(std::string option, bool value);
+  void setStats(const std::string& option, bool value);
 
   unsigned long limitHandler(std::string option, std::string optarg);
   void setResourceWeight(std::string option, std::string optarg);
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index ebd16ebc0..51da36aba 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -97,7 +97,7 @@ void StatisticsRegistry::printSafe(int fd) const
       safe_print(fd, s.first);
       safe_print(fd, " = ");
       s.second->printSafe(fd);
-      safe_print(fd, '\n');
+      safe_print(fd, "\n");
     }
   }
 }
diff --git a/src/util/statistics_value.h b/src/util/statistics_value.h
index 09f429187..950bdd4ab 100644
--- a/src/util/statistics_value.h
+++ b/src/util/statistics_value.h
@@ -154,11 +154,9 @@ struct StatisticHistogramValue : StatisticBaseValue
         {
           safe_print(fd, ", ");
         }
-        safe_print(fd, "(");
         safe_print<Integral>(fd, static_cast<Integral>(i + d_offset));
         safe_print(fd, ": ");
         safe_print<uint64_t>(fd, d_hist[i]);
-        safe_print(fd, ")");
       }
     }
     safe_print(fd, " }");