Refactor / reimplement statistics (#6162)

This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.

2 files changed, 375 insertions, 33 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 1c62bd4f0..2a8e0f4c7 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -61,25 +61,22 @@
 #include "util/random.h"
 #include "util/result.h"
 #include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
+#include "util/statistics_value.h"
 #include "util/utility.h"
 
 namespace cvc5 {
 namespace api {
 
 /* -------------------------------------------------------------------------- */
-/* Statistics                                                                 */
+/* APIStatistics                                                              */
 /* -------------------------------------------------------------------------- */
 
-struct Statistics
+struct APIStatistics
 {
-  Statistics()
-      : d_consts("api::CONSTANT"), d_vars("api::VARIABLE"), d_terms("api::TERM")
-  {
-  }
-  IntegralHistogramStat<TypeConstant> d_consts;
-  IntegralHistogramStat<TypeConstant> d_vars;
-  IntegralHistogramStat<Kind> d_terms;
+  HistogramStat<TypeConstant> d_consts;
+  HistogramStat<TypeConstant> d_vars;
+  HistogramStat<Kind> d_terms;
 };
 
 /* -------------------------------------------------------------------------- */
@@ -4056,6 +4053,200 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
 }
 
 /* -------------------------------------------------------------------------- */
+/* Statistics                                                                 */
+/* -------------------------------------------------------------------------- */
+
+struct Stat::StatData
+{
+  cvc5::StatExportData data;
+  template <typename T>
+  StatData(T&& t) : data(std::forward<T>(t))
+  {
+  }
+  StatData() : data() {}
+};
+
+Stat::~Stat() {}
+Stat::Stat(const Stat& s)
+    : d_expert(s.d_expert), d_data(std::make_unique<StatData>(s.d_data->data))
+{
+}
+Stat& Stat::operator=(const Stat& s)
+{
+  d_expert = s.d_expert;
+  d_data = std::make_unique<StatData>(s.d_data->data);
+  return *this;
+}
+
+bool Stat::isExpert() const { return d_expert; }
+bool Stat::isDefault() const { return d_default; }
+
+bool Stat::isInt() const
+{
+  return std::holds_alternative<int64_t>(d_data->data);
+}
+int64_t Stat::getInt() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK(isInt()) << "Expected Stat of type int64_t.";
+  return std::get<int64_t>(d_data->data);
+  CVC5_API_TRY_CATCH_END;
+}
+bool Stat::isDouble() const
+{
+  return std::holds_alternative<double>(d_data->data);
+}
+double Stat::getDouble() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK(isDouble()) << "Expected Stat of type double.";
+  return std::get<double>(d_data->data);
+  CVC5_API_TRY_CATCH_END;
+}
+bool Stat::isString() const
+{
+  return std::holds_alternative<std::string>(d_data->data);
+}
+const std::string& Stat::getString() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK(isString()) << "Expected Stat of type std::string.";
+  return std::get<std::string>(d_data->data);
+  CVC5_API_TRY_CATCH_END;
+}
+bool Stat::isHistogram() const
+{
+  return std::holds_alternative<HistogramData>(d_data->data);
+}
+const Stat::HistogramData& Stat::getHistogram() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK(isHistogram()) << "Expected Stat of type histogram.";
+  return std::get<HistogramData>(d_data->data);
+  CVC5_API_TRY_CATCH_END;
+}
+
+Stat::Stat(bool expert, bool def, StatData&& sd)
+    : d_expert(expert),
+      d_default(def),
+      d_data(std::make_unique<StatData>(std::move(sd)))
+{
+}
+
+std::ostream& operator<<(std::ostream& os, const Stat& sv)
+{
+  return cvc5::detail::print(os, sv.d_data->data);
+}
+
+Statistics::BaseType::const_reference Statistics::iterator::operator*() const
+{
+  return d_it.operator*();
+}
+Statistics::BaseType::const_pointer Statistics::iterator::operator->() const
+{
+  return d_it.operator->();
+}
+Statistics::iterator& Statistics::iterator::operator++()
+{
+  do
+  {
+    ++d_it;
+  } while (!isVisible());
+  return *this;
+}
+Statistics::iterator Statistics::iterator::operator++(int)
+{
+  iterator tmp = *this;
+  do
+  {
+    ++d_it;
+  } while (!isVisible());
+  return tmp;
+}
+Statistics::iterator& Statistics::iterator::operator--()
+{
+  do
+  {
+    --d_it;
+  } while (!isVisible());
+  return *this;
+}
+Statistics::iterator Statistics::iterator::operator--(int)
+{
+  iterator tmp = *this;
+  do
+  {
+    --d_it;
+  } while (!isVisible());
+  return tmp;
+}
+bool Statistics::iterator::operator==(const Statistics::iterator& rhs) const
+{
+  return d_it == rhs.d_it;
+}
+bool Statistics::iterator::operator!=(const Statistics::iterator& rhs) const
+{
+  return d_it != rhs.d_it;
+}
+Statistics::iterator::iterator(Statistics::BaseType::const_iterator it,
+                               const Statistics::BaseType& base,
+                               bool expert,
+                               bool def)
+    : d_it(it), d_base(&base), d_showExpert(expert), d_showDefault(def)
+{
+  while (!isVisible())
+  {
+    ++d_it;
+  }
+}
+bool Statistics::iterator::isVisible() const
+{
+  if (d_it == d_base->end()) return true;
+  if (!d_showExpert && d_it->second.isExpert()) return false;
+  if (!d_showDefault && d_it->second.isDefault()) return false;
+  return true;
+}
+
+const Stat& Statistics::get(const std::string& name)
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  auto it = d_stats.find(name);
+  CVC5_API_CHECK(it != d_stats.end())
+      << "No stat with name \"" << name << "\" exists.";
+  return it->second;
+  CVC5_API_TRY_CATCH_END;
+}
+
+Statistics::iterator Statistics::begin(bool expert, bool def) const
+{
+  return iterator(d_stats.begin(), d_stats, expert, def);
+}
+Statistics::iterator Statistics::end() const
+{
+  return iterator(d_stats.end(), d_stats, false, false);
+}
+
+Statistics::Statistics(const StatisticsRegistry& reg)
+{
+  for (const auto& svp : reg)
+  {
+    d_stats.emplace(svp.first,
+                    Stat(svp.second->d_expert,
+                         svp.second->isDefault(),
+                         svp.second->getViewer()));
+  }
+}
+
+std::ostream& operator<<(std::ostream& out, const Statistics& stats)
+{
+  for (const auto& stat : stats)
+  {
+    out << stat.first << " = " << stat.second << std::endl;
+  }
+  return out;
+}
+
+/* -------------------------------------------------------------------------- */
 /* Solver                                                                     */
 /* -------------------------------------------------------------------------- */
 
