New statistics registry (#6210)

This PR adds the next part of the new statistics setup: the registry.
The new statistics registry owns the actual data and only issues proxy objects that can be used to modify the internally stored data.
Once we replace the old statistics setup, the files should be renamed from statistics_reg.* to statistics_registry.*.

7 files changed, 468 insertions, 5 deletions

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index cab4332b8..17050cd06 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -86,18 +86,40 @@ header = "options/base_options.h"
 [[option]]
   name       = "statistics"
   smt_name   = "statistics"
-  category   = "common"
   long       = "stats"
+  category   = "common"
   type       = "bool"
   predicates = ["statsEnabledBuild"]
   read_only  = true
   help       = "give statistics on exit"
 
 [[option]]
-  name       = "statsEveryQuery"
-  category   = "regular"
+  name       = "statisticsExpert"
+  smt_name   = "stats-expert"
+  long       = "stats-expert"
+  category   = "expert"
+  type       = "bool"
+  predicates = ["statsEnabledBuild"]
+  read_only  = true
+  help       = "print expert (non-public) statistics as well"
+
+[[option]]
+  name       = "statisticsUnset"
+  smt_name   = "stats-unset"
+  long       = "stats-unset"
+  category   = "expert"
+  type       = "bool"
+  predicates = ["statsEnabledBuild"]
+  read_only  = true
+  help       = "print unset statistics as well"
+
+[[option]]
+  name       = "statisticsEveryQuery"
+  smt_name   = "stats-every-query"
   long       = "stats-every-query"
+  category   = "regular"
   type       = "bool"
+  predicates = ["statsEnabledBuild"]
   default    = "false"
   read_only  = true
   help       = "in incremental mode, print stats after every satisfiability or validity query"
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 1bccc283f..3ccf3b744 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -126,11 +126,11 @@ bool Options::getSemanticChecks() const{
 
 bool Options::getStatistics() const{
   // statsEveryQuery enables stats
-  return (*this)[options::statistics] || (*this)[options::statsEveryQuery];
+  return (*this)[options::statistics] || (*this)[options::statisticsEveryQuery];
 }
 
 bool Options::getStatsEveryQuery() const{
-  return (*this)[options::statsEveryQuery];
+  return (*this)[options::statisticsEveryQuery];
 }
 
 bool Options::getStatsHideZeros() const{
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 2595ab4c0..4bc6da1ae 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -62,6 +62,10 @@ libcvc4_add_sources(
   smt2_quote_string.h
   statistics.cpp
   statistics.h
+  statistics_public.cpp
+  statistics_public.h
+  statistics_reg.cpp
+  statistics_reg.h
   statistics_registry.cpp
   statistics_registry.h
   statistics_value.cpp
diff --git a/src/util/statistics_public.cpp b/src/util/statistics_public.cpp
new file mode 100644
index 000000000..dd488c192
--- /dev/null
+++ b/src/util/statistics_public.cpp
@@ -0,0 +1,28 @@
+/*********************                                                        */
+/*! \file statistics_public.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Registration of public statistics
+ **
+ ** Registration and documentation for all public statistics.
+ **/
+
+#include "util/statistics_public.h"
+
+#include "util/statistics_registry.h"
+
+namespace cvc5 {
+
+void registerPublicStatistics(StatisticsRegistry& reg)
+{
+
+}
+
+}  // namespace cvc5
diff --git a/src/util/statistics_public.h b/src/util/statistics_public.h
new file mode 100644
index 000000000..c2d054f00
--- /dev/null
+++ b/src/util/statistics_public.h
@@ -0,0 +1,33 @@
+/*********************                                                        */
+/*! \file statistics_public.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Registration of public statistics
+ **
+ ** Registration and documentation for all public statistics.
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef CVC4__UTIL__STATISTICS_PUBLIC_H
+#define CVC4__UTIL__STATISTICS_PUBLIC_H
+
+namespace cvc5 {
+
+class StatisticsRegistry;
+
+/**
+ * Preregisters all public (non-expert) statistics.
+ */
+void registerPublicStatistics(StatisticsRegistry& reg);
+
+}  // namespace cvc5
+
+#endif
diff --git a/src/util/statistics_reg.cpp b/src/util/statistics_reg.cpp
new file mode 100644
index 000000000..efb564c74
--- /dev/null
+++ b/src/util/statistics_reg.cpp
@@ -0,0 +1,143 @@
+/*********************                                                        */
+/*! \file statistics_reg.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Central statistics registry.
+ **
+ ** The StatisticsRegistry that issues statistic proxy objects.
+ **/
+
+#include "util/statistics_reg.h"
+
+#include "options/base_options.h"
+#include "util/statistics_public.h"
+
+namespace cvc5 {
+
+StatisticsRegistry::StatisticsRegistry(bool registerPublic)
+{
+  if (registerPublic)
+  {
+    registerPublicStatistics(*this);
+  }
+}
+
+AverageStat StatisticsRegistry::registerAverage(const std::string& name,
+                                                bool expert)
+{
+  return registerStat<AverageStat>(name, expert);
+}
+IntStat StatisticsRegistry::registerInt(const std::string& name, bool expert)
+{
+  return registerStat<IntStat>(name, expert);
+}
+TimerStat StatisticsRegistry::registerTimer(const std::string& name,
+                                            bool expert)
+{
+  return registerStat<TimerStat>(name, expert);
+}
+
+void StatisticsRegistry::storeSnapshot()
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    d_lastSnapshot = std::make_unique<Snapshot>();
+    for (const auto& s : d_stats)
+    {
+      if (!options::statisticsExpert() && s.second->d_expert) continue;
+      if (!options::statisticsUnset() && !s.second->hasValue()) continue;
+      d_lastSnapshot->emplace(
+          s.first,
+          s.second->hasValue() ? s.second->getViewer() : StatExportData{});
+    }
+  }
+}
+
+StatisticBaseValue* StatisticsRegistry::get(const std::string& name) const
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    auto it = d_stats.find(name);
+    if (it == d_stats.end()) return nullptr;
+    return it->second.get();
+  }
+  return nullptr;
+}
+
+void StatisticsRegistry::print(std::ostream& os) const
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    for (const auto& s : d_stats)
+    {
+      if (!options::statisticsExpert() && s.second->d_expert) continue;
+      if (!options::statisticsUnset() && !s.second->hasValue()) continue;
+      os << s.first << " = " << *s.second << std::endl;
+    }
+  }
+}
+
+void StatisticsRegistry::printSafe(int fd) const
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    for (const auto& s : d_stats)
+    {
+      if (!options::statisticsExpert() && s.second->d_expert) continue;
+      if (!options::statisticsUnset() && !s.second->hasValue()) continue;
+
+      safe_print(fd, s.first);
+      safe_print(fd, " = ");
+      if (s.second->hasValue())
+        s.second->printSafe(fd);
+      else
+        safe_print(fd, "<unset>");
+      safe_print(fd, '\n');
+    }
+  }
+}
+void StatisticsRegistry::printDiff(std::ostream& os) const
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    if (!d_lastSnapshot)
+    {
+      // we have no snapshot, print as usual
+      print(os);
+      return;
+    }
+    for (const auto& s : d_stats)
+    {
+      if (!options::statisticsExpert() && s.second->d_expert) continue;
+      if (!options::statisticsUnset() && !s.second->hasValue()) continue;
+      auto oldit = d_lastSnapshot->find(s.first);
+      if (oldit == d_lastSnapshot->end())
+      {
+        // not present in the snapshot
+        os << s.first << " = " << *s.second << " (was <unset>)" << std::endl;
+      }
+      else if (oldit->second != s.second->getViewer())
+      {
+        // present in the snapshow, print old value
+        os << s.first << " = " << *s.second << " (was ";
+        detail::print(os, oldit->second);
+        os << ")" << std::endl;
+      }
+    }
+  }
+}
+
+std::ostream& operator<<(std::ostream& os, const StatisticsRegistry& sr)
+{
+  sr.print(os);
+  return os;
+}
+
+}  // namespace cvc5
diff --git a/src/util/statistics_reg.h b/src/util/statistics_reg.h
new file mode 100644
index 000000000..e020a05b4
--- /dev/null
+++ b/src/util/statistics_reg.h
@@ -0,0 +1,233 @@
+/*********************                                                        */
+/*! \file statistics_reg.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Central statistics registry.
+ **
+ ** The StatisticsRegistry that issues statistic proxy objects.
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef CVC4__UTIL__STATISTICS_REG_H
+#define CVC4__UTIL__STATISTICS_REG_H
+
+#include <iostream>
+#include <map>
+#include <memory>
+#include <typeinfo>
+
+#include "base/check.h"
+#include "util/statistics_stats.h"
+#include "util/statistics_value.h"
+
+namespace cvc5 {
+
+struct StatisticBaseValue;
+
+/**
+ * The central registry for statistics.
+ * Internally stores statistic data objects and issues corresponding proxy
+ * objects to modules that want to expose statistics.
+ * Provides registration methods (e.g. `registerAverage` or
+ * `registerHistogram<T>`) that return the proxy object.
+ * The different statistics are explained in more detail in statistics_stats.h
+ *
+ * Every statistic is identified by a name. If a statistic with the given
+ * name is already registered, the registry issues another proxy object
+ * for that name using the same data it already holds for this name.
+ * While this makes perfect sense for most statistic types, it may lead to
+ * unexpected (though not undefined) behaviour for others. For a reference
+ * statistic, for example, the internal data will simply point to the object
+ * registered last.
+ * Note that the type of the re-registered statistic must always match
+ * the type of the previously registered statistic with the same name.
+ *
+ * We generally distinguish between public (non-expert) and private (expert)
+ * statistics. By default, `--stats` only shows public statistics. Private
+ * ones are printed as well if `--all-statistics` is set.
+ * All registration methods have a trailing argument `expert`, defaulting to
+ * true.
+ *
+ * If statistics are disabled entirely (i.e. the cmake option
+ * `ENABLE_STATISTICS` is not set), the registry still issues proxy objects
+ * that can be used normally.
+ * However, no data is stored in the registry and the modification functions
+ * of the proxy objects do nothing.
+ */
+class StatisticsRegistry
+{
+ public:
+  friend std::ostream& operator<<(std::ostream& os,
+                                  const StatisticsRegistry& sr);
+
+  using Snapshot = std::map<std::string, StatExportData>;
+
+  /**
+   * If `registerPublic` is true, all statistics that are public are
+   * pre-registered as such. This argument mostly exists so that unit tests
+   * can disable this pre-registration.
+   */
+  StatisticsRegistry(bool registerPublic = true);
+
+  /** Register a new running average statistic for `name` */
+
+  AverageStat registerAverage(const std::string& name, bool expert = true);
+  /** Register a new histogram statistic for `name` */
+  template <typename T>
+  HistogramStat<T> registerHistogram(const std::string& name,
+                                     bool expert = true)
+  {
+    return registerStat<HistogramStat<T>>(name, expert);
+  }
+
+  /** Register a new integer statistic for `name` */
+  IntStat registerInt(const std::string& name, bool expert = true);
+
+  /** Register a new reference statistic for `name` */
+  template <typename T>
+  ReferenceStat<T> registerReference(const std::string& name,
+                                     bool expert = true)
+  {
+    return registerStat<ReferenceStat<T>>(name, expert);
+  }
+  /**
+   * Register a new reference statistic for `name` and initialize it to
+   * refer to `t`.
+   */
+  template <typename T>
+  ReferenceStat<T> registerReference(const std::string& name,
+                                     const T& t,
+                                     bool expert = true)
+  {
+    ReferenceStat<T> res = registerStat<ReferenceStat<T>>(name, expert);
+    res.set(t);
+    return res;
+  }
+
+  /**
+   * Register a new container size statistic for `name` and initialize it
+   * to refer to `t`.
+   */
+  template <typename T>
+  SizeStat<T> registerSize(const std::string& name,
+                           const T& t,
+                           bool expert = true)
+  {
+    SizeStat<T> res = registerStat<SizeStat<T>>(name, expert);
+    res.set(t);
+    return res;
+  }
+
+  /** Register a new timer statistic for `name` */
+  TimerStat registerTimer(const std::string& name, bool expert = true);
+
+  /** Register a new value statistic for `name`. */
+  template <typename T>
+  ValueStat<T> registerValue(const std::string& name, bool expert = true)
+  {
+    return registerStat<ValueStat<T>>(name, expert);
+  }
+
+  /** Register a new value statistic for `name` and set it to `init`. */
+  template <typename T>
+  ValueStat<T> registerValue(const std::string& name,
+                             const T& init,
+                             bool expert = true)
+  {
+    ValueStat<T> res = registerStat<ValueStat<T>>(name, expert);
+    res.set(init);
+    return res;
+  }
+
+  /** begin iteration */
+  auto begin() const { return d_stats.begin(); }
+  /** end iteration */
+  auto end() const { return d_stats.end(); }
+
+  /**
+   * Store the current state of the statistics to allow for printing a diff
+   * using `printDiff`.
+   */
+  void storeSnapshot();
+
+  /**
+   * Obtain a single statistic by name. Returns nullptr if no statistic has
+   * been registered for this name.
+   */
+  StatisticBaseValue* get(const std::string& name) const;
+
+  /**
+   * Print all statistics to the given output stream.
+   */
+  void print(std::ostream& os) const;
+  /**
+   * Print all statistics in a safe manner to the given file descriptor.
+   */
+  void printSafe(int fd) const;
+  /**
+   * Print all statistics as a diff to the last snapshot that was stored by
+   * calling `storeSnapshot`.
+   */
+  void printDiff(std::ostream& os) const;
+
+ private:
+  /**
+   * Helper method to register a new statistic.
+   * If the name was already used, a new proxy object is created.
+   * We check whether the type matches the type of the originally registered
+   * statistic using `typeid`.
+   */
+  template <typename Stat>
+  Stat registerStat(const std::string& name, bool expert)
+  {
+    if constexpr (Configuration::isStatisticsBuild())
+    {
+      auto it = d_stats.find(name);
+      if (it == d_stats.end())
+      {
+        it = d_stats.emplace(name, std::make_unique<typename Stat::stat_type>())
+                 .first;
+        it->second->d_expert = expert;
+      }
+      auto* ptr = it->second.get();
+      Assert(typeid(*ptr) == typeid(typename Stat::stat_type))
+          << "Statistic value " << name
+          << " was registered again with a different type.";
+      it->second->d_expert = it->second->d_expert && expert;
+      return Stat(static_cast<typename Stat::stat_type*>(ptr));
+    }
+    return Stat(nullptr);
+  }
+
+  /**
+   * Holds (and owns) all statistic values, indexed by the name they were
+   * registered for.
+   */
+  std::map<std::string, std::unique_ptr<StatisticBaseValue>> d_stats;
+
+  /**
+   * Holds a snapshot of the statistic values as StatExportData.
+   * The current state can be saved to this snapshot using `storeSnapshot`,
+   * which is then used in the next call to `printDiff`, but the data is not
+   * exposed otherwise.
+   * As this snapshot is only used by `printDiff`, which honors the relevant
+   * options `--stats-expert` and `--stats-unset`, the snapshot is populated
+   * by `storeSnapshot` to contain only those values that would be printed.
+   */
+  std::unique_ptr<Snapshot> d_lastSnapshot;
+};
+
+/** Calls `sr.print(os)`. */
+std::ostream& operator<<(std::ostream& os, const StatisticsRegistry& sr);
+
+}  // namespace cvc5
+
+#endif