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, 23 insertions, 26 deletions

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 164b9b058..4dc7201fb 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -43,26 +43,31 @@ Info::~Info() {
   in_stores->deleteSelf();
 }
 
-ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b, std::string statisticsPrefix)
-    : ct(c), bck(b), info_map(),
-      d_mergeInfoTimer(statisticsPrefix + "theory::arrays::mergeInfoTimer"),
-      d_avgIndexListLength(statisticsPrefix + "theory::arrays::avgIndexListLength"),
-      d_avgStoresListLength(statisticsPrefix + "theory::arrays::avgStoresListLength"),
-      d_avgInStoresListLength(statisticsPrefix + "theory::arrays::avgInStoresListLength"),
-      d_listsCount(statisticsPrefix + "theory::arrays::listsCount",0),
-      d_callsMergeInfo(statisticsPrefix + "theory::arrays::callsMergeInfo",0),
-      d_maxList(statisticsPrefix + "theory::arrays::maxList",0),
-      d_tableSize(statisticsPrefix + "theory::arrays::infoTableSize", info_map) {
+ArrayInfo::ArrayInfo(context::Context* c,
+                     Backtracker<TNode>* b,
+                     std::string statisticsPrefix)
+    : ct(c),
+      bck(b),
+      info_map(),
+      d_mergeInfoTimer(smtStatisticsRegistry().registerTimer(
+          statisticsPrefix + "mergeInfoTimer")),
+      d_avgIndexListLength(smtStatisticsRegistry().registerAverage(
+          statisticsPrefix + "avgIndexListLength")),
+      d_avgStoresListLength(smtStatisticsRegistry().registerAverage(
+          statisticsPrefix + "avgStoresListLength")),
+      d_avgInStoresListLength(smtStatisticsRegistry().registerAverage(
+          statisticsPrefix + "avgInStoresListLength")),
+      d_listsCount(
+          smtStatisticsRegistry().registerInt(statisticsPrefix + "listsCount")),
+      d_callsMergeInfo(smtStatisticsRegistry().registerInt(statisticsPrefix
+                                                           + "callsMergeInfo")),
+      d_maxList(
+          smtStatisticsRegistry().registerInt(statisticsPrefix + "maxList")),
+      d_tableSize(smtStatisticsRegistry().registerSize<CNodeInfoMap>(
+          statisticsPrefix + "infoTableSize", info_map))
+{
   emptyList = new(true) CTNodeList(ct);
   emptyInfo = new Info(ct, bck);
-  smtStatisticsRegistry()->registerStat(&d_mergeInfoTimer);
-  smtStatisticsRegistry()->registerStat(&d_avgIndexListLength);
-  smtStatisticsRegistry()->registerStat(&d_avgStoresListLength);
-  smtStatisticsRegistry()->registerStat(&d_avgInStoresListLength);
-  smtStatisticsRegistry()->registerStat(&d_listsCount);
-  smtStatisticsRegistry()->registerStat(&d_callsMergeInfo);
-  smtStatisticsRegistry()->registerStat(&d_maxList);
-  smtStatisticsRegistry()->registerStat(&d_tableSize);
 }
 
 ArrayInfo::~ArrayInfo() {
@@ -75,14 +80,6 @@ ArrayInfo::~ArrayInfo() {
   }
   emptyList->deleteSelf();
   delete emptyInfo;
-  smtStatisticsRegistry()->unregisterStat(&d_mergeInfoTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_avgIndexListLength);
-  smtStatisticsRegistry()->unregisterStat(&d_avgStoresListLength);
-  smtStatisticsRegistry()->unregisterStat(&d_avgInStoresListLength);
-  smtStatisticsRegistry()->unregisterStat(&d_listsCount);
-  smtStatisticsRegistry()->unregisterStat(&d_callsMergeInfo);
-  smtStatisticsRegistry()->unregisterStat(&d_maxList);
-  smtStatisticsRegistry()->unregisterStat(&d_tableSize);
 }
 
 bool inList(const CTNodeList* l, const TNode el) {