diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-14 21:37:12 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-14 19:37:12 +0000 |
commit | 9f14a0d6feca8d8ba727f88ef7dda5268183bb56 (patch) | |
tree | 54d1500f368312ade8abb1fb9962976ae61bedfc /test/unit/util/stats_black.cpp | |
parent | e5c26181dab76704ad9a47126585fe2ec9d6cac2 (diff) |
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.
Diffstat (limited to 'test/unit/util/stats_black.cpp')
-rw-r--r-- | test/unit/util/stats_black.cpp | 182 |
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 |