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.

18 files changed, 373 insertions, 1745 deletions

diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index ea4ece8dd..e495fd4d6 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -67,23 +67,14 @@ libcvc4_add_sources(
   sexpr.h
   smt2_quote_string.cpp
   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_stats.cpp
+  statistics_stats.h
   statistics_value.cpp
   statistics_value.h
-  stats_base.cpp
-  stats_base.h
-  stats_histogram.h
-  stats_timer.cpp
-  stats_timer.h
-  stats_utils.cpp
-  stats_utils.h
   string.cpp
   string.h
   tuple.h
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index d0074c444..461c523df 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -96,11 +96,10 @@ const char* toString(Resource r)
 
 struct ResourceManager::Statistics
 {
-  ReferenceStat<std::uint64_t> d_resourceUnitsUsed;
+  ReferenceStat<uint64_t> d_resourceUnitsUsed;
   IntStat d_spendResourceCalls;
   std::vector<IntStat> d_resourceSteps;
   Statistics(StatisticsRegistry& stats);
-  ~Statistics();
 
   void bump(Resource r, uint64_t amount)
   {
@@ -113,37 +112,18 @@ struct ResourceManager::Statistics
     Assert(stats.size() > id);
     stats[id] += amount;
   }
-
-  StatisticsRegistry& d_statisticsRegistry;
 };
 
 ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
-    : d_resourceUnitsUsed("resource::resourceUnitsUsed"),
-      d_spendResourceCalls("resource::spendResourceCalls", 0),
-      d_statisticsRegistry(stats)
+    : d_resourceUnitsUsed(
+        stats.registerReference<uint64_t>("resource::resourceUnitsUsed")),
+      d_spendResourceCalls(stats.registerInt("resource::spendResourceCalls"))
 {
-  d_statisticsRegistry.registerStat(&d_resourceUnitsUsed);
-  d_statisticsRegistry.registerStat(&d_spendResourceCalls);
-
-  // Make sure we don't reallocate the vector
-  d_resourceSteps.reserve(resman_detail::ResourceMax + 1);
   for (std::size_t id = 0; id <= resman_detail::ResourceMax; ++id)
   {
     Resource r = static_cast<Resource>(id);
-    d_resourceSteps.emplace_back("resource::res::" + std::string(toString(r)),
-                                 0);
-    d_statisticsRegistry.registerStat(&d_resourceSteps[id]);
-  }
-}
-
-ResourceManager::Statistics::~Statistics()
-{
-  d_statisticsRegistry.unregisterStat(&d_resourceUnitsUsed);
-  d_statisticsRegistry.unregisterStat(&d_spendResourceCalls);
-
-  for (auto& stat : d_resourceSteps)
-  {
-    d_statisticsRegistry.unregisterStat(&stat);
+    d_resourceSteps.emplace_back(
+        stats.registerInt("resource::res::" + std::string(toString(r))));
   }
 }
 
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
deleted file mode 100644
index b2930a742..000000000
--- a/src/util/statistics.cpp
+++ /dev/null
@@ -1,134 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Morgan Deters, Gereon Kremer, Tim King
- *
- * This file is part of the cvc5 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.
- * ****************************************************************************
- *
- * [[ Add one-line brief description here ]]
- *
- * [[ Add lengthier description here ]]
- * \todo document this file
- */
-
-#include "util/statistics.h"
-
-#include "util/safe_print.h"
-#include "util/statistics_registry.h" // for details about class Stat
-
-namespace cvc5 {
-
-bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const {
-  return s1->getName() < s2->getName();
-}
-
-StatisticsBase::iterator::value_type StatisticsBase::iterator::operator*() const {
-  return std::make_pair((*d_it)->getName(), (*d_it)->getValue());
-}
-
-StatisticsBase::StatisticsBase() :
-  d_stats() {
-}
-
-StatisticsBase::StatisticsBase(const StatisticsBase& stats) :
-  d_stats() {
-}
-
-StatisticsBase& StatisticsBase::operator=(const StatisticsBase& stats) {
-  return *this;
-}
-
-void Statistics::copyFrom(const StatisticsBase& stats) {
-  // This is ugly, but otherwise we have to introduce a "friend" relation for
-  // Base to its derived class (really obnoxious).
-  const StatisticsBase::const_iterator i_begin = stats.begin();
-  const StatisticsBase::const_iterator i_end = stats.end();
-  for(StatisticsBase::const_iterator i = i_begin; i != i_end; ++i) {
-    SExprStat* p = new SExprStat((*i).first, (*i).second);
-    d_stats.insert(p);
-  }
-}
-
-void Statistics::clear() {
-  for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
-    delete *i;
-  }
-  d_stats.clear();
-}
-
-Statistics::Statistics(const StatisticsBase& stats) :
-  StatisticsBase(stats) {
-  copyFrom(stats);
-}
-
-Statistics::Statistics(const Statistics& stats) :
-  StatisticsBase(stats) {
-  copyFrom(stats);
-}
-
-Statistics::~Statistics() {
-  clear();
-}
-
-Statistics& Statistics::operator=(const StatisticsBase& stats) {
-  clear();
-  this->StatisticsBase::operator=(stats);
-  copyFrom(stats);
-
-  return *this;
-}
-
-Statistics& Statistics::operator=(const Statistics& stats) {
-  return this->operator=((const StatisticsBase&)stats);
-}
-
-StatisticsBase::const_iterator StatisticsBase::begin() const {
-  return iterator(d_stats.begin());
-}
-
-StatisticsBase::const_iterator StatisticsBase::end() const {
-  return iterator(d_stats.end());
-}
-
-void StatisticsBase::flushInformation(std::ostream &out) const {
-#ifdef CVC5_STATISTICS_ON
-  for(StatSet::iterator i = d_stats.begin();
-      i != d_stats.end();
-      ++i) {
-    Stat* s = *i;
-    out << s->getName() << ", ";
-    s->flushInformation(out);
-    out << std::endl;
-  }
-#endif /* CVC5_STATISTICS_ON */
-}
-
-void StatisticsBase::safeFlushInformation(int fd) const {
-#ifdef CVC5_STATISTICS_ON
-  for (StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
-    Stat* s = *i;
-    safe_print(fd, s->getName());
-    safe_print(fd, ", ");
-    s->safeFlushInformation(fd);
-    safe_print(fd, "\n");
-  }
-#endif /* CVC5_STATISTICS_ON */
-}
-
-SExpr StatisticsBase::getStatistic(std::string name) const {
-  SExpr value;
-  IntStat s(name, 0);
-  StatSet::iterator i = d_stats.find(&s);
-  if(i != d_stats.end()) {
-    return (*i)->getValue();
-  } else {
-    return SExpr();
-  }
-}
-
-}  // namespace cvc5
diff --git a/src/util/statistics.h b/src/util/statistics.h
deleted file mode 100644
index f6f9a7ca4..000000000
--- a/src/util/statistics.h
+++ /dev/null
@@ -1,133 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Morgan Deters, Mathias Preiner, Andres Noetzli
- *
- * This file is part of the cvc5 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.
- * ****************************************************************************
- *
- * [[ Add one-line brief description here ]]
- *
- * [[ Add lengthier description here ]]
- * \todo document this file
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__STATISTICS_H
-#define CVC5__STATISTICS_H
-
-#include <iterator>
-#include <ostream>
-#include <set>
-#include <string>
-#include <utility>
-
-#include "cvc4_export.h"
-#include "util/sexpr.h"
-
-namespace cvc5 {
-
-class Stat;
-
-class CVC4_EXPORT StatisticsBase
-{
- protected:
-  /** A helper class for comparing two statistics */
-  struct StatCmp {
-    bool operator()(const Stat* s1, const Stat* s2) const;
-  };/* struct StatisticsRegistry::StatCmp */
-
-  /** A type for a set of statistics */
-  typedef std::set< Stat*, StatCmp > StatSet;
-
-  /** The set of statistics in this object */
-  StatSet d_stats;
-
-  StatisticsBase();
-  StatisticsBase(const StatisticsBase& stats);
-  StatisticsBase& operator=(const StatisticsBase& stats);
-
-public:
-
-  virtual ~StatisticsBase() { }
-
-  class iterator : public std::iterator<std::input_iterator_tag,
-                                        std::pair<std::string, SExpr> >
-  {
-    StatSet::iterator d_it;
-
-    iterator(StatSet::iterator it) : d_it(it) { }
-
-    friend class StatisticsBase;
-
-  public:
-    iterator() : d_it() { }
-    iterator(const iterator& it) : d_it(it.d_it) { }
-    value_type operator*() const;
-    iterator& operator++() { ++d_it; return *this; }
-    iterator operator++(int) { iterator old = *this; ++d_it; return old; }
-    bool operator==(const iterator& i) const { return d_it == i.d_it; }
-    bool operator!=(const iterator& i) const { return d_it != i.d_it; }
-  }; /* class StatisticsBase::iterator */
-
-  /** An iterator type over a set of statistics. */
-  typedef iterator const_iterator;
-
-  /** Flush all statistics to the given output stream. */
-  void flushInformation(std::ostream& out) const;
-
-  /**
-   * Flush all statistics to the given file descriptor. Safe to use in a signal
-   * handler.
-   */
-  void safeFlushInformation(int fd) const;
-
-  /** Get the value of a named statistic. */
-  SExpr getStatistic(std::string name) const;
-
-  /**
-   * Get an iterator to the beginning of the range of the set of
-   * statistics.
-   */
-  const_iterator begin() const;
-
-  /**
-   * Get an iterator to the end of the range of the set of statistics.
-   */
-  const_iterator end() const;
-
-}; /* class StatisticsBase */
-
-class Statistics : public StatisticsBase
-{
-  void clear();
-  void copyFrom(const StatisticsBase&);
-
-public:
-
-  /**
-   * Override the copy constructor to do a "deep" copy of statistics
-   * values.
-   */
-  Statistics(const StatisticsBase& stats);
-  Statistics(const Statistics& stats);
-
-  ~Statistics();
-
-  /**
-   * Override the assignment operator to do a "deep" copy of statistics
-   * values.
-   */
-  Statistics& operator=(const StatisticsBase& stats);
-  Statistics& operator=(const Statistics& stats);
-
-}; /* class Statistics */
-
-}  // namespace cvc5
-
-#endif /* CVC5__STATISTICS_H */
diff --git a/src/util/statistics_public.cpp b/src/util/statistics_public.cpp
index 426bec37c..f88996278 100644
--- a/src/util/statistics_public.cpp
+++ b/src/util/statistics_public.cpp
@@ -15,13 +15,35 @@
 
 #include "util/statistics_public.h"
 
