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.

3 files changed, 30 insertions, 45 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 9b6a6c658..9c32abc56 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -72,7 +72,7 @@ void ProofManager::initSatProof(Minisat::Solver* solver)
   // Destroy old instance before initializing new one to avoid issues with
   // registering stats
   d_satProof.reset();
-  d_satProof.reset(new CoreSatProof(solver, d_context, ""));
+  d_satProof.reset(new CoreSatProof(solver, d_context, "satproof::"));
 }
 
 void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index c55599584..b85d0bc08 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -29,8 +29,7 @@
 #include "expr/node.h"
 #include "proof/clause_id.h"
 #include "proof/proof_manager.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
 
 // Forward declarations.
 namespace cvc5 {
@@ -214,7 +213,6 @@ class TSatProof {
    * hasResolution(id) does not hold. */
   const ResolutionChain& getResolutionChain(ClauseId id) const;
 
-  const std::string& getName() const { return d_name; }
   const ClauseId& getEmptyClauseId() const { return d_emptyClauseId; }
   const IdSet& getSeenLearnt() const { return d_seenLearnt; }
   const IdToConflicts& getAssumptionConflicts() const
@@ -285,16 +283,13 @@ class TSatProof {
     IntStat d_numLearnedInProof;
     IntStat d_numLemmasInProof;
     AverageStat d_avgChainLength;
-    IntegralHistogramStat<uint64_t> d_resChainLengths;
-    IntegralHistogramStat<uint64_t> d_usedResChainLengths;
-    IntegralHistogramStat<uint64_t> d_clauseGlue;
-    IntegralHistogramStat<uint64_t> d_usedClauseGlue;
+    HistogramStat<uint64_t> d_resChainLengths;
+    HistogramStat<uint64_t> d_usedResChainLengths;
+    HistogramStat<uint64_t> d_clauseGlue;
+    HistogramStat<uint64_t> d_usedClauseGlue;
     Statistics(const std::string& name);
-    ~Statistics();
   };
 
-  std::string d_name;
-
   const ClauseId d_emptyClauseId;
   IdSet d_seenLearnt;
   IdToConflicts d_assumptionConflictsDebug;
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 686265326..c411ae741 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -182,10 +182,11 @@ void ResChain<Solver>::addRedundantLit(typename Solver::TLit lit) {
 
 /// SatProof
 template <class Solver>
-TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context,
-                             const std::string& name, bool checkRes)
-    : d_name(name),
-      d_emptyClauseId(ClauseIdEmpty),
+TSatProof<Solver>::TSatProof(Solver* solver,
+                             context::Context* context,
+                             const std::string& name,
+                             bool checkRes)
+    : d_emptyClauseId(ClauseIdEmpty),
       d_seenLearnt(),
       d_assumptionConflictsDebug(),
       d_solver(solver),
@@ -211,7 +212,8 @@ TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context,
       d_seenInputs(),
       d_seenLemmas(),
       d_satProofConstructed(false),
-      d_statistics(name) {
+      d_statistics(name)
+{
 }
 
 template <class Solver>
@@ -1008,35 +1010,23 @@ void TSatProof<Solver>::storeClauseGlue(ClauseId clause, int glue) {
 
 template <class Solver>
 TSatProof<Solver>::Statistics::Statistics(const std::string& prefix)
-    : d_numLearnedClauses("satproof::" + prefix + "::NumLearnedClauses", 0),
-      d_numLearnedInProof("satproof::" + prefix + "::NumLearnedInProof", 0),
-      d_numLemmasInProof("satproof::" + prefix + "::NumLemmasInProof", 0),
-      d_avgChainLength("satproof::" + prefix + "::AvgResChainLength"),
-      d_resChainLengths("satproof::" + prefix + "::ResChainLengthsHist"),
-      d_usedResChainLengths("satproof::" + prefix +
-                            "::UsedResChainLengthsHist"),
-      d_clauseGlue("satproof::" + prefix + "::ClauseGlueHist"),
-      d_usedClauseGlue("satproof::" + prefix + "::UsedClauseGlueHist") {
-  smtStatisticsRegistry()->registerStat(&d_numLearnedClauses);
-  smtStatisticsRegistry()->registerStat(&d_numLearnedInProof);
-  smtStatisticsRegistry()->registerStat(&d_numLemmasInProof);
-  smtStatisticsRegistry()->registerStat(&d_avgChainLength);
-  smtStatisticsRegistry()->registerStat(&d_resChainLengths);
-  smtStatisticsRegistry()->registerStat(&d_usedResChainLengths);
-  smtStatisticsRegistry()->registerStat(&d_clauseGlue);
-  smtStatisticsRegistry()->registerStat(&d_usedClauseGlue);
-}
-
-template <class Solver>
-TSatProof<Solver>::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_numLearnedClauses);
-  smtStatisticsRegistry()->unregisterStat(&d_numLearnedInProof);
-  smtStatisticsRegistry()->unregisterStat(&d_numLemmasInProof);
-  smtStatisticsRegistry()->unregisterStat(&d_avgChainLength);
-  smtStatisticsRegistry()->unregisterStat(&d_resChainLengths);
-  smtStatisticsRegistry()->unregisterStat(&d_usedResChainLengths);
-  smtStatisticsRegistry()->unregisterStat(&d_clauseGlue);
-  smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue);
+    : d_numLearnedClauses(
+        smtStatisticsRegistry().registerInt(prefix + "NumLearnedClauses")),
+      d_numLearnedInProof(
+          smtStatisticsRegistry().registerInt(prefix + "NumLearnedInProof")),
+      d_numLemmasInProof(
+          smtStatisticsRegistry().registerInt(prefix + "NumLemmasInProof")),
+      d_avgChainLength(smtStatisticsRegistry().registerAverage(
+          prefix + "AvgResChainLength")),
+      d_resChainLengths(smtStatisticsRegistry().registerHistogram<uint64_t>(
+          prefix + "ResChainLengthsHist")),
+      d_usedResChainLengths(smtStatisticsRegistry().registerHistogram<uint64_t>(
+          prefix + "UsedResChainLengthsHist")),
+      d_clauseGlue(smtStatisticsRegistry().registerHistogram<uint64_t>(
+          prefix + "ClauseGlueHist")),
+      d_usedClauseGlue(smtStatisticsRegistry().registerHistogram<uint64_t>(
+          prefix + "UsedClauseGlueHist"))
+{
 }
 
 inline std::ostream& operator<<(std::ostream& out, cvc5::ClauseKind k)