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, 60 insertions, 122 deletions

diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp
index d2df271d3..7fdf44298 100644
--- a/test/unit/util/stats_black.cpp
+++ b/test/unit/util/stats_black.cpp
@@ -18,15 +18,27 @@
 #include <ctime>
 #include <sstream>
 #include <string>
+#include <thread>
 
 #include "expr/proof_rule.h"
 #include "lib/clock_gettime.h"
 #include "test.h"
 #include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
+
+std::ostream& operator<<(std::ostream& os, const StatisticBaseValue* sbv)
+{
+  return os << *sbv;
+}
+bool operator==(const StatisticBaseValue* sbv, const std::string& s)
+{
+  std::stringstream ss;
+  ss << sbv;
+  return ss.str() == s;
+}
+
 namespace test {
 
 class TestUtilBlackStats : public TestInternal
@@ -36,127 +48,53 @@ class TestUtilBlackStats : public TestInternal
 TEST_F(TestUtilBlackStats, stats)
 {
 #ifdef CVC5_STATISTICS_ON
+  StatisticsRegistry reg(false);
   std::string empty, bar = "bar", baz = "baz";
-  ReferenceStat<std::string> refStr("stat #1", empty);
-  ReferenceStat<std::string> refStr2("refStr2", bar);
-  BackedStat<std::string> backedStr("backed", baz);
-
-  BackedStat<double> backedDouble("backedDouble", 16.5);
-  BackedStat<double> backedNegDouble("backedNegDouble", -16.5);
-  BackedStat<double> backedDoubleNoDec("backedDoubleNoDec", 2.0);
-  BackedStat<bool> backedBool("backedBool", true);
-  BackedStat<void*> backedAddr("backedDouble", (void*)0xDEADBEEF);
-  IntegralHistogramStat<std::int64_t> histIntStat("hist-int");
-  histIntStat << 15 << 16 << 15 << 14 << 16;
-  IntegralHistogramStat<cvc5::PfRule> histPfRuleStat("hist-pfrule");
-  histPfRuleStat << PfRule::ASSUME << PfRule::SCOPE << PfRule::ASSUME;
-
-  // A statistic with no safe_print support
-  BackedStat<std::string*> backedUnsupported("backedUnsupported", &bar);
-
-  IntStat sInt("my int", 10);
-  TimerStat sTimer("a timer ! for measuring time");
-
-  ASSERT_EQ(refStr.getName(), "stat #1");
-  ASSERT_EQ(refStr2.getName(), "refStr2");
-  ASSERT_EQ(backedStr.getName(), "backed");
-  ASSERT_EQ(sInt.getName(), "my int");
-  ASSERT_EQ(sTimer.getName(), "a timer ! for measuring time");
-  ASSERT_EQ(histIntStat.getName(), "hist-int");
-  ASSERT_EQ(histPfRuleStat.getName(), "hist-pfrule");
-
-  ASSERT_EQ(refStr.get(), empty);
-  ASSERT_EQ(refStr2.get(), bar);
-  empty = "a different string";
-  bar += " and with an addition";
-  ASSERT_EQ(refStr.get(), empty);
-  ASSERT_EQ(refStr2.get(), bar);
-
-  ASSERT_EQ(backedStr.get(), "baz");
-  baz = "something else";
-  ASSERT_EQ(backedStr.get(), "baz");
-
-  ASSERT_EQ(sInt.get(), 10);
-  sInt.set(100);
-  ASSERT_EQ(sInt.get(), 100);
-
-  ASSERT_TRUE(sTimer.get() == std::chrono::nanoseconds());
-
-  std::stringstream sstr;
-
-  refStr.flushInformation(sstr);
-  ASSERT_EQ(sstr.str(), empty);
-  sstr.str("");
-  refStr2.flushInformation(sstr);
-  ASSERT_EQ(sstr.str(), bar);
-  sstr.str("");
-  backedStr.flushInformation(sstr);
-  ASSERT_EQ(sstr.str(), "baz");
-  sstr.str("");
-  sInt.flushInformation(sstr);
-  ASSERT_EQ(sstr.str(), "100");
-  sstr.str("");
-  sTimer.flushInformation(sstr);
-  ASSERT_EQ(sstr.str(), "0.000000000");
-
-  // Test safeFlushInformation (and safe_print functions)
-  char tmp_filename[] = "testXXXXXX";
-  int fd = mkstemp(tmp_filename);
-  ASSERT_NE(fd, -1);
-  refStr.safeFlushInformation(fd);
-  safe_print(fd, "\n");
-  refStr2.safeFlushInformation(fd);
-  safe_print(fd, "\n");
-  backedStr.safeFlushInformation(fd);
-  safe_print(fd, "\n");
-  sInt.safeFlushInformation(fd);
-  safe_print(fd, "\n");
-  sTimer.safeFlushInformation(fd);
-  safe_print(fd, "\n");
-  backedDouble.safeFlushInformation(fd);
-  safe_print(fd, "\n");
-  backedNegDouble.safeFlushInformation(fd);
-  safe_print(fd, "\n");
-  backedDoubleNoDec.safeFlushInformation(fd);
-  safe_print(fd, "\n");
-  backedAddr.safeFlushInformation(fd);
-  safe_print(fd, "\n");
-  backedBool.safeFlushInformation(fd);
-  safe_print(fd, "\n");
-  histIntStat.safeFlushInformation(fd);
-  safe_print(fd, "\n");
-  histPfRuleStat.safeFlushInformation(fd);
-  safe_print(fd, "\n");
-  backedUnsupported.safeFlushInformation(fd);
-  off_t file_size = lseek(fd, 0, SEEK_CUR);
-  close(fd);
-
-  char* buf = new char[file_size];
-  fd = open(tmp_filename, O_RDONLY);
-  ASSERT_NE(fd, -1);
-  ssize_t n_read = pread(fd, buf, file_size, 0);
-  ASSERT_EQ(n_read, file_size);
-  close(fd);
-
-  const char* expected =
-      "a different string\n"
-      "bar and with an addition\n"
-      "baz\n"
-      "100\n"
-      "0.000000000\n"
-      "16.5\n"
-      "-16.5\n"
-      "2.0\n"
-      "0xdeadbeef\n"
-      "true\n"
-      "[(14 : 1), (15 : 2), (16 : 2)]\n"
-      "[(ASSUME : 2), (SCOPE : 1)]\n"
-      "<unsupported>";
-  ASSERT_EQ(strncmp(expected, buf, file_size), 0);
-  delete[] buf;
-
-  int ret = remove(tmp_filename);
-  ASSERT_EQ(ret, 0);
+
+  AverageStat avg = reg.registerAverage("avg");
+  avg << 1.0 << 2.0;
+
+  HistogramStat<int64_t> histInt = reg.registerHistogram<int64_t>("hist-int");
+  histInt << 15 << 16 << 15 << 14 << 16;
+
+  HistogramStat<PfRule> histPfRule =
+      reg.registerHistogram<PfRule>("hist-pfrule");
+  histPfRule << PfRule::ASSUME << PfRule::SCOPE << PfRule::ASSUME;
+
+  IntStat intstat = reg.registerInt("int");
+  intstat = 5;
+  intstat++;
+
+  ReferenceStat<std::string> refStr =
+      reg.registerReference<std::string>("strref1", empty);
+  ReferenceStat<std::string> refStr2 =
+      reg.registerReference<std::string>("strref2", bar);
+
+  TimerStat timer = reg.registerTimer("timer");
+  {
+    CodeTimer ct(timer);
+    std::this_thread::sleep_for(std::chrono::milliseconds(50));
+  }
+
+  ValueStat<std::string> valStr = reg.registerValue("backed", baz);
+  valStr.set("barz");
+  ValueStat<double> valD1 = reg.registerValue("backedDouble", 16.5);
+  valD1.set(3.5);
+  ValueStat<double> valD2 = reg.registerValue("backedNegDouble", -16.5);
+  valD2.set(-3.5);
+  ValueStat<double> valD3 = reg.registerValue("backedDoubleNoDec", 2.0);
+  valD3.set(17);
+
+  ASSERT_EQ(reg.get("avg"), std::string("1.5"));
+  ASSERT_EQ(reg.get("hist-int"), std::string("{ 14: 1, 15: 2, 16: 2 }"));
+  ASSERT_EQ(reg.get("hist-pfrule"), std::string("{ ASSUME: 2, SCOPE: 1 }"));
+  ASSERT_EQ(reg.get("int"), std::string("6"));
+  ASSERT_EQ(reg.get("strref1"), std::string(""));
+  ASSERT_EQ(reg.get("strref2"), std::string("bar"));
+  ASSERT_EQ(reg.get("backed"), std::string("barz"));
+  ASSERT_EQ(reg.get("backedDouble"), std::string("3.5"));
+  ASSERT_EQ(reg.get("backedNegDouble"), std::string("-3.5"));
+  ASSERT_EQ(reg.get("backedDoubleNoDec"), std::string("17"));
 #endif
 }
 }  // namespace test