+#include "api/cpp/cvc5_kind.h"
+#include "expr/kind.h"
+#include "theory/inference_id.h"
+#include "theory/theory_id.h"
 #include "util/statistics_registry.h"
 
 namespace cvc5 {
 
 void registerPublicStatistics(StatisticsRegistry& reg)
 {
+  reg.registerHistogram<TypeConstant>("api::CONSTANT", false);
+  reg.registerHistogram<TypeConstant>("api::VARIABLE", false);
+  reg.registerHistogram<api::Kind>("api::TERM", false);
 
+  reg.registerValue<std::string>("driver::filename", false);
+  reg.registerValue<std::string>("driver::sat/unsat", false);
+  reg.registerValue<double>("driver::totalTime", false);
+
+  for (theory::TheoryId id = theory::THEORY_FIRST; id != theory::THEORY_LAST;
+       ++id)
+  {
+    std::string prefix = theory::getStatsPrefix(id);
+    reg.registerHistogram<theory::InferenceId>(prefix + "inferencesConflict",
+                                               false);
+    reg.registerHistogram<theory::InferenceId>(prefix + "inferencesFact",
+                                               false);
+    reg.registerHistogram<theory::InferenceId>(prefix + "inferencesLemma",
+                                               false);
+  }
 }
 
 }  // namespace cvc5
diff --git a/src/util/statistics_reg.cpp b/src/util/statistics_reg.cpp
deleted file mode 100644
index cb245eb7a..000000000
--- a/src/util/statistics_reg.cpp
+++ /dev/null
@@ -1,144 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Gereon Kremer
- *
- * This file is part of the cvc5 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.
- * ****************************************************************************
- *
- * 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
deleted file mode 100644
index 7b868a5cb..000000000
--- a/src/util/statistics_reg.h
+++ /dev/null
@@ -1,234 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Gereon Kremer
- *
- * This file is part of the cvc5 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.
- * ****************************************************************************
- *
- * Central statistics registry.
- *
- * The StatisticsRegistry that issues statistic proxy objects.
- */
-
-#include "cvc5_private_library.h"
-
-#ifndef CVC5__UTIL__STATISTICS_REG_H
-#define CVC5__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
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index ca7fb8b1c..ebd16ebc0 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -1,6 +1,6 @@
 /******************************************************************************
  * Top contributors (to current version):
- *   Tim King, Morgan Deters, Mathias Preiner
+ *   Gereon Kremer
  *
  * This file is part of the cvc5 project.
  *
@@ -10,81 +10,146 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Statistics utility classes
+ * Central statistics registry.
+ *
+ * The StatisticsRegistry that issues statistic proxy objects.
  */
 
 #include "util/statistics_registry.h"
 
