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.

7 files changed, 51 insertions, 86 deletions

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index b45ccbac3..25f87de2c 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1748,23 +1748,16 @@ void CardinalityExtension::checkCombinedCardinality()
 }
 
 CardinalityExtension::Statistics::Statistics()
-    : d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0),
-      d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0),
-      d_split_lemmas("CardinalityExtension::Split_Lemmas", 0),
-      d_max_model_size("CardinalityExtension::Max_Model_Size", 1)
+    : d_clique_conflicts(smtStatisticsRegistry().registerInt(
+        "CardinalityExtension::Clique_Conflicts")),
+      d_clique_lemmas(smtStatisticsRegistry().registerInt(
+          "CardinalityExtension::Clique_Lemmas")),
+      d_split_lemmas(smtStatisticsRegistry().registerInt(
+          "CardinalityExtension::Split_Lemmas")),
+      d_max_model_size(smtStatisticsRegistry().registerInt(
+          "CardinalityExtension::Max_Model_Size"))
 {
-  smtStatisticsRegistry()->registerStat(&d_clique_conflicts);
-  smtStatisticsRegistry()->registerStat(&d_clique_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_split_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_max_model_size);
-}
-
-CardinalityExtension::Statistics::~Statistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts);
-  smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
+  d_max_model_size.maxAssign(1);
 }
 
 }  // namespace uf
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 53c850897..70db9257f 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -22,7 +22,7 @@
 #include "context/context.h"
 #include "theory/decision_strategy.h"
 #include "theory/theory.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -397,7 +397,6 @@ class CardinalityExtension
     IntStat d_split_lemmas;
     IntStat d_max_model_size;
     Statistics();
-    ~Statistics();
   };
   /** statistics class */
   Statistics d_statistics;
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index fe7b0ab84..7124a8890 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -29,23 +29,14 @@ namespace cvc5 {
 namespace theory {
 namespace eq {
 
-EqualityEngine::Statistics::Statistics(std::string name)
-    : d_mergesCount(name + "::mergesCount", 0),
-      d_termsCount(name + "::termsCount", 0),
-      d_functionTermsCount(name + "::functionTermsCount", 0),
-      d_constantTermsCount(name + "::constantTermsCount", 0)
+EqualityEngine::Statistics::Statistics(const std::string& name)
+    : d_mergesCount(smtStatisticsRegistry().registerInt(name + "mergesCount")),
+      d_termsCount(smtStatisticsRegistry().registerInt(name + "termsCount")),
+      d_functionTermsCount(
+          smtStatisticsRegistry().registerInt(name + "functionTermsCount")),
+      d_constantTermsCount(
+          smtStatisticsRegistry().registerInt(name + "constantTermsCount"))
 {
-  smtStatisticsRegistry()->registerStat(&d_mergesCount);
-  smtStatisticsRegistry()->registerStat(&d_termsCount);
-  smtStatisticsRegistry()->registerStat(&d_functionTermsCount);
-  smtStatisticsRegistry()->registerStat(&d_constantTermsCount);
-}
-
-EqualityEngine::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_mergesCount);
-  smtStatisticsRegistry()->unregisterStat(&d_termsCount);
-  smtStatisticsRegistry()->unregisterStat(&d_functionTermsCount);
-  smtStatisticsRegistry()->unregisterStat(&d_constantTermsCount);
 }
 
 /**
@@ -128,7 +119,7 @@ EqualityEngine::EqualityEngine(context::Context* context,
       d_assertedEqualitiesCount(context, 0),
       d_equalityTriggersCount(context, 0),
       d_subtermEvaluatesSize(context, 0),
-      d_stats(name),
+      d_stats(name + "::"),
       d_inPropagate(false),
       d_constantsAreTriggers(constantsAreTriggers),
       d_anyTermsAreTriggers(anyTermTriggers),
@@ -158,7 +149,7 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify,
       d_assertedEqualitiesCount(context, 0),
       d_equalityTriggersCount(context, 0),
       d_subtermEvaluatesSize(context, 0),
-      d_stats(name),
+      d_stats(name + "::"),
       d_inPropagate(false),
       d_constantsAreTriggers(constantsAreTriggers),
       d_anyTermsAreTriggers(anyTermTriggers),
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index d8a8f3916..8676e446e 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -34,7 +34,7 @@
 #include "theory/uf/equality_engine_iterator.h"
 #include "theory/uf/equality_engine_notify.h"
 #include "theory/uf/equality_engine_types.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -109,9 +109,7 @@ class EqualityEngine : public context::ContextNotifyObj {
     /** Number of constant terms managed by the system */
     IntStat d_constantTermsCount;
 
-    Statistics(std::string name);
-
-    ~Statistics();
+    Statistics(const std::string& name);
   };/* struct EqualityEngine::statistics */
 
 private:
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index 49b056f5a..65ed4d542 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -164,21 +164,20 @@ void SymmetryBreaker::Template::reset() {
   d_reps.clear();
 }
 