@@ -4070,12 +4261,7 @@ Solver::Solver(Options* opts)
   d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), d_originalOptions.get()));
   d_smtEngine->setSolver(this);
   d_rng.reset(new Random(d_smtEngine->getOptions()[options::seed]));
-#if CVC5_STATISTICS_ON
-  d_stats.reset(new Statistics());
-  d_smtEngine->getStatisticsRegistry().registerStat(&d_stats->d_consts);
-  d_smtEngine->getStatisticsRegistry().registerStat(&d_stats->d_vars);
-  d_smtEngine->getStatisticsRegistry().registerStat(&d_stats->d_terms);
-#endif
+  resetStatistics();
 }
 
 Solver::~Solver() {}
@@ -4087,27 +4273,29 @@ NodeManager* Solver::getNodeManager(void) const { return d_nodeMgr.get(); }
 
 void Solver::increment_term_stats(Kind kind) const
 {
-#ifdef CVC5_STATISTICS_ON
-  d_stats->d_terms << kind;
-#endif
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    d_stats->d_terms << kind;
+  }
 }
 
 void Solver::increment_vars_consts_stats(const Sort& sort, bool is_var) const
 {
-#ifdef CVC5_STATISTICS_ON
-  const TypeNode tn = sort.getTypeNode();
-  TypeConstant tc = tn.getKind() == cvc5::kind::TYPE_CONSTANT
-                        ? tn.getConst<TypeConstant>()
-                        : LAST_TYPE;
-  if (is_var)
-  {
-    d_stats->d_vars << tc;
-  }
-  else
+  if constexpr (Configuration::isStatisticsBuild())
   {
-    d_stats->d_consts << tc;
+    const TypeNode tn = sort.getTypeNode();
+    TypeConstant tc = tn.getKind() == cvc5::kind::TYPE_CONSTANT
+                          ? tn.getConst<TypeConstant>()
+                          : LAST_TYPE;
+    if (is_var)
+    {
+      d_stats->d_vars << tc;
+    }
+    else
+    {
+      d_stats->d_consts << tc;
+    }
   }
-#endif
 }
 
 /* Split out to avoid nested API calls (problematic with API tracing).        */