-#include <cstdlib>
-#include <iostream>
-
-#include "base/check.h"
-#include "lib/clock_gettime.h"
-#include "util/ostream_util.h"
-
-#ifdef CVC5_STATISTICS_ON
-#define CVC5_USE_STATISTICS true
-#else
-#define CVC5_USE_STATISTICS false
-#endif
+#include "options/base_options.h"
+#include "util/statistics_public.h"
 
-
-/****************************************************************************/
-/* Some utility functions for timespec                                    */
-/****************************************************************************/
 namespace cvc5 {
 
-void StatisticsRegistry::registerStat(Stat* s)
+StatisticsRegistry::StatisticsRegistry(bool registerPublic)
 {
-#ifdef CVC5_STATISTICS_ON
-  PrettyCheckArgument(
-      d_stats.find(s) == d_stats.end(),
-      s,
-      "Statistic `%s' is already registered with this registry.",
-      s->getName().c_str());
-  d_stats.insert(s);
-#endif /* CVC5_STATISTICS_ON */
-}/* StatisticsRegistry::registerStat_() */
+  if (registerPublic)
+  {
+    registerPublicStatistics(*this);
+  }
+}
 
-void StatisticsRegistry::unregisterStat(Stat* s)
+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)
 {
-#ifdef CVC5_STATISTICS_ON
-  AlwaysAssert(s != nullptr);
-  AlwaysAssert(d_stats.erase(s) > 0)
-      << "Statistic `" << s->getName()
-      << "' was not registered with this registry.";
-#endif /* CVC5_STATISTICS_ON */
-} /* StatisticsRegistry::unregisterStat() */
+  return registerStat<TimerStat>(name, expert);
+}
 
-void StatisticsRegistry::flushStat(std::ostream &out) const {
-#ifdef CVC5_STATISTICS_ON
-  flushInformation(out);
-#endif /* CVC5_STATISTICS_ON */
+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::statisticsAll() && s.second->isDefault()) continue;
+      d_lastSnapshot->emplace(
+          s.first,
+          s.second->getViewer());
+    }
+  }
 }
 
-void StatisticsRegistry::flushInformation(std::ostream &out) const {
-#ifdef CVC5_STATISTICS_ON
-  this->StatisticsBase::flushInformation(out);
-#endif /* CVC5_STATISTICS_ON */
+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::safeFlushInformation(int fd) const {
-#ifdef CVC5_STATISTICS_ON
-  this->StatisticsBase::safeFlushInformation(fd);
-#endif /* CVC5_STATISTICS_ON */
+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::statisticsAll() && s.second->isDefault()) continue;
+      os << s.first << " = " << *s.second << std::endl;
+    }
+  }
 }
 
-RegisterStatistic::RegisterStatistic(StatisticsRegistry* reg, Stat* stat)
-    : d_reg(reg),
-      d_stat(stat) {
-  CheckArgument(reg != NULL, reg,
-                "You need to specify a statistics registry"
-                "on which to set the statistic");
-  d_reg->registerStat(d_stat);
+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::statisticsAll() && s.second->isDefault()) continue;
+
+      safe_print(fd, s.first);
+      safe_print(fd, " = ");
+      s.second->printSafe(fd);
+      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::statisticsAll() && s.second->isDefault())
+      {
+        auto oldit = d_lastSnapshot->find(s.first);
+        if (oldit != d_lastSnapshot->end() && oldit->second != s.second->getViewer())
+        {
+          // present in the snapshot, now defaulted
+          os << s.first << " = " << *s.second << " (was ";
+          detail::print(os, oldit->second);
+          os << ")" << std::endl;
+        }
+      }
+      else
+      {
+        auto oldit = d_lastSnapshot->find(s.first);
+        if (oldit == d_lastSnapshot->end())
+        {
+          // not present in the snapshot
+          os << s.first << " = " << *s.second << " (was <default>)"
+             << std::endl;
+        }
+        else if (oldit->second != s.second->getViewer())
+        {
+          // present in the snapshot, print old value
+          os << s.first << " = " << *s.second << " (was ";
+          detail::print(os, oldit->second);
+          os << ")" << std::endl;
+        }
+      }
+    }
+  }
 }
 
