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)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 2a8e0f4c7cb4187a4475bd563620811e432918db..5c3cbd3f553ee89a20c13e5e9f8a9c75cf69537a 100644 (file)
--- 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 0674a61b0a3b3b2cc5cecd7f1294d6118fcd06ba..da1a75499cd39f85b4c0eb1b2f1b466f1417c911 100644 (file)
--- 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 d5fc3967c2eac08f435727a28f225cb048ece844..5fa1d99fff9ee63050de14b8af2b1fb469bf8bdd 100644 (file)
--- 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 bf0da1073653620d3d0d39b3874d65906b4c525a..53e63af6e831cc3f212b0104cdc4d28348aa933e 100755 (executable)
--- 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 9c02a51d18055d3ceb80a75ee8681478ce542166..4ebb71b769d1315f308a2fceb8729c21ac3a1f6e 100644 (file)
--- 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 28b8073b97d5e764c4865f05d50f1cc080dee06d..86ab9c0b3df28b825c32a5afac59c5fe41841029 100644 (file)
--- 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 f8b818f0fb475549625572c82727cd244f80f5bd..6fd9a398ba7ee3635c2b80de0e4e2f9d7f056083 100644 (file)
--- 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 ebd16ebc0c218b94c070ffd6370bbcec2ca341b9..51da36aba6d49b3ea1daeece3fa473bf2ab0e9e7 100644 (file)
--- 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 09f42918767821c718aaf83829d3c0042c2063b2..950bdd4ab1aadc67745d318c7f213ea2ef4e4ba3 100644 (file)
--- 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, " }");