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.

1 files changed, 14 insertions, 25 deletions

diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index d5ce5ab79..b1f35821f 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -26,32 +26,21 @@ namespace cvc5 {
 namespace theory {
 
 EngineOutputChannel::Statistics::Statistics(theory::TheoryId theory)
-    : conflicts(getStatsPrefix(theory) + "::conflicts", 0),
-      propagations(getStatsPrefix(theory) + "::propagations", 0),
-      lemmas(getStatsPrefix(theory) + "::lemmas", 0),
-      requirePhase(getStatsPrefix(theory) + "::requirePhase", 0),
-      restartDemands(getStatsPrefix(theory) + "::restartDemands", 0),
-      trustedConflicts(getStatsPrefix(theory) + "::trustedConflicts", 0),
-      trustedLemmas(getStatsPrefix(theory) + "::trustedLemmas", 0)
+    : conflicts(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+                                                    + "conflicts")),
+      propagations(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+                                                       + "propagations")),
+      lemmas(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+                                                 + "lemmas")),
+      requirePhase(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+                                                       + "requirePhase")),
+      restartDemands(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+                                                         + "restartDemands")),
+      trustedConflicts(smtStatisticsRegistry().registerInt(
+          getStatsPrefix(theory) + "trustedConflicts")),
+      trustedLemmas(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+                                                        + "trustedLemmas"))
 {
-  smtStatisticsRegistry()->registerStat(&conflicts);
-  smtStatisticsRegistry()->registerStat(&propagations);
-  smtStatisticsRegistry()->registerStat(&lemmas);
-  smtStatisticsRegistry()->registerStat(&requirePhase);
-  smtStatisticsRegistry()->registerStat(&restartDemands);
-  smtStatisticsRegistry()->registerStat(&trustedConflicts);
-  smtStatisticsRegistry()->registerStat(&trustedLemmas);
-}
-
-EngineOutputChannel::Statistics::~Statistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&conflicts);
-  smtStatisticsRegistry()->unregisterStat(&propagations);
-  smtStatisticsRegistry()->unregisterStat(&lemmas);
-  smtStatisticsRegistry()->unregisterStat(&requirePhase);
-  smtStatisticsRegistry()->unregisterStat(&restartDemands);
-  smtStatisticsRegistry()->unregisterStat(&trustedConflicts);
-  smtStatisticsRegistry()->unregisterStat(&trustedLemmas);
 }
 
 EngineOutputChannel::EngineOutputChannel(TheoryEngine* engine,