-RegisterStatistic::~RegisterStatistic() {
-  d_reg->unregisterStat(d_stat);
+std::ostream& operator<<(std::ostream& os, const StatisticsRegistry& sr)
+{
+  sr.print(os);
+  return os;
 }
 
 }  // namespace cvc5
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 098d88c07..7a714012e 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -1,6 +1,6 @@
 /******************************************************************************
  * Top contributors (to current version):
- *   Morgan Deters, Gereon Kremer, Tim King
+ *   Gereon Kremer
  *
  * This file is part of the cvc5 project.
  *
@@ -10,26 +10,9 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Statistics utility classes
- *
- * Statistics utility classes, including classes for holding (and referring
- * to) statistics, the statistics registry, and some other associated
- * classes.
- *
- * This file is somewhat unique in that it is a "cvc5_private_library.h"
- * header. Because of this, most classes need to be marked as CVC4_EXPORT.
- * This is because CVC4_EXPORT is connected to the visibility of the linkage
- * in the object files for the class. It does not dictate what headers are
- * installed.
- * Because the StatisticsRegistry and associated classes are built into
- * libutil, which is used by libcvc4, and then later used by the libmain
- * without referring to libutil as well. Thus the without marking these as
- * CVC4_EXPORT the symbols would be external in libutil, internal in libcvc4,
- * and not be visible to libmain and linking would fail.
- * You can debug this using "nm" on the .so and .o files in the builds/
- * directory. See
- * http://eli.thegreenplace.net/2013/07/09/library-order-in-static-linking
- * for a longer discussion on symbol visibility.
+ * Central statistics registry.
+ *
+ * The StatisticsRegistry that issues statistic proxy objects.
  */
 
 /**
@@ -85,117 +68,203 @@
 #ifndef CVC5__STATISTICS_REGISTRY_H
 #define CVC5__STATISTICS_REGISTRY_H
 
-#include <ctime>
-#include <iomanip>
+#include <iostream>
 #include <map>
-#include <sstream>
-#include <vector>
-
-#ifdef CVC5_STATISTICS_ON
-#define CVC5_USE_STATISTICS true
-#else
-#define CVC5_USE_STATISTICS false
-#endif
+#include <memory>
+#include <typeinfo>
 
-#include "base/exception.h"
-#include "cvc4_export.h"
-#include "util/safe_print.h"
-#include "util/statistics.h"
-#include "util/stats_base.h"
+#include "base/check.h"
+#include "util/statistics_stats.h"
+#include "util/statistics_value.h"
 
 namespace cvc5 {
 
-/** A statistic that contains a SExpr. */
-class SExprStat : public Stat {
-private:
-  SExpr d_data;
+struct StatisticBaseValue;
 
-public:
+/**
+ * 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>;
 
   /**
-   * Construct a SExpr-valued statistic with the given name and
-   * initial value.
+   * 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.
    */
-  SExprStat(const std::string& name, const SExpr& init) :
-    Stat(name), d_data(init){}
+  StatisticsRegistry(bool registerPublic = true);
 
-  void flushInformation(std::ostream& out) const override
+  /** 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)
   {
-    out << d_data;
+    return registerStat<HistogramStat<T>>(name, expert);
   }
 
-  void safeFlushInformation(int fd) const override
+  /** 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)
   {
-    // SExprStat is only used in statistics.cpp in copyFrom, which we cannot
-    // do in a signal handler anyway.
-    safe_print(fd, "<unsupported>");
+    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;
   }
 
-  SExpr getValue() const override { return d_data; }
-
-};/* class SExprStat */
+  /**
+   * 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;
+  }
 
-/****************************************************************************/
-/* Statistics Registry                                                      */
-/****************************************************************************/
+  /** Register a new timer statistic for `name` */
+  TimerStat registerTimer(const std::string& name, bool expert = true);
 
-/**
- * The main statistics registry.  This registry maintains the list of
- * currently active statistics and is able to "flush" them all.
- */
-class CVC4_EXPORT StatisticsRegistry : public StatisticsBase
-{
- private:
-  /** Private copy constructor undefined (no copy permitted). */
-  StatisticsRegistry(const StatisticsRegistry&) = delete;
+  /** 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);
+  }
 
-public:
+  /** 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;
+  }
 
-  /** Construct an nameless statistics registry */
-  StatisticsRegistry() {}
+  /** begin iteration */
+  auto begin() const { return d_stats.begin(); }
+  /** end iteration */
+  auto end() const { return d_stats.end(); }
 
-  void flushStat(std::ostream& out) const;
+  /**
+   * Obtain the current state of all statistics.
+   */
+  void storeSnapshot();
 
-  void flushInformation(std::ostream& out) const;
+  /**
+   * Obtain a single statistic by name. Returns nullptr if no statistic has
+   * been registered for this name.
+   */
+  StatisticBaseValue* get(const std::string& name) const;
 
-  void safeFlushInformation(int fd) 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 stored snapshot.
+   */
+  void printDiff(std::ostream& os) const;
 
-  SExpr getValue() 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)
   {
-    std::vector<SExpr> v;
-    for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
-      std::vector<SExpr> w;
-      w.push_back(SExpr((*i)->getName()));
-      w.push_back((*i)->getValue());
-      v.push_back(SExpr(w));
+    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 SExpr(v);
+    return Stat(nullptr);
   }
 
-  /** Register a new statistic */
-  void registerStat(Stat* s);
-
-  /** Unregister a new statistic */
-  void unregisterStat(Stat* s);
-
-}; /* class StatisticsRegistry */
-
-/**
- * Resource-acquisition-is-initialization idiom for statistics
- * registry.  Useful for stack-based statistics (like in the driver).
- * This RAII class only does registration and unregistration.
- */
-class CVC4_EXPORT RegisterStatistic
-{
- public:
-  RegisterStatistic(StatisticsRegistry* reg, Stat* stat);
-  ~RegisterStatistic();
+  /**
+   * Holds (and owns) all statistic values, indexed by the name they were
+   * registered for.
+   */
+  std::map<std::string, std::unique_ptr<StatisticBaseValue>> d_stats;
 
-private:
-  StatisticsRegistry* d_reg;
-  Stat* d_stat;
+  std::unique_ptr<Snapshot> d_lastSnapshot;
+};
 
-}; /* class RegisterStatistic */
+/** Calls `sr.print(os)`. */
+std::ostream& operator<<(std::ostream& os, const StatisticsRegistry& sr);
 
 }  // namespace cvc5
 
diff --git a/src/util/statistics_value.cpp b/src/util/statistics_value.cpp
index e92507d72..24b482f85 100644
--- a/src/util/statistics_value.cpp
+++ b/src/util/statistics_value.cpp
@@ -42,7 +42,6 @@ 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; },
@@ -70,14 +69,12 @@ StatisticBaseValue::~StatisticBaseValue() {}
 
 std::ostream& operator<<(std::ostream& out, const StatisticBaseValue& sbv)
 {
-  return detail::print(out, sbv.hasValue() ? sbv.getViewer() : StatExportData{});
+  return detail::print(out, sbv.getViewer());
 }
 
 StatExportData StatisticAverageValue::getViewer() const { return get(); }
 
-bool StatisticAverageValue::hasValue() const { return d_count > 0; }
-
-void StatisticAverageValue::print(std::ostream& out) const { out << get(); }
+bool StatisticAverageValue::isDefault() const { return d_count == 0; }
 
 void StatisticAverageValue::printSafe(int fd) const
 {
@@ -88,40 +85,29 @@ double StatisticAverageValue::get() const { return d_sum / d_count; }
 
 StatExportData StatisticTimerValue::getViewer() const
 {
-  return static_cast<int64_t>(get() / std::chrono::milliseconds(1));
+  return std::to_string(get()) + "ms";
 }
 
-bool StatisticTimerValue::hasValue() const
+bool StatisticTimerValue::isDefault() 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();
+  return !d_running && d_duration.count() == 0;
 }
 
 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);
+  safe_print<uint64_t>(fd, get());
+  safe_print<std::string>(fd, "ms");
 }
 
 /** Make sure that we include the time of a currently running timer */