@@ -4503,6 +4691,20 @@ bool Solver::isValidInteger(const std::string& s) const
   return true;
 }
 
+void Solver::resetStatistics()
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    d_stats.reset(new APIStatistics{
+        d_smtEngine->getStatisticsRegistry().registerHistogram<TypeConstant>(
+            "api::CONSTANT"),
+        d_smtEngine->getStatisticsRegistry().registerHistogram<TypeConstant>(
+            "api::VARIABLE"),
+        d_smtEngine->getStatisticsRegistry().registerHistogram<Kind>("api::TERM"),
+    });
+  }
+}
+
 /* Helpers for mkTerm checks.                                                 */
 /* .......................................................................... */
 
@@ -6822,6 +7024,11 @@ SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
  */
 Options& Solver::getOptions(void) { return d_smtEngine->getOptions(); }
 
+Statistics Solver::getStatistics() const
+{
+  return Statistics(d_smtEngine->getStatisticsRegistry());
+}
+
 }  // namespace api
 
 }  // namespace cvc5
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 4876caf80..1e0e17e52 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -47,11 +47,13 @@ class TypeNode;
 class Options;
 class Random;
 class Result;
+class StatisticsRegistry;
 
 namespace api {
 
 class Solver;
-struct Statistics;
+class Statistics;
+struct APIStatistics;
 
 /* -------------------------------------------------------------------------- */
 /* Exception                                                                  */
@@ -2259,6 +2261,130 @@ struct CVC4_EXPORT RoundingModeHashFunction
 };
 
 /* -------------------------------------------------------------------------- */
