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.

12 files changed, 83 insertions, 106 deletions

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 38e93f38e..d079682c5 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -25,6 +25,7 @@
 #include "smt/smt_engine_stats.h"
 #include "theory/rewriter.h"
 #include "util/resource_manager.h"
+#include "util/statistics_registry.h"
 
 using namespace cvc5::smt;
 
diff --git a/src/smt/env.h b/src/smt/env.h
index c2e0a8f54..09e3238ac 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -23,7 +23,6 @@
 
 #include "options/options.h"
 #include "theory/logic_info.h"
-#include "util/statistics.h"
 #include "util/statistics_registry.h"
 
 namespace cvc5 {
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 105376719..16b7f560b 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -1101,25 +1101,18 @@ bool ProofPostprocessCallback::addToTransChildren(Node eq,
 
 ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
     ProofNodeManager* pnm)
-    : d_ruleCount("finalProof::ruleCount"),
-      d_totalRuleCount("finalProof::totalRuleCount", 0),
-      d_minPedanticLevel("finalProof::minPedanticLevel", 10),
-      d_numFinalProofs("finalProofs::numFinalProofs", 0),
+    : d_ruleCount(smtStatisticsRegistry().registerHistogram<PfRule>(
+        "finalProof::ruleCount")),
+      d_totalRuleCount(
+          smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")),
+      d_minPedanticLevel(
+          smtStatisticsRegistry().registerInt("finalProof::minPedanticLevel")),
+      d_numFinalProofs(
+          smtStatisticsRegistry().registerInt("finalProofs::numFinalProofs")),
       d_pnm(pnm),
       d_pedanticFailure(false)
 {
-  smtStatisticsRegistry()->registerStat(&d_ruleCount);
-  smtStatisticsRegistry()->registerStat(&d_totalRuleCount);
-  smtStatisticsRegistry()->registerStat(&d_minPedanticLevel);
-  smtStatisticsRegistry()->registerStat(&d_numFinalProofs);
-}
-
-ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_ruleCount);
-  smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount);
-  smtStatisticsRegistry()->unregisterStat(&d_minPedanticLevel);
-  smtStatisticsRegistry()->unregisterStat(&d_numFinalProofs);
+  d_minPedanticLevel += 10;
 }
 
 void ProofPostprocessFinalCallback::initializeUpdate()
diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index d66641a69..72fa3581d 100644
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -19,12 +19,12 @@
 #define CVC5__SMT__PROOF_POST_PROCESSOR_H
 
 #include <map>
+#include <sstream>
 #include <unordered_set>
 
 #include "expr/proof_node_updater.h"
 #include "smt/witness_form.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 
