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.

2 files changed, 57 insertions, 79 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 57b248ddf..7c7196822 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -24,14 +24,16 @@
 namespace cvc5 {
 namespace prop {
 
-BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name)
-: context::ContextNotifyObj(mainSatContext, false),
-  d_minisat(new BVMinisat::SimpSolver(mainSatContext)),
-  d_minisatNotify(nullptr),
-  d_assertionsCount(0),
-  d_assertionsRealCount(mainSatContext, 0),
-  d_lastPropagation(mainSatContext, 0),
-  d_statistics(registry, name)
+BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry& registry,
+                                       context::Context* mainSatContext,
+                                       const std::string& name)
+    : context::ContextNotifyObj(mainSatContext, false),
+      d_minisat(new BVMinisat::SimpSolver(mainSatContext)),
+      d_minisatNotify(nullptr),
+      d_assertionsCount(0),
+      d_assertionsRealCount(mainSatContext, 0),
+      d_lastPropagation(mainSatContext, 0),
+      d_statistics(registry, name)
 {
   d_statistics.init(d_minisat.get());
 }
@@ -227,58 +229,36 @@ void BVMinisatSatSolver::toSatClause(const BVMinisat::Clause& clause,
 
 // Satistics for BVMinisatSatSolver
 
-BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry,
+BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry& registry,
                                            const std::string& prefix)
-    : d_registry(registry),
-      d_statStarts(prefix + "::bvminisat::starts"),
-      d_statDecisions(prefix + "::bvminisat::decisions"),
-      d_statRndDecisions(prefix + "::bvminisat::rnd_decisions"),
-      d_statPropagations(prefix + "::bvminisat::propagations"),
-      d_statConflicts(prefix + "::bvminisat::conflicts"),
-      d_statClausesLiterals(prefix + "::bvminisat::clauses_literals"),
-      d_statLearntsLiterals(prefix + "::bvminisat::learnts_literals"),
-      d_statMaxLiterals(prefix + "::bvminisat::max_literals"),
-      d_statTotLiterals(prefix + "::bvminisat::tot_literals"),
-      d_statEliminatedVars(prefix + "::bvminisat::eliminated_vars"),
-      d_statCallsToSolve(prefix + "::bvminisat::calls_to_solve", 0),
-      d_statSolveTime(prefix + "::bvminisat::solve_time"),
-      d_registerStats(!prefix.empty())
+    : d_statStarts(
+        registry.registerReference<int64_t>(prefix + "bvminisat::starts")),
+      d_statDecisions(
+          registry.registerReference<int64_t>(prefix + "bvminisat::decisions")),
+      d_statRndDecisions(registry.registerReference<int64_t>(
+          prefix + "bvminisat::rnd_decisions")),
+      d_statPropagations(registry.registerReference<int64_t>(
+          prefix + "bvminisat::propagations")),
+      d_statConflicts(
+          registry.registerReference<int64_t>(prefix + "bvminisat::conflicts")),
+      d_statClausesLiterals(registry.registerReference<int64_t>(
+          prefix + "bvminisat::clauses_literals")),
+      d_statLearntsLiterals(registry.registerReference<int64_t>(
+          prefix + "bvminisat::learnts_literals")),
+      d_statMaxLiterals(registry.registerReference<int64_t>(
+          prefix + "bvminisat::max_literals")),
+      d_statTotLiterals(registry.registerReference<int64_t>(
+          prefix + "bvminisat::tot_literals")),
+      d_statEliminatedVars(registry.registerReference<int64_t>(
+          prefix + "bvminisat::eliminated_vars")),
+      d_statCallsToSolve(
+          registry.registerInt(prefix + "bvminisat::calls_to_solve")),
+      d_statSolveTime(registry.registerTimer(prefix + "bvminisat::solve_time"))
 {
   if (!d_registerStats)
   {
     return;
   }
-
-  d_registry->registerStat(&d_statStarts);
-  d_registry->registerStat(&d_statDecisions);
-  d_registry->registerStat(&d_statRndDecisions);
-  d_registry->registerStat(&d_statPropagations);
-  d_registry->registerStat(&d_statConflicts);
-  d_registry->registerStat(&d_statClausesLiterals);
-  d_registry->registerStat(&d_statLearntsLiterals);
-  d_registry->registerStat(&d_statMaxLiterals);
-  d_registry->registerStat(&d_statTotLiterals);
-  d_registry->registerStat(&d_statEliminatedVars);
-  d_registry->registerStat(&d_statCallsToSolve);
-  d_registry->registerStat(&d_statSolveTime);
-}
-
-BVMinisatSatSolver::Statistics::~Statistics() {
-  if (!d_registerStats){
-    return;
-  }
-  d_registry->unregisterStat(&d_statStarts);
-  d_registry->unregisterStat(&d_statDecisions);
-  d_registry->unregisterStat(&d_statRndDecisions);
-  d_registry->unregisterStat(&d_statPropagations);
-  d_registry->unregisterStat(&d_statConflicts);
-  d_registry->unregisterStat(&d_statClausesLiterals);
-  d_registry->unregisterStat(&d_statLearntsLiterals);
-  d_registry->unregisterStat(&d_statMaxLiterals);
-  d_registry->unregisterStat(&d_statTotLiterals);
-  d_registry->unregisterStat(&d_statEliminatedVars);
-  d_registry->unregisterStat(&d_statCallsToSolve);
-  d_registry->unregisterStat(&d_statSolveTime);
 }
 
 void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index b41a9b836..9d363224f 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -26,8 +26,7 @@
 #include "prop/bvminisat/simp/SimpSolver.h"
 #include "prop/sat_solver.h"
 #include "util/resource_manager.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace prop {