-SymmetryBreaker::SymmetryBreaker(context::Context* context,
-                                 std::string name) :
-  ContextNotifyObj(context),
-  d_assertionsToRerun(context),
-  d_rerunningAssertions(false),
-  d_phi(),
-  d_phiSet(),
-  d_permutations(),
-  d_terms(),
-  d_template(),
-  d_normalizationCache(),
-  d_termEqs(),
-  d_termEqsOnly(),
-  d_name(name),
-  d_stats(d_name)
+SymmetryBreaker::SymmetryBreaker(context::Context* context, std::string name)
+    : ContextNotifyObj(context),
+      d_assertionsToRerun(context),
+      d_rerunningAssertions(false),
+      d_phi(),
+      d_phiSet(),
+      d_permutations(),
+      d_terms(),
+      d_template(),
+      d_normalizationCache(),
+      d_termEqs(),
+      d_termEqsOnly(),
+      d_name(name),
+      d_stats(d_name + "theory::uf::symmetry_breaker::")
 {
 }
 
@@ -750,33 +749,20 @@ void SymmetryBreaker::selectTerms(const Permutation& p) {
   }
 }
 
-SymmetryBreaker::Statistics::Statistics(std::string name)
-  : d_clauses(name + "theory::uf::symmetry_breaker::clauses", 0)
-  , d_units(name + "theory::uf::symmetry_breaker::units", 0)
-  , d_permutationSetsConsidered(name + "theory::uf::symmetry_breaker::permutationSetsConsidered", 0)
-  , d_permutationSetsInvariant(name + "theory::uf::symmetry_breaker::permutationSetsInvariant", 0)
-  , d_invariantByPermutationsTimer(name + "theory::uf::symmetry_breaker::timers::invariantByPermutations")
-  , d_selectTermsTimer(name + "theory::uf::symmetry_breaker::timers::selectTerms")
-  , d_initNormalizationTimer(name + "theory::uf::symmetry_breaker::timers::initNormalization")
-{
-  smtStatisticsRegistry()->registerStat(&d_clauses);
-  smtStatisticsRegistry()->registerStat(&d_units);
-  smtStatisticsRegistry()->registerStat(&d_permutationSetsConsidered);
-  smtStatisticsRegistry()->registerStat(&d_permutationSetsInvariant);
-  smtStatisticsRegistry()->registerStat(&d_invariantByPermutationsTimer);
-  smtStatisticsRegistry()->registerStat(&d_selectTermsTimer);
-  smtStatisticsRegistry()->registerStat(&d_initNormalizationTimer);
-}
-
-SymmetryBreaker::Statistics::~Statistics()
+SymmetryBreaker::Statistics::Statistics(const std::string& name)
+    : d_clauses(smtStatisticsRegistry().registerInt(name + "clauses")),
+      d_units(smtStatisticsRegistry().registerInt(name + "units")),
+      d_permutationSetsConsidered(smtStatisticsRegistry().registerInt(
+          name + "permutationSetsConsidered")),
+      d_permutationSetsInvariant(smtStatisticsRegistry().registerInt(
+          name + "permutationSetsInvariant")),
+      d_invariantByPermutationsTimer(smtStatisticsRegistry().registerTimer(
+          name + "timers::invariantByPermutations")),
+      d_selectTermsTimer(
+          smtStatisticsRegistry().registerTimer(name + "timers::selectTerms")),
+      d_initNormalizationTimer(smtStatisticsRegistry().registerTimer(
+          name + "timers::initNormalization"))
 {
-  smtStatisticsRegistry()->unregisterStat(&d_clauses);
-  smtStatisticsRegistry()->unregisterStat(&d_units);
-  smtStatisticsRegistry()->unregisterStat(&d_permutationSetsConsidered);
-  smtStatisticsRegistry()->unregisterStat(&d_permutationSetsInvariant);
-  smtStatisticsRegistry()->unregisterStat(&d_invariantByPermutationsTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_selectTermsTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_initNormalizationTimer);
 }
 
 SymmetryBreaker::Terms::iterator
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index eb78f9101..b5d0fbdf9 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -52,8 +52,7 @@
 #include "expr/node.h"
 #include "expr/node_builder.h"
 #include "smt/smt_statistics_registry.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -147,8 +146,7 @@ private:
     /** time spent in initial round of normalization */
     TimerStat d_initNormalizationTimer;
 
-    Statistics(std::string name);
-    ~Statistics();
+    Statistics(const std::string& name);
   };
 
   Statistics d_stats;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 9fa86f402..5d91faa87 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -53,7 +53,7 @@ TheoryUF::TheoryUF(context::Context* c,
       d_functionsTerms(c),
       d_symb(u, instanceName),
       d_state(c, u, valuation),
-      d_im(*this, d_state, pnm, "theory::uf", false),
+      d_im(*this, d_state, pnm, "theory::uf::" + instanceName, false),
       d_notify(d_im, *this)
 {
   d_true = NodeManager::currentNM()->mkConst( true );