-StatisticTimerValue::duration StatisticTimerValue::get() const
+uint64_t StatisticTimerValue::get() const
 {
   auto data = d_duration;
   if (d_running)
   {
     data += clock::now() - d_start;
   }
-  return data;
+  return static_cast<int64_t>(data / std::chrono::milliseconds(1));
 }
 
 }  // namespace cvc5
diff --git a/src/util/statistics_value.h b/src/util/statistics_value.h
index fef518a69..09f429187 100644
--- a/src/util/statistics_value.h
+++ b/src/util/statistics_value.h
@@ -42,11 +42,8 @@ namespace cvc5 {
 
 class StatisticsRegistry;
 
-using StatExportData = std::variant<std::monostate,
-                                    int64_t,
-                                    double,
-                                    std::string,
-                                    std::map<std::string, uint64_t>>;
+using StatExportData =
+    std::variant<int64_t, double, std::string, std::map<std::string, uint64_t>>;
 namespace detail {
   std::ostream& print(std::ostream& out, const StatExportData& sed);
 }
@@ -57,26 +54,16 @@ namespace detail {
 struct StatisticBaseValue
 {
   virtual ~StatisticBaseValue();
-  /** Checks whether the data holds a non-default value. */
-  virtual bool hasValue() const = 0;
+  /** Checks whether the data holds the default value. */
+  virtual bool isDefault() 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;
 
@@ -89,8 +76,7 @@ std::ostream& operator<<(std::ostream& out, const StatisticBaseValue& sbv);
 struct StatisticAverageValue : StatisticBaseValue
 {
   StatExportData getViewer() const override;
-  bool hasValue() const override;
-  void print(std::ostream& out) const override;
+  bool isDefault() const override;
   void printSafe(int fd) const override;
   double get() const;
 
@@ -111,8 +97,7 @@ 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; }
+  bool isDefault() const override { return d_value == T(); }
   void printSafe(int fd) const override { safe_print<T>(fd, d_value); }
 
   T d_value;
@@ -152,32 +137,10 @@ struct StatisticHistogramValue : StatisticBaseValue
     }
     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 << "]";
-  }
+  bool isDefault() const override { return d_hist.size() == 0; }
   void printSafe(int fd) const override
   {
-    safe_print(fd, "[");
+    safe_print(fd, "{ ");
     bool first = true;
     for (size_t i = 0, n = d_hist.size(); i < n; ++i)
     {
@@ -193,12 +156,12 @@ struct StatisticHistogramValue : StatisticBaseValue
         }
         safe_print(fd, "(");
         safe_print<Integral>(fd, static_cast<Integral>(i + d_offset));
-        safe_print(fd, " : ");
+        safe_print(fd, ": ");
         safe_print<uint64_t>(fd, d_hist[i]);
         safe_print(fd, ")");
       }
     }