@@ -241,7 +241,6 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
 {
  public:
   ProofPostprocessFinalCallback(ProofNodeManager* pnm);
-  ~ProofPostprocessFinalCallback();
   /**
    * Initialize, called once for each new ProofNode to process. This initializes
    * static information to be used by successive calls to update.
@@ -256,7 +255,7 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
 
  private:
   /** Counts number of postprocessed proof nodes for each kind of proof rule */
-  IntegralHistogramStat<PfRule> d_ruleCount;
+  HistogramStat<PfRule> d_ruleCount;
   /** Total number of postprocessed rule applications */
   IntStat d_totalRuleCount;
   /** The minimum pedantic level of any rule encountered */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3d38ba37b..d3347b019 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -66,6 +66,7 @@
 #include "theory/theory_engine.h"
 #include "util/random.h"
 #include "util/resource_manager.h"
+#include "util/statistics_registry.h"
 
 // required for hacks related to old proofs for unsat cores
 #include "base/configuration.h"
@@ -412,7 +413,8 @@ LogicInfo SmtEngine::getUserLogicInfo() const
 void SmtEngine::notifyStartParsing(const std::string& filename)
 {
   d_state->setFilename(filename);
-  d_stats->d_driverFilename.set(filename);
+  d_env->getStatisticsRegistry().registerValue<std::string>("driver::filename",
+                                                            filename);
   // Copy the original options. This is called prior to beginning parsing.
   // Hence reset should revert to these options, which note is after reading
   // the command line.
@@ -424,11 +426,12 @@ const std::string& SmtEngine::getFilename() const
 }
 
 void SmtEngine::setResultStatistic(const std::string& result) {
-    d_stats->d_driverResult.set(result);
+  d_env->getStatisticsRegistry().registerValue<std::string>("driver::sat/unsat",
+                                                            result);
 }
-
 void SmtEngine::setTotalTimeStatistic(double seconds) {
-  d_stats->d_driverTotalTime.set(seconds);
+  d_env->getStatisticsRegistry().registerValue<double>("driver::totalTime",
+                                                       seconds);
 }
 
 void SmtEngine::setLogicInternal()
@@ -516,11 +519,13 @@ cvc5::SExpr SmtEngine::getInfo(const std::string& key) const
   if (key == "all-statistics")
   {
     vector<SExpr> stats;
-    for (const auto& s: d_env->getStatisticsRegistry())
+    for (const auto& s : d_env->getStatisticsRegistry())
     {
+      std::stringstream ss;
+      ss << *s.second;
       vector<SExpr> v;
       v.push_back(s.first);
-      v.push_back(s.second);
+      v.push_back(ss.str());
       stats.push_back(v);
     }
     return SExpr(stats);
@@ -1866,24 +1871,28 @@ NodeManager* SmtEngine::getNodeManager() const
   return d_env->getNodeManager();
 }
 
-Statistics SmtEngine::getStatistics() const
-{
-  return Statistics(d_env->getStatisticsRegistry());
-}
-
 SExpr SmtEngine::getStatistic(std::string name) const
 {
-  return d_env->getStatisticsRegistry().getStatistic(name);
+  const auto* val = d_env->getStatisticsRegistry().get(name);
+  std::stringstream ss;
+  ss << *val;
+  return SExpr({SExpr(name), SExpr(ss.str())});
 }
 
 void SmtEngine::printStatistics(std::ostream& out) const
 {
-  d_env->getStatisticsRegistry().flushInformation(out);
+  d_env->getStatisticsRegistry().print(out);
 }
 
 void SmtEngine::printStatisticsSafe(int fd) const
 {
-  d_env->getStatisticsRegistry().safeFlushInformation(fd);
+  d_env->getStatisticsRegistry().printSafe(fd);
+}
+
+void SmtEngine::printStatisticsDiff(std::ostream& out) const
+{
+  d_env->getStatisticsRegistry().printDiff(out);
+  d_env->getStatisticsRegistry().storeSnapshot();
 }
 
 void SmtEngine::setUserAttribute(const std::string& attr,
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index ec2699c31..5947367f2 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -31,7 +31,6 @@
 #include "theory/logic_info.h"
 #include "util/result.h"
 #include "util/sexpr.h"
-#include "util/statistics.h"
 
 namespace cvc5 {
 
@@ -827,22 +826,30 @@ class CVC4_EXPORT SmtEngine
   /** Permit access to the underlying NodeManager. */
   NodeManager* getNodeManager() const;
 
-  /** Export statistics from this SmtEngine. */
-  Statistics getStatistics() const;
-
   /** Get the value of one named statistic from this SmtEngine. */
   SExpr getStatistic(std::string name) const;
 
-  /** Flush statistics from this SmtEngine and the NodeManager it uses. */
+  /**
+   * Print statistics from the statistics registry in the env object owned by
+   * this SmtEngine.
+   */
   void printStatistics(std::ostream& out) const;
 
   /**
-   * Flush statistics from this SmtEngine and the NodeManager it uses. Safe to
-   * use in a signal handler.
+   * Print statistics from the statistics registry in the env object owned by
+   * this SmtEngine. Safe to use in a signal handler.
    */
   void printStatisticsSafe(int fd) const;
 
   /**
+   * Print the changes to the statistics from the statistics registry in the
+   * env object owned by this SmtEngine since this method was called the last
+   * time. Internally prints the diff and then stores a snapshot for the next
+   * call.
+   */
+  void printStatisticsDiff(std::ostream&) const;
+
+  /**
    * Set user attribute.
    * This function is called when an attribute is set by a user.
    * In SMT-LIBv2 this is done via the syntax (! expr :attr)
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 1164bc1b5..962529924 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -61,9 +61,10 @@ SmtScope::~SmtScope() {
                    << std::endl;
 }
 
-StatisticsRegistry* SmtScope::currentStatisticsRegistry() {
+StatisticsRegistry& SmtScope::currentStatisticsRegistry()
+{
   Assert(smtEngineInScope());
-  return &(s_smtEngine_current->getStatisticsRegistry());
+  return s_smtEngine_current->getStatisticsRegistry();
 }
 
 }  // namespace smt
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index a1d660adf..76bc5c641 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -51,7 +51,7 @@ class SmtScope : public NodeManagerScope
    * This returns the StatisticsRegistry attached to the currently in scope
    * SmtEngine.
    */
-  static StatisticsRegistry* currentStatisticsRegistry();
+  static StatisticsRegistry& currentStatisticsRegistry();
 
  private:
   /** The old SmtEngine, to be restored on destruction. */
diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp
index 5147c046a..417d345cb 100644
--- a/src/smt/smt_engine_stats.cpp
+++ b/src/smt/smt_engine_stats.cpp
@@ -20,54 +20,29 @@
 namespace cvc5 {
 namespace smt {
 
-SmtEngineStatistics::SmtEngineStatistics()
-    : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
-      d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
-      d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
-      d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
-      d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
-      d_checkModelTime("smt::SmtEngine::checkModelTime"),
-      d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
-      d_solveTime("smt::SmtEngine::solveTime"),
-      d_pushPopTime("smt::SmtEngine::pushPopTime"),
-      d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
-      d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
-      d_driverFilename("driver::filename", ""),
-      d_driverResult("driver::sat/unsat", ""),
-      d_driverTotalTime("driver::totalTime", 0.0)
+SmtEngineStatistics::SmtEngineStatistics(const std::string& name)
+    : d_definitionExpansionTime(smtStatisticsRegistry().registerTimer(
+        name + "definitionExpansionTime")),
+      d_numConstantProps(
+          smtStatisticsRegistry().registerInt(name + "numConstantProps")),
+      d_cnfConversionTime(
+          smtStatisticsRegistry().registerTimer(name + "cnfConversionTime")),
+      d_numAssertionsPre(smtStatisticsRegistry().registerInt(
+          name + "numAssertionsPreITERemoval")),
+      d_numAssertionsPost(smtStatisticsRegistry().registerInt(
+          name + "numAssertionsPostITERemoval")),
+      d_checkModelTime(
+          smtStatisticsRegistry().registerTimer(name + "checkModelTime")),
+      d_checkUnsatCoreTime(
+          smtStatisticsRegistry().registerTimer(name + "checkUnsatCoreTime")),
+      d_solveTime(smtStatisticsRegistry().registerTimer(name + "solveTime")),
+      d_pushPopTime(
+          smtStatisticsRegistry().registerTimer(name + "pushPopTime")),
+      d_processAssertionsTime(smtStatisticsRegistry().registerTimer(
+          name + "processAssertionsTime")),
+      d_simplifiedToFalse(
+          smtStatisticsRegistry().registerInt(name + "simplifiedToFalse"))
 {
-  smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
-  smtStatisticsRegistry()->registerStat(&d_numConstantProps);
-  smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
-  smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
-  smtStatisticsRegistry()->registerStat(&d_numAssertionsPost);
-  smtStatisticsRegistry()->registerStat(&d_checkModelTime);
-  smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime);
-  smtStatisticsRegistry()->registerStat(&d_solveTime);
-  smtStatisticsRegistry()->registerStat(&d_pushPopTime);
-  smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
-  smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
-  smtStatisticsRegistry()->registerStat(&d_driverFilename);
-  smtStatisticsRegistry()->registerStat(&d_driverResult);
-  smtStatisticsRegistry()->registerStat(&d_driverTotalTime);
-}
-
-SmtEngineStatistics::~SmtEngineStatistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
-  smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
-  smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
-  smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
-  smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost);
-  smtStatisticsRegistry()->unregisterStat(&d_checkModelTime);
-  smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime);
-  smtStatisticsRegistry()->unregisterStat(&d_solveTime);
-  smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
-  smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
-  smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
-  smtStatisticsRegistry()->unregisterStat(&d_driverFilename);
-  smtStatisticsRegistry()->unregisterStat(&d_driverResult);
-  smtStatisticsRegistry()->unregisterStat(&d_driverTotalTime);
 }
 
 }  // namespace smt
diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h
index d2bece92f..441721a54 100644
--- a/src/smt/smt_engine_stats.h
+++ b/src/smt/smt_engine_stats.h
@@ -18,16 +18,14 @@
 #ifndef CVC5__SMT__SMT_ENGINE_STATS_H
 #define CVC5__SMT__SMT_ENGINE_STATS_H
 
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace smt {
 
 struct SmtEngineStatistics
 {
-  SmtEngineStatistics();
-  ~SmtEngineStatistics();
+  SmtEngineStatistics(const std::string& name = "smt::SmtEngine::");
   /** time spent in definition-expansion */
   TimerStat d_definitionExpansionTime;
   /** number of constant propagations found during nonclausal simp */
@@ -51,13 +49,6 @@ struct SmtEngineStatistics
 
   /** Has something simplified to false? */
   IntStat d_simplifiedToFalse;
-
-  /** Name of the input file */
-  BackedStat<std::string> d_driverFilename;
-  /** Result of the last check */
-  BackedStat<std::string> d_driverResult;
-  /** Total time of the current run */
-  BackedStat<double> d_driverTotalTime;
 }; /* struct SmtEngineStatistics */
 
 }  // namespace smt
diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp
index db437526a..bb1cfc9fa 100644
--- a/src/smt/smt_statistics_registry.cpp
+++ b/src/smt/smt_statistics_registry.cpp
@@ -16,11 +16,12 @@
 #include "smt/smt_statistics_registry.h"
 
 #include "smt/smt_engine_scope.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 
-StatisticsRegistry* smtStatisticsRegistry() {
+StatisticsRegistry& smtStatisticsRegistry()
+{
   return smt::SmtScope::currentStatisticsRegistry();
 }
 
diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h
index d8adde3c3..31f55375c 100644
--- a/src/smt/smt_statistics_registry.h
+++ b/src/smt/smt_statistics_registry.h
@@ -18,6 +18,7 @@
 #pragma once
 
 #include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 
@@ -25,6 +26,6 @@ namespace cvc5 {
  * This returns the StatisticsRegistry attached to the currently in scope
  * SmtEngine. This is a synonym for smt::SmtScope::currentStatisticsRegistry().
  */
-StatisticsRegistry* smtStatisticsRegistry();
+StatisticsRegistry& smtStatisticsRegistry();
 
 }  // namespace cvc5