+/* Statistics                                                                 */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * Represents a snapshot of a single statistic value.
+ * A value can be of type int64_t, double, std::string or a histogram
+ * (`std::map<std::string, uint64_t>`).
+ * The value type can be queried (using `isInt`, `isString`, etc.) and
+ * the stored value can be accessed (using `getInt`, `getString`, etc.).
+ */
+class CVC4_EXPORT Stat
+{
+  struct StatData;
+
+ public:
+  friend class Statistics;
+  friend std::ostream& operator<<(std::ostream& os, const Stat& sv);
+  using HistogramData = std::map<std::string, uint64_t>;
+  /** Create from the given value. */
+  Stat() = delete;
+  Stat(const Stat& s);
+  ~Stat();
+  Stat& operator=(const Stat& s);
+
+  /** Is this value intended for experts only? */
+  bool isExpert() const;
+  /** Does this value hold the default value? */
+  bool isDefault() const;
+
+  /** Is this value an integer? */
+  bool isInt() const;
+  /** Return the integer value */
+  int64_t getInt() const;
+  /** Is this value a double? */
+  bool isDouble() const;
+  /** Return the double value */
+  double getDouble() const;
+  /** Is this value an string? */
+  bool isString() const;
+  /** Return the string value */
+  const std::string& getString() const;
+  /** Is this value an histogram? */
+  bool isHistogram() const;
+  /** Return the histogram value */
+  const HistogramData& getHistogram() const;
+
+ private:
+  Stat(bool expert, bool def, StatData&& sd);
+  /** Whether this statistic is only meant for experts */
+  bool d_expert;
+  /** Whether this statistic has the default value */
+  bool d_default;
+  std::unique_ptr<StatData> d_data;
+};
+
+std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC4_EXPORT;
+
+/**
+ * Represents a snapshot of the solver statistics.
+ * Once obtained, an instance of this class is independent of the `Solver`
+ * object: it will not change when the solvers internal statistics do, it
+ * will not be invalidated if the solver is destroyed.
+ * Statistics are generally categorized as public and expert statistics.
+ * Furthermore, statistics may hold the default values and thus be not of
+ * interest.
+ * Iterating on this class (via `begin()` and `end()`) shows only public
+ * statistics that have been set. By passing appropriate flags to `begin()`,
+ * statistics that are expert, unchanged, or both, can be included as well.
+ * A single statistic value is represented as `Stat`.
+ */
+class CVC4_EXPORT Statistics
+{
+ public:
+  friend Solver;
+  using BaseType = std::map<std::string, Stat>;
+
+  /** Custom iterator to hide expert statistics from regular iteration */
+  class iterator
+  {
+   public:
+    friend Statistics;
+    BaseType::const_reference operator*() const;
+    BaseType::const_pointer operator->() const;
+    iterator& operator++();
+    iterator operator++(int);
+    iterator& operator--();
+    iterator operator--(int);
+    bool operator==(const iterator& rhs) const;
+    bool operator!=(const iterator& rhs) const;
+
+   private:
+    iterator(BaseType::const_iterator it,
+             const BaseType& base,
+             bool expert,
+             bool def);
+    bool isVisible() const;
+    BaseType::const_iterator d_it;
+    const BaseType* d_base;
+    bool d_showExpert = false;
+    bool d_showDefault = false;
+  };
+
+  /** Retrieve the statistic with the given name. */
+  const Stat& get(const std::string& name);
+  /**
+   * Begin iteration over the statistics values.
+   * By default, only entries that are public (non-expert) and have been set
+   * are visible while the others are skipped.
+   * With `expert` set to true, expert statistics are shown as well.
+   * With `def` set to true, defaulted statistics are shown as well.
+   */
+  iterator begin(bool expert = false, bool def = false) const;
+  /** end iteration */
+  iterator end() const;
+
+ private:
+  Statistics() = default;
+  Statistics(const StatisticsRegistry& reg);
+  /** Internal data */
+  BaseType d_stats;
+};
+std::ostream& operator<<(std::ostream& out, const Statistics& stats) CVC4_EXPORT;
+
+/* -------------------------------------------------------------------------- */
 /* Solver                                                                     */
 /* -------------------------------------------------------------------------- */
 
@@ -3680,9 +3806,18 @@ class CVC4_EXPORT Solver
   // the driver level. !!!
   Options& getOptions(void);
 
+  /**
+   * Returns a snapshot of the current state of the statistic values of this
+   * solver. The returned object is completely decoupled from the solver and
+   * will not change when the solver is used again.
+   */
+  Statistics getStatistics() const;
+
  private:
   /** @return the node manager of this solver */
   NodeManager* getNodeManager(void) const;
+  /** Reset the API statistics */
+  void resetStatistics();
 
   /** Helper to check for API misuse in mkOp functions. */
   void checkMkTerm(Kind kind, uint32_t nchildren) const;
@@ -3779,7 +3914,7 @@ class CVC4_EXPORT Solver
   /** The node manager of this solver. */
   std::unique_ptr<NodeManager> d_nodeMgr;
   /** The statistics collected on the Api level. */
-  std::unique_ptr<Statistics> d_stats;
+  std::unique_ptr<APIStatistics> d_stats;
   /** The SMT engine of this solver. */
   std::unique_ptr<SmtEngine> d_smtEngine;
   /** The random number generator of this solver. */