-    safe_print(fd, "]");
+    safe_print(fd, " }");
   }
 
   /**
@@ -267,19 +230,24 @@ struct StatisticReferenceValue : StatisticBaseValue
         return *d_value;
       }
     }
-    return {};
+    if constexpr (std::is_integral_v<T>)
+    {
+      return static_cast<int64_t>(0);
+    }
+    else
+    {
+      // this else branch is required to ensure compilation.
+      // if T is unsigned int, this return statement triggers a compiler error
+      return T();
+    }
   }
-  bool hasValue() const override { return d_committed || d_value != nullptr; }
-  void print(std::ostream& out) const override
+  bool isDefault() const override
   {
     if (d_committed)
     {
-      out << *d_committed;
-    }
-    else if (d_value != nullptr)
-    {
-      out << *d_value;
+      return *d_committed == T();
     }
+    return d_value == nullptr || *d_value == T();
   }
   void printSafe(int fd) const override
   {
@@ -291,6 +259,10 @@ struct StatisticReferenceValue : StatisticBaseValue
     {
       safe_print<T>(fd, *d_value);
     }
+    else
+    {
+      safe_print<T>(fd, T());
+    }
   }
   void commit()
   {
@@ -324,19 +296,15 @@ struct StatisticSizeValue : StatisticBaseValue
     {
       return static_cast<int64_t>(d_value->size());
     }
-    return {};
+    return static_cast<int64_t>(0);
   }
-  bool hasValue() const override { return d_committed || d_value != nullptr; }
-  void print(std::ostream& out) const override
+  bool isDefault() const override
   {
     if (d_committed)
     {
-      out << *d_committed;
-    }
-    else if (d_value != nullptr)
-    {
-      out << d_value->size();
+      return *d_committed == 0;
     }
+    return d_value == nullptr || d_value->size() == 0;
   }
   void printSafe(int fd) const override
   {
@@ -348,6 +316,10 @@ struct StatisticSizeValue : StatisticBaseValue
     {
       safe_print(fd, d_value->size());
     }
+    else
+    {
+      safe_print(fd, 0);
+    }
   }
   void commit()
   {
@@ -376,13 +348,14 @@ struct StatisticTimerValue : StatisticBaseValue
   };
   /** 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;
+  bool isDefault() 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;
+  /**
+   * Returns the elapsed time in milliseconds.
+   * Make sure that we include the time of a currently running timer
+   */
+  uint64_t get() const;
 
   /**
    * The cumulative duration of the timer so far. 
diff --git a/src/util/stats_base.cpp b/src/util/stats_base.cpp
deleted file mode 100644
index 886effe5e..000000000
--- a/src/util/stats_base.cpp
+++ /dev/null
@@ -1,114 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Gereon Kremer, Tim King, Morgan Deters
- *
- * This file is part of the cvc5 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.
- * ****************************************************************************
- *
- * Base statistic classes.
- */
-
-#include "util/stats_base.h"
-
-#include "util/statistics_registry.h"
-
-namespace cvc5 {
-
-Stat::Stat(const std::string& name) : d_name(name)
-{
-  if (CVC5_USE_STATISTICS)
-  {
-    CheckArgument(d_name.find(", ") == std::string::npos,
-                  name,
-                  "Statistics names cannot include a comma (',')");
-  }
-}
-
-IntStat::IntStat(const std::string& name, int64_t init)
-    : BackedStat<int64_t>(name, init)
-{
-}
-
-/** Increment the underlying integer statistic. */
-IntStat& IntStat::operator++()
-{
-  if (CVC5_USE_STATISTICS)
-  {
-    ++d_data;
-  }
-  return *this;
-}
-/** Increment the underlying integer statistic. */
-IntStat& IntStat::operator++(int)
-{
-  if (CVC5_USE_STATISTICS)
-  {
-    ++d_data;
-  }
-  return *this;
-}
-
-/** Increment the underlying integer statistic by the given amount. */
-IntStat& IntStat::operator+=(int64_t val)
-{
-  if (CVC5_USE_STATISTICS)
-  {
-    d_data += val;
-  }
-  return *this;
-}
-
-/** Keep the maximum of the current statistic value and the given one. */
-void IntStat::maxAssign(int64_t val)
-{
-  if (CVC5_USE_STATISTICS)
-  {
-    if (d_data < val)
-    {
-      d_data = val;
-    }
-  }
-}
-
-/** Keep the minimum of the current statistic value and the given one. */
-void IntStat::minAssign(int64_t val)
-{
-  if (CVC5_USE_STATISTICS)
-  {
-    if (d_data > val)
-    {
-      d_data = val;
-    }
-  }
-}
-
-AverageStat::AverageStat(const std::string& name)
-    : BackedStat<double>(name, 0.0)
-{
-}
-
-/** Add an entry to the running-average calculation. */
-AverageStat& AverageStat::operator<<(double e)
-{
-  if (CVC5_USE_STATISTICS)
-  {
-    ++d_count;
-    d_sum += e;
-    set(d_sum / d_count);
-  }
-  return *this;
-}
-
-SExpr AverageStat::getValue() const
-{
-  std::stringstream ss;
-  ss << std::fixed << std::setprecision(8) << d_data;
-  return SExpr(Rational::fromDecimal(ss.str()));
-}
-
-}  // namespace cvc5
diff --git a/src/util/stats_base.h b/src/util/stats_base.h
deleted file mode 100644
index 9c3222d02..000000000
--- a/src/util/stats_base.h
+++ /dev/null
@@ -1,278 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Gereon Kremer, Morgan Deters, Tim King
- *
- * This file is part of the cvc5 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.
- * ****************************************************************************
- *
- * Base statistic classes.
- */
-
-#include "cvc5_private_library.h"
-
-#ifndef CVC5__UTIL__STATS_BASE_H
-#define CVC5__UTIL__STATS_BASE_H
-
-#include <iomanip>
-#include <sstream>
-#include <string>
-
-#include "cvc4_export.h"
-#include "util/safe_print.h"
-#include "util/sexpr.h"
-#include "util/stats_utils.h"
-
-#ifdef CVC5_STATISTICS_ON
-#define CVC5_USE_STATISTICS true
-#else
-#define CVC5_USE_STATISTICS false
-#endif
-
-namespace cvc5 {
-
-/**
- * The base class for all statistics.
- *
- * This base class keeps the name of the statistic and declares the (pure)
- * virtual functions flushInformation() and safeFlushInformation().
- * Derived classes must implement these function and pass their name to
- * the base class constructor.
- */
-class CVC4_EXPORT Stat
-{
- public:
-  /**
-   * Construct a statistic with the given name.  Debug builds of CVC4
-   * will throw an assertion exception if the given name contains the
-   * statistic delimiter string.
-   */
-  Stat(const std::string& name);
-
-  /** Destruct a statistic.  This base-class version does nothing. */
-  virtual ~Stat() = default;
-
-  /**
-   * Flush the value of this statistic to an output stream.  Should
-   * finish the output with an end-of-line character.
-   */
-  virtual void flushInformation(std::ostream& out) const = 0;
-
-  /**
-   * Flush the value of this statistic to a file descriptor. Should finish the
-   * output with an end-of-line character. Should be safe to use in a signal
-   * handler.
-   */
-  virtual void safeFlushInformation(int fd) const = 0;
-
-  /** Get the name of this statistic. */
-  const std::string& getName() const { return d_name; }
-
-  /** Get the value of this statistic as a string. */
-  virtual SExpr getValue() const
-  {
-    std::stringstream ss;
-    flushInformation(ss);
-    return SExpr(ss.str());
-  }
-
- protected:
-  /** The name of this statistic */
-  std::string d_name;
-}; /* class Stat */
-
-/**
- * A data statistic that keeps a T and sets it with setData().
- *
- * Template class T must have an operator=() and a copy constructor.
- */
-template <class T>
-class BackedStat : public Stat
-{
- public:
-  /** Construct a backed statistic with the given name and initial value. */
-  BackedStat(const std::string& name, const T& init) : Stat(name), d_data(init)
-  {
-  }
-
-  /** Set the underlying data value to the given value. */
-  void set(const T& t)
-  {
-    if (CVC5_USE_STATISTICS)
-    {
-      d_data = t;
-    }
-  }
-
-  const T& get() const { return d_data; }
-
-  /** Flush the value of the statistic to the given output stream. */
-  virtual void flushInformation(std::ostream& out) const override
-  {
-    out << d_data;
-  }
-
-  virtual void safeFlushInformation(int fd) const override
-  {
-    safe_print<T>(fd, d_data);
-  }
-
- protected:
-  /** The internally-kept statistic value */
-  T d_data;
-}; /* class BackedStat<T> */
-
-/**
- * A data statistic that references a data cell of type T,
- * implementing get() by referencing that memory cell, and
- * setData() by reassigning the statistic to point to the new
- * data cell.  The referenced data cell is kept as a const
- * reference, meaning the referenced data is never actually
- * modified by this class (it must be externally modified for
- * a reference statistic to make sense).  A common use for
- * this type of statistic is to output a statistic that is kept
- * outside the statistics package (for example, one that's kept
- * by a theory implementation for internal heuristic purposes,
- * which is important to keep even if statistics are turned off).
- *
- * Template class T must have an assignment operator=().
- */
-template <class T>
-class ReferenceStat : public Stat
-{
- public:
-  /**
-   * Construct a reference stat with the given name and a reference
-   * to nullptr.
-   */
-  ReferenceStat(const std::string& name) : Stat(name) {}
-
-  /**
-   * Construct a reference stat with the given name and a reference to
-   * the given data.
-   */
-  ReferenceStat(const std::string& name, const T& data) : Stat(name)
-  {
-    set(data);
-  }
-
-  /** Set this reference statistic to refer to the given data cell. */
-  void set(const T& t)
-  {
-    if (CVC5_USE_STATISTICS)
-    {
-      d_data = &t;
-    }
-  }
-  const T& get() const { return *d_data; }
-
-  /** Flush the value of the statistic to the given output stream. */
-  virtual void flushInformation(std::ostream& out) const override
-  {
-    out << *d_data;
-  }
-
-  virtual void safeFlushInformation(int fd) const override
-  {
-    safe_print<T>(fd, *d_data);
-  }
-
- private:
-  /** The referenced data cell */
-  const T* d_data = nullptr;
-}; /* class ReferenceStat<T> */
-
-/**
- * A backed integer-valued (64-bit signed) statistic.
- * This doesn't functionally differ from its base class BackedStat<int64_t>,
- * except for adding convenience functions for dealing with integers.
- */
-class IntStat : public BackedStat<int64_t>
-{
- public:
-  /**
-   * Construct an integer-valued statistic with the given name and
-   * initial value.
-   */
-  IntStat(const std::string& name, int64_t init);
-
-  /** Increment the underlying integer statistic. */
-  IntStat& operator++();
-  /** Increment the underlying integer statistic. */
-  IntStat& operator++(int);
-
-  /** Increment the underlying integer statistic by the given amount. */
-  IntStat& operator+=(int64_t val);
-
-  /** Keep the maximum of the current statistic value and the given one. */
-  void maxAssign(int64_t val);
-
-  /** Keep the minimum of the current statistic value and the given one. */
-  void minAssign(int64_t val);
-
-  SExpr getValue() const override { return SExpr(Integer(d_data)); }
-
-}; /* class IntStat */
-
-/**
- * The value for an AverageStat is the running average of (e1, e_2, ..., e_n),
- *   (e1 + e_2 + ... + e_n)/n,
- * where e_i is an entry added by an addEntry(e_i) call.
- * The value is initially always 0.
- * (This is to avoid making parsers confused.)
- *
- * A call to setData() will change the running average but not reset the
- * running count, so should generally be avoided.  Call addEntry() to add
- * an entry to the average calculation.
- */
-class AverageStat : public BackedStat<double>
-{
- public:
-  /** Construct an average statistic with the given name. */
-  AverageStat(const std::string& name);
-
-  /** Add an entry to the running-average calculation. */
-  AverageStat& operator<<(double e);
-
-  SExpr getValue() const override;
-
- private:
-  /**
-   * The number of accumulations of the running average that we
-   * have seen so far.
-   */
-  uint32_t d_count = 0;
-  double d_sum = 0;
-}; /* class AverageStat */
-
-template <class T>
-class SizeStat : public Stat
-{
- public:
-  SizeStat(const std::string& name, const T& sized) : Stat(name), d_sized(sized)
-  {
-  }
-  ~SizeStat() {}
-
-  /** Flush the value of the statistic to the given output stream. */
-  void flushInformation(std::ostream& out) const override
-  {
-    out << d_sized.size();
-  }
-
-  void safeFlushInformation(int fd) const override
-  {
-    safe_print(fd, d_sized.size());
-  }
-
- private:
-  const T& d_sized;
-}; /* class SizeStat */
-
-}  // namespace cvc5
-
-#endif
diff --git a/src/util/stats_histogram.h b/src/util/stats_histogram.h
deleted file mode 100644
index 99dcbb448..000000000
--- a/src/util/stats_histogram.h
+++ /dev/null
@@ -1,129 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Gereon Kremer, Mathias Preiner, Tim King
- *
- * This file is part of the cvc5 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.
- * ****************************************************************************
- *
- * Histogram statistics.
- *
- * Stat classes that represent histograms.
- */
-
-#include "cvc5_private_library.h"
-
-#ifndef CVC5__UTIL__STATS_HISTOGRAM_H
-#define CVC5__UTIL__STATS_HISTOGRAM_H
-
-#include <map>
-#include <vector>
-
-#include "util/stats_base.h"
-
-namespace cvc5 {
-
-/**
- * A histogram statistic class for integral types.
- * Avoids using an std::map (like we would do for generic types) in favor of a
- * faster std::vector by casting the integral values to indices into the
- * vector. Requires the type to be an integral type that is convertible to
- * int64_t, also supporting appropriate enum types.
- * The vector is resized on demand to grow as necessary and supports negative
- * values as well.
- */
-template <typename Integral>
-class IntegralHistogramStat : public Stat
-{
-  static_assert(std::is_integral<Integral>::value
-                    || std::is_enum<Integral>::value,
-                "Type should be a fundamental integral type.");
-
- public:
-  /** Construct a histogram of a stream of entries. */
-  IntegralHistogramStat(const std::string& name) : Stat(name) {}
-
-  void flushInformation(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 safeFlushInformation(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, "]");
-  }
-
-  IntegralHistogramStat& operator<<(Integral val)
-  {
-    if (CVC5_USE_STATISTICS)
-    {
-      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]++;
-    }
-    return (*this);
-  }
-
- private:
-  std::vector<uint64_t> d_hist;
-  int64_t d_offset;
-}; /* class IntegralHistogramStat */
-
-}  // namespace cvc5
-
-#endif
diff --git a/src/util/stats_timer.cpp b/src/util/stats_timer.cpp
deleted file mode 100644
index 1ffbe28a8..000000000
--- a/src/util/stats_timer.cpp
+++ /dev/null
@@ -1,105 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Gereon Kremer, Morgan Deters, Andres Noetzli
- *
- * This file is part of the cvc5 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.
- * ****************************************************************************
- *
- * Timer statistics.
- *
- * Stat classes that hold timers.
- */
-
-#include "util/stats_timer.h"
-
-#include <iostream>
-
-#include "base/check.h"
-#include "util/ostream_util.h"
-
-namespace cvc5 {
-
-template <>
-void safe_print(int fd, const timer_stat_detail::duration& t)
-{
-  safe_print<uint64_t>(fd, t / std::chrono::seconds(1));
-  safe_print(fd, ".");
-  safe_print_right_aligned(fd, (t % std::chrono::seconds(1)).count(), 9);
-}
-
-void TimerStat::start()
-{
-  if (CVC5_USE_STATISTICS)
-  {
-    PrettyCheckArgument(!d_running, *this, "timer already running");
-    d_start = timer_stat_detail::clock::now();
-    d_running = true;
-  }
-}
-
-void TimerStat::stop()
-{
-  if (CVC5_USE_STATISTICS)
-  {
-    AlwaysAssert(d_running) << "timer not running";
-    d_data += timer_stat_detail::clock::now() - d_start;
-    d_running = false;
-  }
-}
-
-bool TimerStat::running() const { return d_running; }
-
-timer_stat_detail::duration TimerStat::get() const
-{
-  auto data = d_data;
-  if (CVC5_USE_STATISTICS && d_running)
-  {
-    data += timer_stat_detail::clock::now() - d_start;
-  }
-  return data;
-}
-
-SExpr TimerStat::getValue() const
-{
-  auto data = d_data;
-  if (CVC5_USE_STATISTICS && d_running)
-  {
-    data += timer_stat_detail::clock::now() - d_start;
-  }
-  std::stringstream ss;
-  ss << std::fixed << std::setprecision(8) << data;
-  return SExpr(Rational::fromDecimal(ss.str()));
-}
-
-void TimerStat::flushInformation(std::ostream& out) const { out << get(); }
-
-void TimerStat::safeFlushInformation(int fd) const
-{
-  // Overwrite the implementation in the superclass because we cannot use
-  // getDataRef(): it might return stale data if the timer is currently
-  // running.
-  safe_print<timer_stat_detail::duration>(fd, get());
-}
-
-CodeTimer::CodeTimer(TimerStat& timer, bool allow_reentrant)
-    : d_timer(timer), d_reentrant(false)
-{
-  if (!allow_reentrant || !(d_reentrant = d_timer.running()))
-  {
-    d_timer.start();
-  }
-}
-CodeTimer::~CodeTimer()
-{
-  if (!d_reentrant)
-  {
-    d_timer.stop();
-  }
-}
-
-}  // namespace cvc5
diff --git a/src/util/stats_timer.h b/src/util/stats_timer.h
deleted file mode 100644
index bbb0750de..000000000
--- a/src/util/stats_timer.h
+++ /dev/null
@@ -1,114 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Morgan Deters, Gereon Kremer, Mathias Preiner
- *
- * This file is part of the cvc5 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.
- * ****************************************************************************
- *
- * Timer statistics.
- *
- * Stat classes that hold timers.
- */
-
-#include "cvc5_private_library.h"
-
-#ifndef CVC5__UTIL__STATS_TIMER_H
-#define CVC5__UTIL__STATS_TIMER_H
-
-#include <chrono>
-
-#include "cvc4_export.h"
-#include "util/stats_base.h"
-
-namespace cvc5 {
-namespace timer_stat_detail {
-using clock = std::chrono::steady_clock;
-using time_point = clock::time_point;
-struct duration : public std::chrono::nanoseconds
-{
-};
-}  // namespace timer_stat_detail
-
-template <>
-void CVC4_EXPORT safe_print(int fd, const timer_stat_detail::duration& t);
-
-class CodeTimer;
-
-/**
- * A timer statistic.  The timer can be started and stopped
- * arbitrarily, like a stopwatch; the value of the statistic at the
- * end is the accumulated time over all (start,stop) pairs.
- */
-class CVC4_EXPORT TimerStat : public BackedStat<timer_stat_detail::duration>
-{
- public:
-  typedef cvc5::CodeTimer CodeTimer;
-
-  /**
-   * Construct a timer statistic with the given name.  Newly-constructed
-   * timers have a 0.0 value and are not running.
-   */
-  TimerStat(const std::string& name)
-      : BackedStat<timer_stat_detail::duration>(name,
-                                                timer_stat_detail::duration()),
-        d_start(),
-        d_running(false)
-  {
-  }
-
-  /** Start the timer. */
-  void start();
-
-  /**
-   * Stop the timer and update the statistic value with the
-   * accumulated time.
-   */
-  void stop();
-
-  /** If the timer is currently running */
-  bool running() const;
-
-  timer_stat_detail::duration get() const;
-
-  void flushInformation(std::ostream& out) const override;
-  void safeFlushInformation(int fd) const override;
-
-  SExpr getValue() const override;
-
- private:
-  /** The last start time of this timer */
-  timer_stat_detail::time_point d_start;
-
-  /** Whether this timer is currently running */
-  bool d_running;
-}; /* class TimerStat */
-
-/**
- * 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.
- */
-class CodeTimer
-{
- public:
-  CodeTimer(TimerStat& timer, bool allow_reentrant = false);
-  ~CodeTimer();
-
-private:
-  TimerStat& d_timer;
-  bool d_reentrant;
-
-  /** Private copy constructor undefined (no copy permitted). */
-  CodeTimer(const CodeTimer& timer) = delete;
-  /** Private assignment operator undefined (no copy permitted). */
-  CodeTimer& operator=(const CodeTimer& timer) = delete;
-}; /* class CodeTimer */
-
-}  // namespace cvc5
-
-#endif
diff --git a/src/util/stats_utils.cpp b/src/util/stats_utils.cpp
deleted file mode 100644
index e30266cbb..000000000
--- a/src/util/stats_utils.cpp
+++ /dev/null
@@ -1,37 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Gereon Kremer
- *
- * This file is part of the cvc5 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.
- * ****************************************************************************
- *
- * Statistic utilities.
- */
-
-#include "util/stats_utils.h"
-
-#include <chrono>
-#include <iomanip>
-#include <iostream>
-
-#include "util/ostream_util.h"
-#include "util/stats_timer.h"
-
-namespace cvc5 {
-
-std::ostream& operator<<(std::ostream& os,
-                         const timer_stat_detail::duration& dur)
-{
-  StreamFormatScope format_scope(os);
-
-  return os << (dur / std::chrono::seconds(1)) << "." << std::setfill('0')
-            << std::setw(9) << std::right
-            << (dur % std::chrono::seconds(1)).count();
-}
-
-}  // namespace cvc5
diff --git a/src/util/stats_utils.h b/src/util/stats_utils.h
deleted file mode 100644
index 41d191ea0..000000000
--- a/src/util/stats_utils.h
+++ /dev/null
@@ -1,36 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Gereon Kremer, Mathias Preiner
- *
- * This file is part of the cvc5 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.
- * ****************************************************************************
- *
- * Statistic utilities.
- */
-
-#include "cvc5_private_library.h"
-
-#ifndef CVC5__UTIL__STATS_UTILS_H
-#define CVC5__UTIL__STATS_UTILS_H
-
-#include <iosfwd>
-
-#include "cvc4_export.h"
-
-namespace cvc5 {
-
-namespace timer_stat_detail {
-struct duration;
-}
-
-std::ostream& operator<<(std::ostream& os,
-                         const timer_stat_detail::duration& dur) CVC4_EXPORT;
-
-}  // namespace cvc5
-
-#endif