From 9f14a0d6feca8d8ba727f88ef7dda5268183bb56 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 14 Apr 2021 21:37:12 +0200 Subject: 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. --- src/smt/env.cpp | 1 + src/smt/env.h | 1 - src/smt/proof_post_processor.cpp | 25 +++++--------- src/smt/proof_post_processor.h | 7 ++-- src/smt/smt_engine.cpp | 37 ++++++++++++-------- src/smt/smt_engine.h | 21 +++++++---- src/smt/smt_engine_scope.cpp | 5 +-- src/smt/smt_engine_scope.h | 2 +- src/smt/smt_engine_stats.cpp | 69 ++++++++++++------------------------- src/smt/smt_engine_stats.h | 13 ++----- src/smt/smt_statistics_registry.cpp | 5 +-- src/smt/smt_statistics_registry.h | 3 +- 12 files changed, 83 insertions(+), 106 deletions(-) (limited to 'src/smt') diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 38e93f38e..d079682c5 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -25,6 +25,7 @@ #include "smt/smt_engine_stats.h" #include "theory/rewriter.h" #include "util/resource_manager.h" +#include "util/statistics_registry.h" using namespace cvc5::smt; diff --git a/src/smt/env.h b/src/smt/env.h index c2e0a8f54..09e3238ac 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -23,7 +23,6 @@ #include "options/options.h" #include "theory/logic_info.h" -#include "util/statistics.h" #include "util/statistics_registry.h" namespace cvc5 { diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 105376719..16b7f560b 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -1101,25 +1101,18 @@ bool ProofPostprocessCallback::addToTransChildren(Node eq, ProofPostprocessFinalCallback::ProofPostprocessFinalCallback( ProofNodeManager* pnm) - : d_ruleCount("finalProof::ruleCount"), - d_totalRuleCount("finalProof::totalRuleCount", 0), - d_minPedanticLevel("finalProof::minPedanticLevel", 10), - d_numFinalProofs("finalProofs::numFinalProofs", 0), + : d_ruleCount(smtStatisticsRegistry().registerHistogram( + "finalProof::ruleCount")), + d_totalRuleCount( + smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")), + d_minPedanticLevel( + smtStatisticsRegistry().registerInt("finalProof::minPedanticLevel")), + d_numFinalProofs( + smtStatisticsRegistry().registerInt("finalProofs::numFinalProofs")), d_pnm(pnm), d_pedanticFailure(false) { - smtStatisticsRegistry()->registerStat(&d_ruleCount); - smtStatisticsRegistry()->registerStat(&d_totalRuleCount); - smtStatisticsRegistry()->registerStat(&d_minPedanticLevel); - smtStatisticsRegistry()->registerStat(&d_numFinalProofs); -} - -ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback() -{ - smtStatisticsRegistry()->unregisterStat(&d_ruleCount); - smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount); - smtStatisticsRegistry()->unregisterStat(&d_minPedanticLevel); - smtStatisticsRegistry()->unregisterStat(&d_numFinalProofs); + d_minPedanticLevel += 10; } void ProofPostprocessFinalCallback::initializeUpdate() diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index d66641a69..72fa3581d 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -19,12 +19,12 @@ #define CVC5__SMT__PROOF_POST_PROCESSOR_H #include +#include #include #include "expr/proof_node_updater.h" #include "smt/witness_form.h" -#include "util/statistics_registry.h" -#include "util/stats_histogram.h" +#include "util/statistics_stats.h" namespace cvc5 { @@ -241,7 +241,6 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback { public: ProofPostprocessFinalCallback(ProofNodeManager* pnm); - ~ProofPostprocessFinalCallback(); /** * Initialize, called once for each new ProofNode to process. This initializes * static information to be used by successive calls to update. @@ -256,7 +255,7 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback private: /** Counts number of postprocessed proof nodes for each kind of proof rule */ - IntegralHistogramStat d_ruleCount; + HistogramStat d_ruleCount; /** Total number of postprocessed rule applications */ IntStat d_totalRuleCount; /** The minimum pedantic level of any rule encountered */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3d38ba37b..d3347b019 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -66,6 +66,7 @@ #include "theory/theory_engine.h" #include "util/random.h" #include "util/resource_manager.h" +#include "util/statistics_registry.h" // required for hacks related to old proofs for unsat cores #include "base/configuration.h" @@ -412,7 +413,8 @@ LogicInfo SmtEngine::getUserLogicInfo() const void SmtEngine::notifyStartParsing(const std::string& filename) { d_state->setFilename(filename); - d_stats->d_driverFilename.set(filename); + d_env->getStatisticsRegistry().registerValue("driver::filename", + filename); // Copy the original options. This is called prior to beginning parsing. // Hence reset should revert to these options, which note is after reading // the command line. @@ -424,11 +426,12 @@ const std::string& SmtEngine::getFilename() const } void SmtEngine::setResultStatistic(const std::string& result) { - d_stats->d_driverResult.set(result); + d_env->getStatisticsRegistry().registerValue("driver::sat/unsat", + result); } - void SmtEngine::setTotalTimeStatistic(double seconds) { - d_stats->d_driverTotalTime.set(seconds); + d_env->getStatisticsRegistry().registerValue("driver::totalTime", + seconds); } void SmtEngine::setLogicInternal() @@ -516,11 +519,13 @@ cvc5::SExpr SmtEngine::getInfo(const std::string& key) const if (key == "all-statistics") { vector stats; - for (const auto& s: d_env->getStatisticsRegistry()) + for (const auto& s : d_env->getStatisticsRegistry()) { + std::stringstream ss; + ss << *s.second; vector v; v.push_back(s.first); - v.push_back(s.second); + v.push_back(ss.str()); stats.push_back(v); } return SExpr(stats); @@ -1866,24 +1871,28 @@ NodeManager* SmtEngine::getNodeManager() const return d_env->getNodeManager(); } -Statistics SmtEngine::getStatistics() const -{ - return Statistics(d_env->getStatisticsRegistry()); -} - SExpr SmtEngine::getStatistic(std::string name) const { - return d_env->getStatisticsRegistry().getStatistic(name); + const auto* val = d_env->getStatisticsRegistry().get(name); + std::stringstream ss; + ss << *val; + return SExpr({SExpr(name), SExpr(ss.str())}); } void SmtEngine::printStatistics(std::ostream& out) const { - d_env->getStatisticsRegistry().flushInformation(out); + d_env->getStatisticsRegistry().print(out); } void SmtEngine::printStatisticsSafe(int fd) const { - d_env->getStatisticsRegistry().safeFlushInformation(fd); + d_env->getStatisticsRegistry().printSafe(fd); +} + +void SmtEngine::printStatisticsDiff(std::ostream& out) const +{ + d_env->getStatisticsRegistry().printDiff(out); + d_env->getStatisticsRegistry().storeSnapshot(); } void SmtEngine::setUserAttribute(const std::string& attr, diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index ec2699c31..5947367f2 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -31,7 +31,6 @@ #include "theory/logic_info.h" #include "util/result.h" #include "util/sexpr.h" -#include "util/statistics.h" namespace cvc5 { @@ -827,21 +826,29 @@ class CVC4_EXPORT SmtEngine /** Permit access to the underlying NodeManager. */ NodeManager* getNodeManager() const; - /** Export statistics from this SmtEngine. */ - Statistics getStatistics() const; - /** Get the value of one named statistic from this SmtEngine. */ SExpr getStatistic(std::string name) const; - /** Flush statistics from this SmtEngine and the NodeManager it uses. */ + /** + * Print statistics from the statistics registry in the env object owned by + * this SmtEngine. + */ void printStatistics(std::ostream& out) const; /** - * Flush statistics from this SmtEngine and the NodeManager it uses. Safe to - * use in a signal handler. + * Print statistics from the statistics registry in the env object owned by + * this SmtEngine. Safe to use in a signal handler. */ void printStatisticsSafe(int fd) const; + /** + * Print the changes to the statistics from the statistics registry in the + * env object owned by this SmtEngine since this method was called the last + * time. Internally prints the diff and then stores a snapshot for the next + * call. + */ + void printStatisticsDiff(std::ostream&) const; + /** * Set user attribute. * This function is called when an attribute is set by a user. diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 1164bc1b5..962529924 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -61,9 +61,10 @@ SmtScope::~SmtScope() { << std::endl; } -StatisticsRegistry* SmtScope::currentStatisticsRegistry() { +StatisticsRegistry& SmtScope::currentStatisticsRegistry() +{ Assert(smtEngineInScope()); - return &(s_smtEngine_current->getStatisticsRegistry()); + return s_smtEngine_current->getStatisticsRegistry(); } } // namespace smt diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index a1d660adf..76bc5c641 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -51,7 +51,7 @@ class SmtScope : public NodeManagerScope * This returns the StatisticsRegistry attached to the currently in scope * SmtEngine. */ - static StatisticsRegistry* currentStatisticsRegistry(); + static StatisticsRegistry& currentStatisticsRegistry(); private: /** The old SmtEngine, to be restored on destruction. */ diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp index 5147c046a..417d345cb 100644 --- a/src/smt/smt_engine_stats.cpp +++ b/src/smt/smt_engine_stats.cpp @@ -20,54 +20,29 @@ namespace cvc5 { namespace smt { -SmtEngineStatistics::SmtEngineStatistics() - : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), - d_numConstantProps("smt::SmtEngine::numConstantProps", 0), - d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), - d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), - d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0), - d_checkModelTime("smt::SmtEngine::checkModelTime"), - d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"), - d_solveTime("smt::SmtEngine::solveTime"), - d_pushPopTime("smt::SmtEngine::pushPopTime"), - d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"), - d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0), - d_driverFilename("driver::filename", ""), - d_driverResult("driver::sat/unsat", ""), - d_driverTotalTime("driver::totalTime", 0.0) +SmtEngineStatistics::SmtEngineStatistics(const std::string& name) + : d_definitionExpansionTime(smtStatisticsRegistry().registerTimer( + name + "definitionExpansionTime")), + d_numConstantProps( + smtStatisticsRegistry().registerInt(name + "numConstantProps")), + d_cnfConversionTime( + smtStatisticsRegistry().registerTimer(name + "cnfConversionTime")), + d_numAssertionsPre(smtStatisticsRegistry().registerInt( + name + "numAssertionsPreITERemoval")), + d_numAssertionsPost(smtStatisticsRegistry().registerInt( + name + "numAssertionsPostITERemoval")), + d_checkModelTime( + smtStatisticsRegistry().registerTimer(name + "checkModelTime")), + d_checkUnsatCoreTime( + smtStatisticsRegistry().registerTimer(name + "checkUnsatCoreTime")), + d_solveTime(smtStatisticsRegistry().registerTimer(name + "solveTime")), + d_pushPopTime( + smtStatisticsRegistry().registerTimer(name + "pushPopTime")), + d_processAssertionsTime(smtStatisticsRegistry().registerTimer( + name + "processAssertionsTime")), + d_simplifiedToFalse( + smtStatisticsRegistry().registerInt(name + "simplifiedToFalse")) { - smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime); - smtStatisticsRegistry()->registerStat(&d_numConstantProps); - smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); - smtStatisticsRegistry()->registerStat(&d_numAssertionsPre); - smtStatisticsRegistry()->registerStat(&d_numAssertionsPost); - smtStatisticsRegistry()->registerStat(&d_checkModelTime); - smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime); - smtStatisticsRegistry()->registerStat(&d_solveTime); - smtStatisticsRegistry()->registerStat(&d_pushPopTime); - smtStatisticsRegistry()->registerStat(&d_processAssertionsTime); - smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse); - smtStatisticsRegistry()->registerStat(&d_driverFilename); - smtStatisticsRegistry()->registerStat(&d_driverResult); - smtStatisticsRegistry()->registerStat(&d_driverTotalTime); -} - -SmtEngineStatistics::~SmtEngineStatistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime); - smtStatisticsRegistry()->unregisterStat(&d_numConstantProps); - smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); - smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre); - smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost); - smtStatisticsRegistry()->unregisterStat(&d_checkModelTime); - smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime); - smtStatisticsRegistry()->unregisterStat(&d_solveTime); - smtStatisticsRegistry()->unregisterStat(&d_pushPopTime); - smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime); - smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse); - smtStatisticsRegistry()->unregisterStat(&d_driverFilename); - smtStatisticsRegistry()->unregisterStat(&d_driverResult); - smtStatisticsRegistry()->unregisterStat(&d_driverTotalTime); } } // namespace smt diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h index d2bece92f..441721a54 100644 --- a/src/smt/smt_engine_stats.h +++ b/src/smt/smt_engine_stats.h @@ -18,16 +18,14 @@ #ifndef CVC5__SMT__SMT_ENGINE_STATS_H #define CVC5__SMT__SMT_ENGINE_STATS_H -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace smt { struct SmtEngineStatistics { - SmtEngineStatistics(); - ~SmtEngineStatistics(); + SmtEngineStatistics(const std::string& name = "smt::SmtEngine::"); /** time spent in definition-expansion */ TimerStat d_definitionExpansionTime; /** number of constant propagations found during nonclausal simp */ @@ -51,13 +49,6 @@ struct SmtEngineStatistics /** Has something simplified to false? */ IntStat d_simplifiedToFalse; - - /** Name of the input file */ - BackedStat d_driverFilename; - /** Result of the last check */ - BackedStat d_driverResult; - /** Total time of the current run */ - BackedStat d_driverTotalTime; }; /* struct SmtEngineStatistics */ } // namespace smt diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp index db437526a..bb1cfc9fa 100644 --- a/src/smt/smt_statistics_registry.cpp +++ b/src/smt/smt_statistics_registry.cpp @@ -16,11 +16,12 @@ #include "smt/smt_statistics_registry.h" #include "smt/smt_engine_scope.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { -StatisticsRegistry* smtStatisticsRegistry() { +StatisticsRegistry& smtStatisticsRegistry() +{ return smt::SmtScope::currentStatisticsRegistry(); } diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h index d8adde3c3..31f55375c 100644 --- a/src/smt/smt_statistics_registry.h +++ b/src/smt/smt_statistics_registry.h @@ -18,6 +18,7 @@ #pragma once #include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { @@ -25,6 +26,6 @@ namespace cvc5 { * This returns the StatisticsRegistry attached to the currently in scope * SmtEngine. This is a synonym for smt::SmtScope::currentStatisticsRegistry(). */ -StatisticsRegistry* smtStatisticsRegistry(); +StatisticsRegistry& smtStatisticsRegistry(); } // namespace cvc5 -- cgit v1.2.3