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/api/cpp/cvc5.cpp | 269 +++++++++++++++++++++++++++++++++++++++++++++------ src/api/cpp/cvc5.h | 139 +++++++++++++++++++++++++- 2 files changed, 375 insertions(+), 33 deletions(-) (limited to 'src/api') diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 1c62bd4f0..2a8e0f4c7 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -61,25 +61,22 @@ #include "util/random.h" #include "util/result.h" #include "util/statistics_registry.h" -#include "util/stats_histogram.h" +#include "util/statistics_stats.h" +#include "util/statistics_value.h" #include "util/utility.h" namespace cvc5 { namespace api { /* -------------------------------------------------------------------------- */ -/* Statistics */ +/* APIStatistics */ /* -------------------------------------------------------------------------- */ -struct Statistics +struct APIStatistics { - Statistics() - : d_consts("api::CONSTANT"), d_vars("api::VARIABLE"), d_terms("api::TERM") - { - } - IntegralHistogramStat d_consts; - IntegralHistogramStat d_vars; - IntegralHistogramStat d_terms; + HistogramStat d_consts; + HistogramStat d_vars; + HistogramStat d_terms; }; /* -------------------------------------------------------------------------- */ @@ -4055,6 +4052,200 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const return size_t(rm); } +/* -------------------------------------------------------------------------- */ +/* Statistics */ +/* -------------------------------------------------------------------------- */ + +struct Stat::StatData +{ + cvc5::StatExportData data; + template + StatData(T&& t) : data(std::forward(t)) + { + } + StatData() : data() {} +}; + +Stat::~Stat() {} +Stat::Stat(const Stat& s) + : d_expert(s.d_expert), d_data(std::make_unique(s.d_data->data)) +{ +} +Stat& Stat::operator=(const Stat& s) +{ + d_expert = s.d_expert; + d_data = std::make_unique(s.d_data->data); + return *this; +} + +bool Stat::isExpert() const { return d_expert; } +bool Stat::isDefault() const { return d_default; } + +bool Stat::isInt() const +{ + return std::holds_alternative(d_data->data); +} +int64_t Stat::getInt() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK(isInt()) << "Expected Stat of type int64_t."; + return std::get(d_data->data); + CVC5_API_TRY_CATCH_END; +} +bool Stat::isDouble() const +{ + return std::holds_alternative(d_data->data); +} +double Stat::getDouble() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK(isDouble()) << "Expected Stat of type double."; + return std::get(d_data->data); + CVC5_API_TRY_CATCH_END; +} +bool Stat::isString() const +{ + return std::holds_alternative(d_data->data); +} +const std::string& Stat::getString() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK(isString()) << "Expected Stat of type std::string."; + return std::get(d_data->data); + CVC5_API_TRY_CATCH_END; +} +bool Stat::isHistogram() const +{ + return std::holds_alternative(d_data->data); +} +const Stat::HistogramData& Stat::getHistogram() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK(isHistogram()) << "Expected Stat of type histogram."; + return std::get(d_data->data); + CVC5_API_TRY_CATCH_END; +} + +Stat::Stat(bool expert, bool def, StatData&& sd) + : d_expert(expert), + d_default(def), + d_data(std::make_unique(std::move(sd))) +{ +} + +std::ostream& operator<<(std::ostream& os, const Stat& sv) +{ + return cvc5::detail::print(os, sv.d_data->data); +} + +Statistics::BaseType::const_reference Statistics::iterator::operator*() const +{ + return d_it.operator*(); +} +Statistics::BaseType::const_pointer Statistics::iterator::operator->() const +{ + return d_it.operator->(); +} +Statistics::iterator& Statistics::iterator::operator++() +{ + do + { + ++d_it; + } while (!isVisible()); + return *this; +} +Statistics::iterator Statistics::iterator::operator++(int) +{ + iterator tmp = *this; + do + { + ++d_it; + } while (!isVisible()); + return tmp; +} +Statistics::iterator& Statistics::iterator::operator--() +{ + do + { + --d_it; + } while (!isVisible()); + return *this; +} +Statistics::iterator Statistics::iterator::operator--(int) +{ + iterator tmp = *this; + do + { + --d_it; + } while (!isVisible()); + return tmp; +} +bool Statistics::iterator::operator==(const Statistics::iterator& rhs) const +{ + return d_it == rhs.d_it; +} +bool Statistics::iterator::operator!=(const Statistics::iterator& rhs) const +{ + return d_it != rhs.d_it; +} +Statistics::iterator::iterator(Statistics::BaseType::const_iterator it, + const Statistics::BaseType& base, + bool expert, + bool def) + : d_it(it), d_base(&base), d_showExpert(expert), d_showDefault(def) +{ + while (!isVisible()) + { + ++d_it; + } +} +bool Statistics::iterator::isVisible() const +{ + if (d_it == d_base->end()) return true; + if (!d_showExpert && d_it->second.isExpert()) return false; + if (!d_showDefault && d_it->second.isDefault()) return false; + return true; +} + +const Stat& Statistics::get(const std::string& name) +{ + CVC5_API_TRY_CATCH_BEGIN; + auto it = d_stats.find(name); + CVC5_API_CHECK(it != d_stats.end()) + << "No stat with name \"" << name << "\" exists."; + return it->second; + CVC5_API_TRY_CATCH_END; +} + +Statistics::iterator Statistics::begin(bool expert, bool def) const +{ + return iterator(d_stats.begin(), d_stats, expert, def); +} +Statistics::iterator Statistics::end() const +{ + return iterator(d_stats.end(), d_stats, false, false); +} + +Statistics::Statistics(const StatisticsRegistry& reg) +{ + for (const auto& svp : reg) + { + d_stats.emplace(svp.first, + Stat(svp.second->d_expert, + svp.second->isDefault(), + svp.second->getViewer())); + } +} + +std::ostream& operator<<(std::ostream& out, const Statistics& stats) +{ + for (const auto& stat : stats) + { + out << stat.first << " = " << stat.second << std::endl; + } + return out; +} + /* -------------------------------------------------------------------------- */ /* Solver */ /* -------------------------------------------------------------------------- */ @@ -4070,12 +4261,7 @@ Solver::Solver(Options* opts) d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), d_originalOptions.get())); d_smtEngine->setSolver(this); d_rng.reset(new Random(d_smtEngine->getOptions()[options::seed])); -#if CVC5_STATISTICS_ON - d_stats.reset(new Statistics()); - d_smtEngine->getStatisticsRegistry().registerStat(&d_stats->d_consts); - d_smtEngine->getStatisticsRegistry().registerStat(&d_stats->d_vars); - d_smtEngine->getStatisticsRegistry().registerStat(&d_stats->d_terms); -#endif + resetStatistics(); } Solver::~Solver() {} @@ -4087,27 +4273,29 @@ NodeManager* Solver::getNodeManager(void) const { return d_nodeMgr.get(); } void Solver::increment_term_stats(Kind kind) const { -#ifdef CVC5_STATISTICS_ON - d_stats->d_terms << kind; -#endif + if constexpr (Configuration::isStatisticsBuild()) + { + d_stats->d_terms << kind; + } } void Solver::increment_vars_consts_stats(const Sort& sort, bool is_var) const { -#ifdef CVC5_STATISTICS_ON - const TypeNode tn = sort.getTypeNode(); - TypeConstant tc = tn.getKind() == cvc5::kind::TYPE_CONSTANT - ? tn.getConst() - : LAST_TYPE; - if (is_var) - { - d_stats->d_vars << tc; - } - else + if constexpr (Configuration::isStatisticsBuild()) { - d_stats->d_consts << tc; + const TypeNode tn = sort.getTypeNode(); + TypeConstant tc = tn.getKind() == cvc5::kind::TYPE_CONSTANT + ? tn.getConst() + : LAST_TYPE; + if (is_var) + { + d_stats->d_vars << tc; + } + else + { + d_stats->d_consts << tc; + } } -#endif } /* Split out to avoid nested API calls (problematic with API tracing). */ @@ -4503,6 +4691,20 @@ bool Solver::isValidInteger(const std::string& s) const return true; } +void Solver::resetStatistics() +{ + if constexpr (Configuration::isStatisticsBuild()) + { + d_stats.reset(new APIStatistics{ + d_smtEngine->getStatisticsRegistry().registerHistogram( + "api::CONSTANT"), + d_smtEngine->getStatisticsRegistry().registerHistogram( + "api::VARIABLE"), + d_smtEngine->getStatisticsRegistry().registerHistogram("api::TERM"), + }); + } +} + /* Helpers for mkTerm checks. */ /* .......................................................................... */ @@ -6822,6 +7024,11 @@ SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); } */ Options& Solver::getOptions(void) { return d_smtEngine->getOptions(); } +Statistics Solver::getStatistics() const +{ + return Statistics(d_smtEngine->getStatisticsRegistry()); +} + } // namespace api } // namespace cvc5 diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 4876caf80..1e0e17e52 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -47,11 +47,13 @@ class TypeNode; class Options; class Random; class Result; +class StatisticsRegistry; namespace api { class Solver; -struct Statistics; +class Statistics; +struct APIStatistics; /* -------------------------------------------------------------------------- */ /* Exception */ @@ -2258,6 +2260,130 @@ struct CVC4_EXPORT RoundingModeHashFunction inline size_t operator()(const RoundingMode& rm) const; }; +/* -------------------------------------------------------------------------- */ +/* Statistics */ +/* -------------------------------------------------------------------------- */ + +/** + * Represents a snapshot of a single statistic value. + * A value can be of type int64_t, double, std::string or a histogram + * (`std::map`). + * The value type can be queried (using `isInt`, `isString`, etc.) and + * the stored value can be accessed (using `getInt`, `getString`, etc.). + */ +class CVC4_EXPORT Stat +{ + struct StatData; + + public: + friend class Statistics; + friend std::ostream& operator<<(std::ostream& os, const Stat& sv); + using HistogramData = std::map; + /** Create from the given value. */ + Stat() = delete; + Stat(const Stat& s); + ~Stat(); + Stat& operator=(const Stat& s); + + /** Is this value intended for experts only? */ + bool isExpert() const; + /** Does this value hold the default value? */ + bool isDefault() const; + + /** Is this value an integer? */ + bool isInt() const; + /** Return the integer value */ + int64_t getInt() const; + /** Is this value a double? */ + bool isDouble() const; + /** Return the double value */ + double getDouble() const; + /** Is this value an string? */ + bool isString() const; + /** Return the string value */ + const std::string& getString() const; + /** Is this value an histogram? */ + bool isHistogram() const; + /** Return the histogram value */ + const HistogramData& getHistogram() const; + + private: + Stat(bool expert, bool def, StatData&& sd); + /** Whether this statistic is only meant for experts */ + bool d_expert; + /** Whether this statistic has the default value */ + bool d_default; + std::unique_ptr d_data; +}; + +std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC4_EXPORT; + +/** + * Represents a snapshot of the solver statistics. + * Once obtained, an instance of this class is independent of the `Solver` + * object: it will not change when the solvers internal statistics do, it + * will not be invalidated if the solver is destroyed. + * Statistics are generally categorized as public and expert statistics. + * Furthermore, statistics may hold the default values and thus be not of + * interest. + * Iterating on this class (via `begin()` and `end()`) shows only public + * statistics that have been set. By passing appropriate flags to `begin()`, + * statistics that are expert, unchanged, or both, can be included as well. + * A single statistic value is represented as `Stat`. + */ +class CVC4_EXPORT Statistics +{ + public: + friend Solver; + using BaseType = std::map; + + /** Custom iterator to hide expert statistics from regular iteration */ + class iterator + { + public: + friend Statistics; + BaseType::const_reference operator*() const; + BaseType::const_pointer operator->() const; + iterator& operator++(); + iterator operator++(int); + iterator& operator--(); + iterator operator--(int); + bool operator==(const iterator& rhs) const; + bool operator!=(const iterator& rhs) const; + + private: + iterator(BaseType::const_iterator it, + const BaseType& base, + bool expert, + bool def); + bool isVisible() const; + BaseType::const_iterator d_it; + const BaseType* d_base; + bool d_showExpert = false; + bool d_showDefault = false; + }; + + /** Retrieve the statistic with the given name. */ + const Stat& get(const std::string& name); + /** + * Begin iteration over the statistics values. + * By default, only entries that are public (non-expert) and have been set + * are visible while the others are skipped. + * With `expert` set to true, expert statistics are shown as well. + * With `def` set to true, defaulted statistics are shown as well. + */ + iterator begin(bool expert = false, bool def = false) const; + /** end iteration */ + iterator end() const; + + private: + Statistics() = default; + Statistics(const StatisticsRegistry& reg); + /** Internal data */ + BaseType d_stats; +}; +std::ostream& operator<<(std::ostream& out, const Statistics& stats) CVC4_EXPORT; + /* -------------------------------------------------------------------------- */ /* Solver */ /* -------------------------------------------------------------------------- */ @@ -3680,9 +3806,18 @@ class CVC4_EXPORT Solver // the driver level. !!! Options& getOptions(void); + /** + * Returns a snapshot of the current state of the statistic values of this + * solver. The returned object is completely decoupled from the solver and + * will not change when the solver is used again. + */ + Statistics getStatistics() const; + private: /** @return the node manager of this solver */ NodeManager* getNodeManager(void) const; + /** Reset the API statistics */ + void resetStatistics(); /** Helper to check for API misuse in mkOp functions. */ void checkMkTerm(Kind kind, uint32_t nchildren) const; @@ -3779,7 +3914,7 @@ class CVC4_EXPORT Solver /** The node manager of this solver. */ std::unique_ptr d_nodeMgr; /** The statistics collected on the Api level. */ - std::unique_ptr d_stats; + std::unique_ptr d_stats; /** The SMT engine of this solver. */ std::unique_ptr d_smtEngine; /** The random number generator of this solver. */ -- cgit v1.2.3