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)

1 files changed, 11 insertions, 13 deletions

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 {