diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/CMakeLists.txt | 4 | ||||
-rw-r--r-- | src/util/statistics_public.cpp | 28 | ||||
-rw-r--r-- | src/util/statistics_public.h | 33 | ||||
-rw-r--r-- | src/util/statistics_reg.cpp | 143 | ||||
-rw-r--r-- | src/util/statistics_reg.h | 233 |
5 files changed, 441 insertions, 0 deletions
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 2595ab4c0..4bc6da1ae 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -62,6 +62,10 @@ libcvc4_add_sources( smt2_quote_string.h statistics.cpp statistics.h + statistics_public.cpp + statistics_public.h + statistics_reg.cpp + statistics_reg.h statistics_registry.cpp statistics_registry.h statistics_value.cpp diff --git a/src/util/statistics_public.cpp b/src/util/statistics_public.cpp new file mode 100644 index 000000000..dd488c192 --- /dev/null +++ b/src/util/statistics_public.cpp @@ -0,0 +1,28 @@ +/********************* */ +/*! \file statistics_public.cpp + ** \verbatim + ** Top contributors (to current version): + ** Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Registration of public statistics + ** + ** Registration and documentation for all public statistics. + **/ + +#include "util/statistics_public.h" + +#include "util/statistics_registry.h" + +namespace cvc5 { + +void registerPublicStatistics(StatisticsRegistry& reg) +{ + +} + +} // namespace cvc5 diff --git a/src/util/statistics_public.h b/src/util/statistics_public.h new file mode 100644 index 000000000..c2d054f00 --- /dev/null +++ b/src/util/statistics_public.h @@ -0,0 +1,33 @@ +/********************* */ +/*! \file statistics_public.h + ** \verbatim + ** Top contributors (to current version): + ** Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Registration of public statistics + ** + ** Registration and documentation for all public statistics. + **/ + +#include "cvc4_private_library.h" + +#ifndef CVC4__UTIL__STATISTICS_PUBLIC_H +#define CVC4__UTIL__STATISTICS_PUBLIC_H + +namespace cvc5 { + +class StatisticsRegistry; + +/** + * Preregisters all public (non-expert) statistics. + */ +void registerPublicStatistics(StatisticsRegistry& reg); + +} // namespace cvc5 + +#endif diff --git a/src/util/statistics_reg.cpp b/src/util/statistics_reg.cpp new file mode 100644 index 000000000..efb564c74 --- /dev/null +++ b/src/util/statistics_reg.cpp @@ -0,0 +1,143 @@ +/********************* */ +/*! \file statistics_reg.cpp + ** \verbatim + ** Top contributors (to current version): + ** Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Central statistics registry. + ** + ** The StatisticsRegistry that issues statistic proxy objects. + **/ + +#include "util/statistics_reg.h" + +#include "options/base_options.h" +#include "util/statistics_public.h" + +namespace cvc5 { + +StatisticsRegistry::StatisticsRegistry(bool registerPublic) +{ + if (registerPublic) + { + registerPublicStatistics(*this); + } +} + +AverageStat StatisticsRegistry::registerAverage(const std::string& name, + bool expert) +{ + return registerStat<AverageStat>(name, expert); +} +IntStat StatisticsRegistry::registerInt(const std::string& name, bool expert) +{ + return registerStat<IntStat>(name, expert); +} +TimerStat StatisticsRegistry::registerTimer(const std::string& name, + bool expert) +{ + return registerStat<TimerStat>(name, expert); +} + +void StatisticsRegistry::storeSnapshot() +{ + if constexpr (Configuration::isStatisticsBuild()) + { + d_lastSnapshot = std::make_unique<Snapshot>(); + for (const auto& s : d_stats) + { + if (!options::statisticsExpert() && s.second->d_expert) continue; + if (!options::statisticsUnset() && !s.second->hasValue()) continue; + d_lastSnapshot->emplace( + s.first, + s.second->hasValue() ? s.second->getViewer() : StatExportData{}); + } + } +} + +StatisticBaseValue* StatisticsRegistry::get(const std::string& name) const +{ + if constexpr (Configuration::isStatisticsBuild()) + { + auto it = d_stats.find(name); + if (it == d_stats.end()) return nullptr; + return it->second.get(); + } + return nullptr; +} + +void StatisticsRegistry::print(std::ostream& os) const +{ + if constexpr (Configuration::isStatisticsBuild()) + { + for (const auto& s : d_stats) + { + if (!options::statisticsExpert() && s.second->d_expert) continue; + if (!options::statisticsUnset() && !s.second->hasValue()) continue; + os << s.first << " = " << *s.second << std::endl; + } + } +} + +void StatisticsRegistry::printSafe(int fd) const +{ + if constexpr (Configuration::isStatisticsBuild()) + { + for (const auto& s : d_stats) + { + if (!options::statisticsExpert() && s.second->d_expert) continue; + if (!options::statisticsUnset() && !s.second->hasValue()) continue; + + safe_print(fd, s.first); + safe_print(fd, " = "); + if (s.second->hasValue()) + s.second->printSafe(fd); + else + safe_print(fd, "<unset>"); + safe_print(fd, '\n'); + } + } +} +void StatisticsRegistry::printDiff(std::ostream& os) const +{ + if constexpr (Configuration::isStatisticsBuild()) + { + if (!d_lastSnapshot) + { + // we have no snapshot, print as usual + print(os); + return; + } + for (const auto& s : d_stats) + { + if (!options::statisticsExpert() && s.second->d_expert) continue; + if (!options::statisticsUnset() && !s.second->hasValue()) continue; + auto oldit = d_lastSnapshot->find(s.first); + if (oldit == d_lastSnapshot->end()) + { + // not present in the snapshot + os << s.first << " = " << *s.second << " (was <unset>)" << std::endl; + } + else if (oldit->second != s.second->getViewer()) + { + // present in the snapshow, print old value + os << s.first << " = " << *s.second << " (was "; + detail::print(os, oldit->second); + os << ")" << std::endl; + } + } + } +} + +std::ostream& operator<<(std::ostream& os, const StatisticsRegistry& sr) +{ + sr.print(os); + return os; +} + +} // namespace cvc5 diff --git a/src/util/statistics_reg.h b/src/util/statistics_reg.h new file mode 100644 index 000000000..e020a05b4 --- /dev/null +++ b/src/util/statistics_reg.h @@ -0,0 +1,233 @@ +/********************* */ +/*! \file statistics_reg.h + ** \verbatim + ** Top contributors (to current version): + ** Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Central statistics registry. + ** + ** The StatisticsRegistry that issues statistic proxy objects. + **/ + +#include "cvc4_private_library.h" + +#ifndef CVC4__UTIL__STATISTICS_REG_H +#define CVC4__UTIL__STATISTICS_REG_H + +#include <iostream> +#include <map> +#include <memory> +#include <typeinfo> + +#include "base/check.h" +#include "util/statistics_stats.h" +#include "util/statistics_value.h" + +namespace cvc5 { + +struct StatisticBaseValue; + +/** + * The central registry for statistics. + * Internally stores statistic data objects and issues corresponding proxy + * objects to modules that want to expose statistics. + * Provides registration methods (e.g. `registerAverage` or + * `registerHistogram<T>`) that return the proxy object. + * The different statistics are explained in more detail in statistics_stats.h + * + * Every statistic is identified by a name. If a statistic with the given + * name is already registered, the registry issues another proxy object + * for that name using the same data it already holds for this name. + * While this makes perfect sense for most statistic types, it may lead to + * unexpected (though not undefined) behaviour for others. For a reference + * statistic, for example, the internal data will simply point to the object + * registered last. + * Note that the type of the re-registered statistic must always match + * the type of the previously registered statistic with the same name. + * + * We generally distinguish between public (non-expert) and private (expert) + * statistics. By default, `--stats` only shows public statistics. Private + * ones are printed as well if `--all-statistics` is set. + * All registration methods have a trailing argument `expert`, defaulting to + * true. + * + * If statistics are disabled entirely (i.e. the cmake option + * `ENABLE_STATISTICS` is not set), the registry still issues proxy objects + * that can be used normally. + * However, no data is stored in the registry and the modification functions + * of the proxy objects do nothing. + */ +class StatisticsRegistry +{ + public: + friend std::ostream& operator<<(std::ostream& os, + const StatisticsRegistry& sr); + + using Snapshot = std::map<std::string, StatExportData>; + + /** + * If `registerPublic` is true, all statistics that are public are + * pre-registered as such. This argument mostly exists so that unit tests + * can disable this pre-registration. + */ + StatisticsRegistry(bool registerPublic = true); + + /** Register a new running average statistic for `name` */ + + AverageStat registerAverage(const std::string& name, bool expert = true); + /** Register a new histogram statistic for `name` */ + template <typename T> + HistogramStat<T> registerHistogram(const std::string& name, + bool expert = true) + { + return registerStat<HistogramStat<T>>(name, expert); + } + + /** Register a new integer statistic for `name` */ + IntStat registerInt(const std::string& name, bool expert = true); + + /** Register a new reference statistic for `name` */ + template <typename T> + ReferenceStat<T> registerReference(const std::string& name, + bool expert = true) + { + return registerStat<ReferenceStat<T>>(name, expert); + } + /** + * Register a new reference statistic for `name` and initialize it to + * refer to `t`. + */ + template <typename T> + ReferenceStat<T> registerReference(const std::string& name, + const T& t, + bool expert = true) + { + ReferenceStat<T> res = registerStat<ReferenceStat<T>>(name, expert); + res.set(t); + return res; + } + + /** + * Register a new container size statistic for `name` and initialize it + * to refer to `t`. + */ + template <typename T> + SizeStat<T> registerSize(const std::string& name, + const T& t, + bool expert = true) + { + SizeStat<T> res = registerStat<SizeStat<T>>(name, expert); + res.set(t); + return res; + } + + /** Register a new timer statistic for `name` */ + TimerStat registerTimer(const std::string& name, bool expert = true); + + /** Register a new value statistic for `name`. */ + template <typename T> + ValueStat<T> registerValue(const std::string& name, bool expert = true) + { + return registerStat<ValueStat<T>>(name, expert); + } + + /** Register a new value statistic for `name` and set it to `init`. */ + template <typename T> + ValueStat<T> registerValue(const std::string& name, + const T& init, + bool expert = true) + { + ValueStat<T> res = registerStat<ValueStat<T>>(name, expert); + res.set(init); + return res; + } + + /** begin iteration */ + auto begin() const { return d_stats.begin(); } + /** end iteration */ + auto end() const { return d_stats.end(); } + + /** + * Store the current state of the statistics to allow for printing a diff + * using `printDiff`. + */ + void storeSnapshot(); + + /** + * Obtain a single statistic by name. Returns nullptr if no statistic has + * been registered for this name. + */ + StatisticBaseValue* get(const std::string& name) const; + + /** + * Print all statistics to the given output stream. + */ + void print(std::ostream& os) const; + /** + * Print all statistics in a safe manner to the given file descriptor. + */ + void printSafe(int fd) const; + /** + * Print all statistics as a diff to the last snapshot that was stored by + * calling `storeSnapshot`. + */ + void printDiff(std::ostream& os) const; + + private: + /** + * Helper method to register a new statistic. + * If the name was already used, a new proxy object is created. + * We check whether the type matches the type of the originally registered + * statistic using `typeid`. + */ + template <typename Stat> + Stat registerStat(const std::string& name, bool expert) + { + if constexpr (Configuration::isStatisticsBuild()) + { + auto it = d_stats.find(name); + if (it == d_stats.end()) + { + it = d_stats.emplace(name, std::make_unique<typename Stat::stat_type>()) + .first; + it->second->d_expert = expert; + } + auto* ptr = it->second.get(); + Assert(typeid(*ptr) == typeid(typename Stat::stat_type)) + << "Statistic value " << name + << " was registered again with a different type."; + it->second->d_expert = it->second->d_expert && expert; + return Stat(static_cast<typename Stat::stat_type*>(ptr)); + } + return Stat(nullptr); + } + + /** + * Holds (and owns) all statistic values, indexed by the name they were + * registered for. + */ + std::map<std::string, std::unique_ptr<StatisticBaseValue>> d_stats; + + /** + * Holds a snapshot of the statistic values as StatExportData. + * The current state can be saved to this snapshot using `storeSnapshot`, + * which is then used in the next call to `printDiff`, but the data is not + * exposed otherwise. + * As this snapshot is only used by `printDiff`, which honors the relevant + * options `--stats-expert` and `--stats-unset`, the snapshot is populated + * by `storeSnapshot` to contain only those values that would be printed. + */ + std::unique_ptr<Snapshot> d_lastSnapshot; +}; + +/** Calls `sr.print(os)`. */ +std::ostream& operator<<(std::ostream& os, const StatisticsRegistry& sr); + +} // namespace cvc5 + +#endif |