@@ -68,19 +67,20 @@ protected:
  void contextNotifyPop() override;
 
 public:
+ BVMinisatSatSolver(StatisticsRegistry& registry,
+                    context::Context* mainSatContext,
+                    const std::string& name = "");
+ virtual ~BVMinisatSatSolver();
 
-  BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = "");
-  virtual ~BVMinisatSatSolver();
+ void setNotify(BVSatSolverNotify* notify) override;
 
-  void setNotify(BVSatSolverNotify* notify) override;
+ ClauseId addClause(SatClause& clause, bool removable) override;
 
-  ClauseId addClause(SatClause& clause, bool removable) override;
-
-  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
-  {
-    Unreachable() << "Minisat does not support native XOR reasoning";
-    return ClauseIdError;
-  }
+ ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
+ {
+   Unreachable() << "Minisat does not support native XOR reasoning";
+   return ClauseIdError;
+ }
 
   SatValue propagate() override;
 
@@ -130,19 +130,17 @@ public:
 
   class Statistics {
   public:
-    StatisticsRegistry* d_registry;
-    ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
-    ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
-    ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
-    ReferenceStat<uint64_t> d_statLearntsLiterals,  d_statMaxLiterals;
-    ReferenceStat<uint64_t> d_statTotLiterals;
-    ReferenceStat<int> d_statEliminatedVars;
-    IntStat d_statCallsToSolve;
-    TimerStat d_statSolveTime;
-    bool d_registerStats;
-    Statistics(StatisticsRegistry* registry, const std::string& prefix);
-    ~Statistics();
-    void init(BVMinisat::SimpSolver* minisat);
+   ReferenceStat<int64_t> d_statStarts, d_statDecisions;
+   ReferenceStat<int64_t> d_statRndDecisions, d_statPropagations;
+   ReferenceStat<int64_t> d_statConflicts, d_statClausesLiterals;
+   ReferenceStat<int64_t> d_statLearntsLiterals, d_statMaxLiterals;
+   ReferenceStat<int64_t> d_statTotLiterals;
+   ReferenceStat<int64_t> d_statEliminatedVars;
+   IntStat d_statCallsToSolve;
+   TimerStat d_statSolveTime;
+   bool d_registerStats;
+   Statistics(StatisticsRegistry& registry, const std::string& prefix);
+   void init(BVMinisat::SimpSolver* minisat);
   };
 
   Statistics d_statistics;