Add utility classes for new statistics (#6178)

This PR introduces two new sets of classes used for the new statistics setup.
The first set are the statistic values that hold the actual data and will live in the new statistics registry itself.
The second set are proxy objects: they only hold a pointer to the value classes and implement all the modifiers.

The code is not used yet, but replaces the code in the stats_* files in a subsequent PR.

5 files changed, 1005 insertions, 0 deletions

diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 2ca6ab605..2595ab4c0 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -64,6 +64,8 @@ libcvc4_add_sources(
   statistics.h
   statistics_registry.cpp
   statistics_registry.h
+  statistics_value.cpp
+  statistics_value.h
   stats_base.cpp
   stats_base.h
   stats_histogram.h
diff --git a/src/util/statistics_stats.cpp b/src/util/statistics_stats.cpp
new file mode 100644
index 000000000..8aa686e5d
--- /dev/null
+++ b/src/util/statistics_stats.cpp
@@ -0,0 +1,135 @@
+/*********************                                                        */
+/*! \file statistics_stats.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 Basic statistics representation
+ **
+ ** The basic statistics classes.
+ **/
+
+#include "util/statistics_stats.h"
+
+#include "base/check.h"
+#include "util/statistics_value.h"
+
+namespace cvc5 {
+
+AverageStat& AverageStat::operator<<(double v)
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    d_data->d_sum += v;
+    d_data->d_count++;
+  }
+  return *this;
+}
+
+IntStat& IntStat::operator=(int64_t val)
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    d_data->d_value = val;
+  }
+  return *this;
+}
+
+IntStat& IntStat::operator++()
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    d_data->d_value++;
+  }
+  return *this;
+}
+
+IntStat& IntStat::operator++(int)
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    d_data->d_value++;
+  }
+  return *this;
+}
+
+IntStat& IntStat::operator+=(int64_t val)
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    d_data->d_value += val;
+  }
+  return *this;
+}
+
+void IntStat::maxAssign(int64_t val)
+{
+  if (d_data->d_value < val)
+  {
+    d_data->d_value = val;
+  }
+}
+
+void IntStat::minAssign(int64_t val)
+{
+  if (d_data->d_value > val)
+  {
+    d_data->d_value = val;
+  }
+}
+
+void TimerStat::start()
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    Assert(!d_data->d_running) << "timer is already running";
+    d_data->d_start = StatisticTimerValue::clock::now();
+    d_data->d_running = true;
+  }
+}
+void TimerStat::stop()
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    Assert(d_data->d_running) << "timer is not running";
+    d_data->d_duration += StatisticTimerValue::clock::now() - d_data->d_start;
+    d_data->d_running = false;
+  }
+}
+bool TimerStat::running() const
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    return d_data->d_running;
+  }
+  return false;
+}
+
+CodeTimer::CodeTimer(TimerStat& timer, bool allow_reentrant)
+    : d_timer(timer), d_reentrant(false)
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    if (!allow_reentrant || !(d_reentrant = d_timer.running()))
+    {
+      d_timer.start();
+    }
+  }
+}
+CodeTimer::~CodeTimer()
+{
+  if constexpr (Configuration::isStatisticsBuild())
+  {
+    if (!d_reentrant)
+    {
+      d_timer.stop();
+    }
+  }
+}
+
+}  // namespace cvc5
diff --git a/src/util/statistics_stats.h b/src/util/statistics_stats.h
new file mode 100644
index 000000000..9757c31cc
--- /dev/null
+++ b/src/util/statistics_stats.h
@@ -0,0 +1,340 @@
+/*********************                                                        */
+/*! \file statistics_stats.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 Statistic proxy objects
+ **
+ ** Conceptually, every statistic consists of a data object and a proxy
+ ** object. The proxy objects are issued by the `StatisticsRegistry` and
+ ** maintained by the user. They only hold a pointer to a matching data
+ ** object. The purpose of proxy objects is to implement methods to easily
+ ** change the statistic data, but shield the regular user from the internals.
+ */
+
+#include "cvc4_private_library.h"
+
+#ifndef CVC4__UTIL__STATISTICS_STATS_H
+#define CVC4__UTIL__STATISTICS_STATS_H
+
+#include <optional>
+
+#include "base/configuration.h"
+
+namespace cvc5 {
+
+// forward declare all values to avoid inclusion
+struct StatisticAverageValue;
+template <typename T>
+struct StatisticBackedValue;
+template <typename T>
+struct StatisticHistogramValue;
+template <typename T>
+struct StatisticReferenceValue;
+template <typename T>
+struct StatisticSizeValue;
+struct StatisticTimerValue;
+
+class StatisticsRegistry;
+
+/**
+ * Collects the average of a series of double values.
+ * New values are added by
+ *   AverageStat stat;
+ *   stat << 1.0 << 2.0;
+ */
+class AverageStat
+{
+ public:
+  /** Allow access to private constructor */
+  friend class StatisticsRegistry;
+  /** Value stored for this statistic */
+  using stat_type = StatisticAverageValue;
+  /** Add the value `v` to the running average */
+  AverageStat& operator<<(double v);
+
+ private:
+  /** Construct from a pointer to the internal data */
+  AverageStat(stat_type* data) : d_data(data) {}
+  /** The actual data that lives in the registry */
+  stat_type* d_data;
+};
+
+/**
+ * Collects a histogram over some type.
+ * The type needs to be (convertible to) integral and support streaming to
+ * an `std::ostream`.
+ * New values are added by
+ *    HistogramStat<Kind> stat;
+ *    stat << Kind::PLUS << Kind::AND;
+ */
+template <typename Integral>
+class HistogramStat
+{
+ public:
+  /** Allow access to private constructor */
+  friend class StatisticsRegistry;
+  /** Value stored for this statistic */
+  using stat_type = StatisticHistogramValue<Integral>;
+  /** Add the value `val` to the histogram */
+  HistogramStat& operator<<(Integral val)
+  {
+    if constexpr (Configuration::isStatisticsBuild())
+    {
+      d_data->add(val);
+    }
+    return *this;
+  }
+
+ private:
+  /** Construct from a pointer to the internal data */
+  HistogramStat(stat_type* data) : d_data(data) {}
+  /** The actual data that lives in the registry */
+  stat_type* d_data;
+};
+
+/**
+ * Stores the reference to some value that exists outside of this statistic.
+ * Despite being called `ReferenceStat`, the reference is held as a pointer
+ * and can thus be reset using `set`.
+ * Note that the referenced object must have a lifetime that is longer than
+ * the lifetime of the `ReferenceStat` object. Upon destruction of the
+ * `ReferenceStat` the current value of the referenced object is copied into
+ * the `StatisticsRegistry`.
+ *
+ * To convert to the API representation in `api::Stat`, `T` can only be one
+ * of the types accepted by the `api::Stat` constructors (or be implicitly
+ * converted to one of them).
+ */
+template <typename T>
+class ReferenceStat
+{
+ public:
+  /** Allow access to private constructor */
+  friend class StatisticsRegistry;
+  /** Value stored for this statistic */
+  using stat_type = StatisticReferenceValue<T>;
+  /** Reset the reference to point to `t`. */
+  void set(const T& t)
+  {
+    if constexpr (Configuration::isStatisticsBuild())
+    {
+      d_data->d_value = &t;
+    }
+  }
+  /** Copy the current value of the referenced object. */
+  ~ReferenceStat()
+  {
+    if constexpr (Configuration::isStatisticsBuild())
+    {
+      d_data->commit();
+    }
+  }
+
+ private:
+  /** Construct from a pointer to the internal data */
+  ReferenceStat(StatisticReferenceValue<T>* data) : d_data(data) {}
+  /** The actual data that lives in the registry */
+  StatisticReferenceValue<T>* d_data;
+};
+
+/**
+ * Stores the size of some container that exists outside of this statistic.
+ * Note that the referenced container must have a lifetime that is longer than
+ * the lifetime of the `SizeStat` object. Upon destruction of the `SizeStat`
+ * the current size of the referenced container is copied into the
+ * `StatisticsRegistry`.
+ */
+template <typename T>
+class SizeStat
+{
+ public:
+  /** Allow access to private constructor */
+  friend class StatisticsRegistry;
+  /** Value stored for this statistic */
+  using stat_type = StatisticSizeValue<T>;
+  /** Reset the reference to point to `t`. */
+  void set(const T& t)
+  {
+    if constexpr (Configuration::isStatisticsBuild())
+    {
+      d_data->d_value = &t;
+    }
+  }
+  /** Copy the current size of the referenced container. */
+  ~SizeStat()
+  {
+    if constexpr (Configuration::isStatisticsBuild())
+    {
+      d_data->commit();
+    }
+  }
+
+ private:
+  /** Construct from a pointer to the internal data */
+  SizeStat(stat_type* data) : d_data(data) {}
+  /** The actual data that lives in the registry */
+  stat_type* d_data;
+};
+
+class CodeTimer;
+/**
+ * Collects cumulative runtimes. The timer can be started and stopped
+ * arbitrarily like a stopwatch. The value of the statistic is the
+ * accumulated time over all (start,stop) pairs.
+ * While the runtimes are stored in nanosecond precision internally,
+ * the API exports runtimes as integral numbers in millisecond
+ * precision.
+ *
+ * Note that it is recommended to use it in an RAII fashion using the
+ * `CodeTimer` class.
+ */
+class TimerStat
+{
+ public:
+  /** Utility for RAII-style timing of code blocks */
+  using CodeTimer = cvc5::CodeTimer;
+  /** Allow access to private constructor */
+  friend class StatisticsRegistry;
+  /** Value stored for this statistic */
+  using stat_type = StatisticTimerValue;
+
+  /** Start the timer. Assumes it is not already running. */
+  void start();
+  /** Stop the timer. Assumes it is running. */
+  void stop();
+  /** Checks whether the timer is running. */
+  bool running() const;
+
+ private:
+  /** Construct from a pointer to the internal data */
+  TimerStat(stat_type* data) : d_data(data) {}
+  /** The actual data that lives in the registry */
+  stat_type* d_data;
+};
+
+/**
+ * Utility class to make it easier to call `stop` at the end of a code
+ * block. When constructed, it starts the timer. When destructed, it stops
+ * the timer.
+ *
+ * Allows for reentrant usage. If `allow_reentrant` is true, we check
+ * whether the timer is already running. If so, this particular instance
+ * of `CodeTimer` neither starts nor stops the actual timer, but leaves
+ * this to the first (or outermost) `CodeTimer`.
+ */
+class CodeTimer
+{
+ public:
+  /** Disallow copying */
+  CodeTimer(const CodeTimer& timer) = delete;
+  /** Disallow assignment */
+  CodeTimer& operator=(const CodeTimer& timer) = delete;
+  /**
+   * Start the timer.
+   * If `allow_reentrant` is true we check whether the timer is already
+   * running. If so, this particular instance of `CodeTimer` neither starts
+   * nor stops the actual timer, but leaves this to the first (or outermost)
+   * `CodeTimer`.
+   */
+  CodeTimer(TimerStat& timer, bool allow_reentrant = false);
+  /** Stop the timer */
+  ~CodeTimer();
+
+ private:
+  /** Reference to the timer this utility works on */
+  TimerStat& d_timer;
+  /** Whether this timer is reentrant (i.e. does not do anything) */
+  bool d_reentrant;
+};
+
+/**
+ * Stores a simple value that can be set manually using regular assignment
+ * or the `set` method.
+ *
+ * To convert to the API representation in `api::Stat`, `T` can only be one
+ * of the types accepted by the `api::Stat` constructors (or be implicitly
+ * converted to one of them).
+ */
+template <typename T>
+class ValueStat
+{
+ public:
+  /** Allow access to private constructor */
+  friend class StatisticsRegistry;
+  friend class IntStat;
+  /** Value stored for this statistic */
+  using stat_type = StatisticBackedValue<T>;
+  /** Set to `t` */
+  void set(const T& t)
+  {
+    if constexpr (Configuration::isStatisticsBuild())
+    {
+      d_data->d_value = t;
+    }
+  }
+  /** Set to `t` */
+  ValueStat<T>& operator=(const T& t)
+  {
+    if constexpr (Configuration::isStatisticsBuild())
+    {
+      set(t);
+    }
+    return *this;
+  }
+  T get() const
+  {
+    if constexpr (Configuration::isStatisticsBuild())
+    {
+      return d_data->d_value;
+    }
+    return T();
+  }
+
+ private:
+  /** Construct from a pointer to the internal data */
+  ValueStat(StatisticBackedValue<T>* data) : d_data(data) {}
+  /** The actual data that lives in the registry */
+  StatisticBackedValue<T>* d_data;
+};
+
+/**
+ * Stores an integer value as int64_t.
+ * Supports the most useful standard operators (assignment, pre- and
+ * post-increment, addition assignment) and some custom ones (maximum
+ * assignment, minimum assignment).
+ */
+class IntStat : public ValueStat<int64_t>
+{
+ public:
+  /** Allow access to private constructor */
+  friend class StatisticsRegistry;
+  /** Value stored for this statistic */
+  using stat_type = StatisticBackedValue<int64_t>;
+  /** Set to given value */
+  IntStat& operator=(int64_t val);
+  /** Pre-increment for the integer */
+  IntStat& operator++();
+  /** Post-increment for the integer */
+  IntStat& operator++(int);
+  /** Add `val` to the integer */
+  IntStat& operator+=(int64_t val);
+  /** Assign the maximum of the current value and `val` */
+  void maxAssign(int64_t val);
+  /** Assign the minimum of the current value and `val` */
+  void minAssign(int64_t val);
+
+ private:
+  /** Construct from a pointer to the internal data */
+  IntStat(stat_type* data) : ValueStat(data) {}
+};
+
+}  // namespace cvc5
+
+#endif
diff --git a/src/util/statistics_value.cpp b/src/util/statistics_value.cpp
new file mode 100644
index 000000000..6db0b3cd3
--- /dev/null
+++ b/src/util/statistics_value.cpp
@@ -0,0 +1,126 @@
+/*********************                                                        */
+/*! \file statistics_value.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 Statistic data classes
+ **
+ ** The statistic data classes that actually hold the data for the statistics.
+ **
+ ** Conceptually, every statistic consists of a data object and a proxy object.
+ ** The data objects (statistic values) are derived from `StatisticBaseValue`
+ ** and live in the `StatisticsRegistry`.
+ ** They are solely exported to the proxy objects, which should be the sole
+ ** way to manipulate the data of a data object.
+ ** The data objects themselves need to implement printing (normal and safe) and
+ ** conversion to the API type `Stat`.
+ **/
+
+#include "util/statistics_value.h"
+
+#include "util/ostream_util.h"
+
+namespace cvc5 {
+
+// standard helper, see https://en.cppreference.com/w/cpp/utility/variant/visit
+template <class... Ts>
+struct overloaded : Ts...
+{
+  using Ts::operator()...;
+};
+template <class... Ts>
+overloaded(Ts...) -> overloaded<Ts...>;
+
+namespace detail {
+std::ostream& print(std::ostream& out, const StatExportData& sed)
+{
+  std::visit(overloaded{
+                 [&out](std::monostate v) { out << "<unset>"; },
+                 [&out](int64_t v) { out << v; },
+                 [&out](uint64_t v) { out << v; },
+                 [&out](double v) { out << v; },
+                 [&out](const std::string& v) { out << v; },
+                 [&out](const std::map<std::string, uint64_t>& v) {
+                   out << "{ ";
+                   bool first = true;
+                   for (const auto& e : v)
+                   {
+                     if (!first)
+                       out << ", ";
+                     else
+                       first = false;
+                     out << e.first << ": " << e.second;
+                   }
+                   out << " }";
+                 },
+             },
+             sed);
+  return out;
+}
+}
+
+StatisticBaseValue::~StatisticBaseValue() {}
+
+std::ostream& operator<<(std::ostream& out, const StatisticBaseValue& sbv)
+{
+  return detail::print(out, sbv.hasValue() ? sbv.getViewer() : StatExportData{});
+}
+
+StatExportData StatisticAverageValue::getViewer() const { return get(); }
+
+bool StatisticAverageValue::hasValue() const { return d_count > 0; }
+
+void StatisticAverageValue::print(std::ostream& out) const { out << get(); }
+
+void StatisticAverageValue::printSafe(int fd) const
+{
+  safe_print<double>(fd, get());
+}
+
+double StatisticAverageValue::get() const { return d_sum / d_count; }
+
+StatExportData StatisticTimerValue::getViewer() const
+{
+  return static_cast<int64_t>(get() / std::chrono::milliseconds(1));
+}
+
+bool StatisticTimerValue::hasValue() const
+{
+  return d_running || d_duration.count() > 0;
+}
+
+void StatisticTimerValue::print(std::ostream& out) const
+{
+  StreamFormatScope format_scope(out);
+  duration dur = get();
+
+  out << (dur / std::chrono::seconds(1)) << "." << std::setfill('0')
+      << std::setw(9) << std::right << (dur % std::chrono::seconds(1)).count();
+}
+
+void StatisticTimerValue::printSafe(int fd) const
+{
+  duration dur = get();
+  safe_print<uint64_t>(fd, dur / std::chrono::seconds(1));
+  safe_print(fd, ".");
+  safe_print_right_aligned(fd, (dur % std::chrono::seconds(1)).count(), 9);
+}
+
+/** Make sure that we include the time of a currently running timer */
+StatisticTimerValue::duration StatisticTimerValue::get() const
+{
+  auto data = d_duration;
+  if (d_running)
+  {
+    data += clock::now() - d_start;
+  }
+  return data;
+}
+
+}  // namespace cvc5
diff --git a/src/util/statistics_value.h b/src/util/statistics_value.h
new file mode 100644
index 000000000..a272c7a05
--- /dev/null
+++ b/src/util/statistics_value.h
@@ -0,0 +1,402 @@
+/*********************                                                        */
+/*! \file statistics_value.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 Statistic data classes
+ **
+ ** The statistic data classes that actually hold the data for the statistics.
+ **
+ ** Conceptually, every statistic consists of a data object and a proxy object.
+ ** The data objects (statistic values) are derived from `StatisticBaseValue`
+ ** and live in the `StatisticsRegistry`.
+ ** They are solely exported to the proxy objects, which should be the sole
+ ** way to manipulate the data of a data object.
+ ** The data objects themselves need to implement printing (normal and safe) and
+ ** conversion to the API type `Stat`.
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef CVC4__UTIL__STATISTICS_VALUE_H
+#define CVC4__UTIL__STATISTICS_VALUE_H
+
+#include <chrono>
+#include <iomanip>
+#include <map>
+#include <optional>
+#include <sstream>
+#include <variant>
+#include <vector>
+
+#include "util/safe_print.h"
+
+namespace cvc5 {
+
+class StatisticsRegistry;
+
+using StatExportData = std::variant<std::monostate,
+                                    int64_t,
+                                    double,
+                                    std::string,
+                                    std::map<std::string, uint64_t>>;
+namespace detail {
+  std::ostream& print(std::ostream& out, const StatExportData& sed);
+}
+
+/**
+ * Base class for all statistic values.
+ */
+struct StatisticBaseValue
+{
+  virtual ~StatisticBaseValue();
+  /** Checks whether the data holds a non-default value. */
+  virtual bool hasValue() const = 0;
+  /**
+   * Converts the internal data to an instance of `StatExportData` that is
+   * suitable for printing and exporting to the API.
+   * Assumes that `hasValue` returns true. Otherwise, the return value should
+   * assumed to be `std::monostate`.
+   */
+  virtual StatExportData getViewer() const = 0;
+  /**
+   * Writes the data to a regular `std::ostream`.
+   * Assumes that `hasValue` returns true. Otherwise, the user should write
+   * `<undef>` to the stream.
+   */
+  virtual void print(std::ostream&) const = 0;
+  /**
+   * Safely writes the data to a file descriptor. Is suitable to be used
+   * within a signal handler.
+   * Assumes that `hasValue` returns true. Otherwise, the user should write
+   * `<undef>` to the file descriptor.
+   */
+  virtual void printSafe(int fd) const = 0;
+
+  bool d_expert = true;
+};
+/** Writes the data to an output stream */
+std::ostream& operator<<(std::ostream& out, const StatisticBaseValue& sbv);
+
+/** Holds the data for an running average statistic */
+struct StatisticAverageValue : StatisticBaseValue
+{
+  StatExportData getViewer() const override;
+  bool hasValue() const override;
+  void print(std::ostream& out) const override;
+  void printSafe(int fd) const override;
+  double get() const;
+
+  /** Sum of added values */
+  double d_sum;
+  /** Number of added values */
+  uint64_t d_count;
+};
+
+/**
+ * Holds some value of type `T`.
+ *
+ * To convert to the API representation in `getViewer`, `T` can only be one
+ * of the types listed in `Stat::d_data` (or be implicitly converted to
+ * one of them).
+ */
+template <typename T>
+struct StatisticBackedValue : StatisticBaseValue
+{
+  StatExportData getViewer() const override { return d_value; }
+  bool hasValue() const override { return d_value != T(); }
+  void print(std::ostream& out) const override { out << d_value; }
+  void printSafe(int fd) const override { safe_print<T>(fd, d_value); }
+
+  T d_value;
+};
+
+/**
+ * Holds the data for a histogram. We assume the type to be (convertible to)
+ * integral, and we can thus use a std::vector<uint64_t> for fast storage.
+ * The core idea is to track the minimum and maximum values `[a,b]` that have
+ * been added to the histogram and maintain a vector with `b-a+1` values.
+ * The vector is resized on demand to grow as necessary and supports negative
+ * values as well.
+ * Note that the template type needs to have a streaming operator to convert it
+ * to a string in `getViewer`.
+ */
+template <typename Integral>
+struct StatisticHistogramValue : StatisticBaseValue
+{
+  static_assert(std::is_integral<Integral>::value
+                    || std::is_enum<Integral>::value,
+                "Type should be a fundamental integral type.");
+
+  /**
+   * Convert the internal representation to a `std::map<std::string, uint64_t>`
+   */
+  StatExportData getViewer() const override
+  {
+    std::map<std::string, uint64_t> res;
+    for (size_t i = 0, n = d_hist.size(); i < n; ++i)
+    {
+      if (d_hist[i] > 0)
+      {
+        std::stringstream ss;
+        ss << static_cast<Integral>(i + d_offset);
+        res.emplace(ss.str(), d_hist[i]);
+      }
+    }
+    return res;
+  }
+  bool hasValue() const override { return d_hist.size() > 0; }
+  void print(std::ostream& out) const override
+  {
+    out << "[";
+    bool first = true;
+    for (size_t i = 0, n = d_hist.size(); i < n; ++i)
+    {
+      if (d_hist[i] > 0)
+      {
+        if (first)
+        {
+          first = false;
+        }
+        else
+        {
+          out << ", ";
+        }
+        out << "(" << static_cast<Integral>(i + d_offset) << " : " << d_hist[i]
+            << ")";
+      }
+    }
+    out << "]";
+  }
+  void printSafe(int fd) const override
+  {
+    safe_print(fd, "[");
+    bool first = true;
+    for (size_t i = 0, n = d_hist.size(); i < n; ++i)
+    {
+      if (d_hist[i] > 0)
+      {
+        if (first)
+        {
+          first = false;
+        }
+        else
+        {
+          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, "]");
+  }
+
+  /**
+   * Add `val` to the histogram. Casts `val` to `int64_t`, then resizes and
+   * moves the vector entries as necessary.
+   */
+  void add(Integral val)
+  {
+    int64_t v = static_cast<int64_t>(val);
+    if (d_hist.empty())
+    {
+      d_offset = v;
+    }
+    if (v < d_offset)
+    {
+      d_hist.insert(d_hist.begin(), d_offset - v, 0);
+      d_offset = v;
+    }
+    if (static_cast<size_t>(v - d_offset) >= d_hist.size())
+    {
+      d_hist.resize(v - d_offset + 1);
+    }
+    d_hist[v - d_offset]++;
+  }
+
+  /** Actual data */
+  std::vector<uint64_t> d_hist;
+  /** Offset of the entries. d_hist[i] corresponds to Interval(d_offset + i) */
+  int64_t d_offset;
+};
+
+/**
+ * Holds the data for a `ReferenceStat`.
+ * When the `ReferenceStat` is destroyed the current value is copied into
+ * `d_committed`. Once `d_committed` is set, this value is returned, even if
+ * the reference is still valid.
+ */
+template <typename T>
+struct StatisticReferenceValue : StatisticBaseValue
+{
+  StatExportData getViewer() const override
+  {
+    if (d_committed)
+    {
+      if constexpr (std::is_integral_v<T>)
+      {
+        return static_cast<int64_t>(*d_committed);
+      }
+      else
+      {
+        // this else branch is required to ensure compilation.
+        // if T is unsigned int, this return statement triggers a compiler error
+        return *d_committed;
+      }
+    }
+    else if (d_value != nullptr)
+    {
+      if constexpr (std::is_integral_v<T>)
+      {
+        return static_cast<int64_t>(*d_value);
+      }
+      else
+      {
+        // this else branch is required to ensure compilation.
+        // if T is unsigned int, this return statement triggers a compiler error
+        return *d_value;
+      }
+    }
+    return {};
+  }
+  bool hasValue() const override { return d_committed || d_value != nullptr; }
+  void print(std::ostream& out) const override
+  {
+    if (d_committed)
+    {
+      out << *d_committed;
+    }
+    else if (d_value != nullptr)
+    {
+      out << *d_value;
+    }
+  }
+  void printSafe(int fd) const override
+  {
+    if (d_committed)
+    {
+      safe_print<T>(fd, *d_committed);
+    }
+    else if (d_value != nullptr)
+    {
+      safe_print<T>(fd, *d_value);
+    }
+  }
+  void commit()
+  {
+    if (d_value != nullptr)
+    {
+      d_committed = *d_value;
+    }
+  }
+  const T& get() const { return d_committed ? *d_committed : *d_value; }
+
+  const T* d_value = nullptr;
+  std::optional<T> d_committed;
+};
+
+/**
+ * Holds the data for a `SizeStat`.
+ * When the `SizeStat` is destroyed the current size is copied into
+ * `d_committed`. Once `d_committed` is set, this value is returned, even if
+ * the reference is still valid.
+ */
+template <typename T>
+struct StatisticSizeValue : StatisticBaseValue
+{
+  StatExportData getViewer() const override
+  {
+    if (d_committed)
+    {
+      return static_cast<int64_t>(*d_committed);
+    }
+    else if (d_value != nullptr)
+    {
+      return static_cast<int64_t>(d_value->size());
+    }
+    return {};
+  }
+  bool hasValue() const override { return d_committed || d_value != nullptr; }
+  void print(std::ostream& out) const override
+  {
+    if (d_committed)
+    {
+      out << *d_committed;
+    }
+    else if (d_value != nullptr)
+    {
+      out << d_value->size();
+    }
+  }
+  void printSafe(int fd) const override
+  {
+    if (d_committed)
+    {
+      safe_print(fd, *d_committed);
+    }
+    else if (d_value != nullptr)
+    {
+      safe_print(fd, d_value->size());
+    }
+  }
+  void commit()
+  {
+    if (d_value != nullptr)
+    {
+      d_committed = d_value->size();
+    }
+  }
+  size_t get() const { return d_committed ? *d_committed : d_value->size(); }
+
+  const T* d_value = nullptr;
+  std::optional<std::size_t> d_committed;
+};
+
+/**
+ * Holds the data for a `TimerStat`.
+ * Uses `std::chrono` to obtain the current time, store a time point and sum up
+ * the total durations.
+ */
+struct StatisticTimerValue : StatisticBaseValue
+{
+  using clock = std::chrono::steady_clock;
+  using time_point = clock::time_point;
+  struct duration : public std::chrono::nanoseconds
+  {
+  };
+  /** Returns the number of milliseconds */
+  StatExportData getViewer() const override;
+  bool hasValue() const override;
+  /** Prints seconds in fixed-point format */
+  void print(std::ostream& out) const override;
+  /** Prints seconds in fixed-point format */
+  void printSafe(int fd) const override;
+  /** Make sure that we include the time of a currently running timer */
+  duration get() const;
+
+  /**
+   * The cumulative duration of the timer so far. 
+   * Does not include a currently running timer, but `get()` takes care of this.
+   */
+  duration d_duration;
+  /**
+   * The start time of a currently running timer.
+   * May not be reset when the timer is stopped.
+   */
+  time_point d_start;
+  /** Whether a timer is running right now. */
+  bool d_running;
+};
+
+}  // namespace cvc5
+
+#endif