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