diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/configuration.cpp | 4 | ||||
| -rw-r--r-- | src/base/configuration.h | 9 | ||||
| -rw-r--r-- | src/base/configuration_private.h | 6 | ||||
| -rw-r--r-- | src/util/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/util/statistics_stats.cpp | 135 | ||||
| -rw-r--r-- | src/util/statistics_stats.h | 340 | ||||
| -rw-r--r-- | src/util/statistics_value.cpp | 126 | ||||
| -rw-r--r-- | src/util/statistics_value.h | 402 |
8 files changed, 1013 insertions, 11 deletions
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 5dd9c2831..561500a16 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -46,10 +46,6 @@ bool Configuration::isDebugBuild() { return IS_DEBUG_BUILD; } -bool Configuration::isStatisticsBuild() { - return IS_STATISTICS_BUILD; -} - bool Configuration::isTracingBuild() { return IS_TRACING_BUILD; } diff --git a/src/base/configuration.h b/src/base/configuration.h index 4d7a73d4c..e277739dc 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -48,7 +48,14 @@ public: static bool isDebugBuild(); - static bool isStatisticsBuild(); + static constexpr bool isStatisticsBuild() + { +#ifdef CVC4_STATISTICS_ON + return true; +#else + return false; +#endif + } static bool isTracingBuild(); diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 1ec28dc4b..a39393814 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -30,12 +30,6 @@ namespace cvc5 { # define IS_DEBUG_BUILD false #endif /* CVC4_DEBUG */ -#ifdef CVC4_STATISTICS_ON -# define IS_STATISTICS_BUILD true -#else /* CVC4_STATISTICS_ON */ -# define IS_STATISTICS_BUILD false -#endif /* CVC4_STATISTICS_ON */ - #ifdef CVC4_TRACING # define IS_TRACING_BUILD true #else /* CVC4_TRACING */ diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 2ca6ab605..2595ab4c0 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -64,6 +64,8 @@ libcvc4_add_sources( statistics.h statistics_registry.cpp statistics_registry.h + statistics_value.cpp + statistics_value.h stats_base.cpp stats_base.h stats_histogram.h diff --git a/src/util/statistics_stats.cpp b/src/util/statistics_stats.cpp new file mode 100644 index 000000000..8aa686e5d --- /dev/null +++ b/src/util/statistics_stats.cpp @@ -0,0 +1,135 @@ +/********************* */ +/*! \file statistics_stats.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 Basic statistics representation + ** + ** The basic statistics classes. + **/ + +#include "util/statistics_stats.h" + +#include "base/check.h" +#include "util/statistics_value.h" + +namespace cvc5 { + +AverageStat& AverageStat::operator<<(double v) +{ + if constexpr (Configuration::isStatisticsBuild()) + { + d_data->d_sum += v; + d_data->d_count++; + } + return *this; +} + +IntStat& IntStat::operator=(int64_t val) +{ + if constexpr (Configuration::isStatisticsBuild()) + { + d_data->d_value = val; + } + return *this; +} + +IntStat& IntStat::operator++() +{ + if constexpr (Configuration::isStatisticsBuild()) + { + d_data->d_value++; + } + return *this; +} + +IntStat& IntStat::operator++(int) +{ + if constexpr (Configuration::isStatisticsBuild()) + { + d_data->d_value++; + } + return *this; +} + +IntStat& IntStat::operator+=(int64_t val) +{ + if constexpr (Configuration::isStatisticsBuild()) + { + d_data->d_value += val; + } + return *this; +} + +void IntStat::maxAssign(int64_t val) +{ + if (d_data->d_value < val) + { + d_data->d_value = val; + } +} + +void IntStat::minAssign(int64_t val) +{ + if (d_data->d_value > val) + { + d_data->d_value = val; + } +} + +void TimerStat::start() +{ + if constexpr (Configuration::isStatisticsBuild()) + { + Assert(!d_data->d_running) << "timer is already running"; + d_data->d_start = StatisticTimerValue::clock::now(); + d_data->d_running = true; + } +} +void TimerStat::stop() +{ + if constexpr (Configuration::isStatisticsBuild()) + { + Assert(d_data->d_running) << "timer is not running"; + d_data->d_duration += StatisticTimerValue::clock::now() - d_data->d_start; + d_data->d_running = false; + } +} +bool TimerStat::running() const +{ + if constexpr (Configuration::isStatisticsBuild()) + { + return d_data->d_running; + } + return false; +} + +CodeTimer::CodeTimer(TimerStat& timer, bool allow_reentrant) + : d_timer(timer), d_reentrant(false) +{ + if constexpr (Configuration::isStatisticsBuild()) + { + if (!allow_reentrant || !(d_reentrant = d_timer.running())) + { + d_timer.start(); + } + } +} +CodeTimer::~CodeTimer() +{ + if constexpr (Configuration::isStatisticsBuild()) + { + if (!d_reentrant) + { + d_timer.stop(); + } + } +} + +} // namespace cvc5 diff --git a/src/util/statistics_stats.h b/src/util/statistics_stats.h new file mode 100644 index 000000000..9757c31cc --- /dev/null +++ b/src/util/statistics_stats.h @@ -0,0 +1,340 @@ +/********************* */ +/*! \file statistics_stats.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 Statistic proxy objects + ** + ** Conceptually, every statistic consists of a data object and a proxy + ** object. The proxy objects are issued by the `StatisticsRegistry` and + ** maintained by the user. They only hold a pointer to a matching data + ** object. The purpose of proxy objects is to implement methods to easily + ** change the statistic data, but shield the regular user from the internals. + */ + +#include "cvc4_private_library.h" + +#ifndef CVC4__UTIL__STATISTICS_STATS_H +#define CVC4__UTIL__STATISTICS_STATS_H + +#include <optional> + +#include "base/configuration.h" + +namespace cvc5 { + +// forward declare all values to avoid inclusion +struct StatisticAverageValue; +template <typename T> +struct StatisticBackedValue; +template <typename T> +struct StatisticHistogramValue; +template <typename T> +struct StatisticReferenceValue; +template <typename T> +struct StatisticSizeValue; +struct StatisticTimerValue; + +class StatisticsRegistry; + +/** + * Collects the average of a series of double values. + * New values are added by + * AverageStat stat; + * stat << 1.0 << 2.0; + */ +class AverageStat +{ + public: + /** Allow access to private constructor */ + friend class StatisticsRegistry; + /** Value stored for this statistic */ + using stat_type = StatisticAverageValue; + /** Add the value `v` to the running average */ + AverageStat& operator<<(double v); + + private: + /** Construct from a pointer to the internal data */ + AverageStat(stat_type* data) : d_data(data) {} + /** The actual data that lives in the registry */ + stat_type* d_data; +}; + +/** + * Collects a histogram over some type. + * The type needs to be (convertible to) integral and support streaming to + * an `std::ostream`. + * New values are added by + * HistogramStat<Kind> stat; + * stat << Kind::PLUS << Kind::AND; + */ +template <typename Integral> +class HistogramStat +{ + public: + /** Allow access to private constructor */ + friend class StatisticsRegistry; + /** Value stored for this statistic */ + using stat_type = StatisticHistogramValue<Integral>; + /** Add the value `val` to the histogram */ + HistogramStat& operator<<(Integral val) + { + if constexpr (Configuration::isStatisticsBuild()) + { + d_data->add(val); + } + return *this; + } + + private: + /** Construct from a pointer to the internal data */ + HistogramStat(stat_type* data) : d_data(data) {} + /** The actual data that lives in the registry */ + stat_type* d_data; +}; + +/** + * Stores the reference to some value that exists outside of this statistic. + * Despite being called `ReferenceStat`, the reference is held as a pointer + * and can thus be reset using `set`. + * Note that the referenced object must have a lifetime that is longer than + * the lifetime of the `ReferenceStat` object. Upon destruction of the + * `ReferenceStat` the current value of the referenced object is copied into + * the `StatisticsRegistry`. + * + * To convert to the API representation in `api::Stat`, `T` can only be one + * of the types accepted by the `api::Stat` constructors (or be implicitly + * converted to one of them). + */ +template <typename T> +class ReferenceStat +{ + public: + /** Allow access to private constructor */ + friend class StatisticsRegistry; + /** Value stored for this statistic */ + using stat_type = StatisticReferenceValue<T>; + /** Reset the reference to point to `t`. */ + void set(const T& t) + { + if constexpr (Configuration::isStatisticsBuild()) + { + d_data->d_value = &t; + } + } + /** Copy the current value of the referenced object. */ + ~ReferenceStat() + { + if constexpr (Configuration::isStatisticsBuild()) + { + d_data->commit(); + } + } + + private: + /** Construct from a pointer to the internal data */ + ReferenceStat(StatisticReferenceValue<T>* data) : d_data(data) {} + /** The actual data that lives in the registry */ + StatisticReferenceValue<T>* d_data; +}; + +/** + * Stores the size of some container that exists outside of this statistic. + * Note that the referenced container must have a lifetime that is longer than + * the lifetime of the `SizeStat` object. Upon destruction of the `SizeStat` + * the current size of the referenced container is copied into the + * `StatisticsRegistry`. + */ +template <typename T> +class SizeStat +{ + public: + /** Allow access to private constructor */ + friend class StatisticsRegistry; + /** Value stored for this statistic */ + using stat_type = StatisticSizeValue<T>; + /** Reset the reference to point to `t`. */ + void set(const T& t) + { + if constexpr (Configuration::isStatisticsBuild()) + { + d_data->d_value = &t; + } + } + /** Copy the current size of the referenced container. */ + ~SizeStat() + { + if constexpr (Configuration::isStatisticsBuild()) + { + d_data->commit(); + } + } + + private: + /** Construct from a pointer to the internal data */ + SizeStat(stat_type* data) : d_data(data) {} + /** The actual data that lives in the registry */ + stat_type* d_data; +}; + +class CodeTimer; +/** + * Collects cumulative runtimes. The timer can be started and stopped + * arbitrarily like a stopwatch. The value of the statistic is the + * accumulated time over all (start,stop) pairs. + * While the runtimes are stored in nanosecond precision internally, + * the API exports runtimes as integral numbers in millisecond + * precision. + * + * Note that it is recommended to use it in an RAII fashion using the + * `CodeTimer` class. + */ +class TimerStat +{ + public: + /** Utility for RAII-style timing of code blocks */ + using CodeTimer = cvc5::CodeTimer; + /** Allow access to private constructor */ + friend class StatisticsRegistry; + /** Value stored for this statistic */ + using stat_type = StatisticTimerValue; + + /** Start the timer. Assumes it is not already running. */ + void start(); + /** Stop the timer. Assumes it is running. */ + void stop(); + /** Checks whether the timer is running. */ + bool running() const; + + private: + /** Construct from a pointer to the internal data */ + TimerStat(stat_type* data) : d_data(data) {} + /** The actual data that lives in the registry */ + stat_type* d_data; +}; + +/** + * Utility class to make it easier to call `stop` at the end of a code + * block. When constructed, it starts the timer. When destructed, it stops + * the timer. + * + * Allows for reentrant usage. If `allow_reentrant` is true, we check + * whether the timer is already running. If so, this particular instance + * of `CodeTimer` neither starts nor stops the actual timer, but leaves + * this to the first (or outermost) `CodeTimer`. + */ +class CodeTimer +{ + public: + /** Disallow copying */ + CodeTimer(const CodeTimer& timer) = delete; + /** Disallow assignment */ + CodeTimer& operator=(const CodeTimer& timer) = delete; + /** + * Start the timer. + * If `allow_reentrant` is true we check whether the timer is already + * running. If so, this particular instance of `CodeTimer` neither starts + * nor stops the actual timer, but leaves this to the first (or outermost) + * `CodeTimer`. + */ + CodeTimer(TimerStat& timer, bool allow_reentrant = false); + /** Stop the timer */ + ~CodeTimer(); + + private: + /** Reference to the timer this utility works on */ + TimerStat& d_timer; + /** Whether this timer is reentrant (i.e. does not do anything) */ + bool d_reentrant; +}; + +/** + * Stores a simple value that can be set manually using regular assignment + * or the `set` method. + * + * To convert to the API representation in `api::Stat`, `T` can only be one + * of the types accepted by the `api::Stat` constructors (or be implicitly + * converted to one of them). + */ +template <typename T> +class ValueStat +{ + public: + /** Allow access to private constructor */ + friend class StatisticsRegistry; + friend class IntStat; + /** Value stored for this statistic */ + using stat_type = StatisticBackedValue<T>; + /** Set to `t` */ + void set(const T& t) + { + if constexpr (Configuration::isStatisticsBuild()) + { + d_data->d_value = t; + } + } + /** Set to `t` */ + ValueStat<T>& operator=(const T& t) + { + if constexpr (Configuration::isStatisticsBuild()) + { + set(t); + } + return *this; + } + T get() const + { + if constexpr (Configuration::isStatisticsBuild()) + { + return d_data->d_value; + } + return T(); + } + + private: + /** Construct from a pointer to the internal data */ + ValueStat(StatisticBackedValue<T>* data) : d_data(data) {} + /** The actual data that lives in the registry */ + StatisticBackedValue<T>* d_data; +}; + +/** + * Stores an integer value as int64_t. + * Supports the most useful standard operators (assignment, pre- and + * post-increment, addition assignment) and some custom ones (maximum + * assignment, minimum assignment). + */ +class IntStat : public ValueStat<int64_t> +{ + public: + /** Allow access to private constructor */ + friend class StatisticsRegistry; + /** Value stored for this statistic */ + using stat_type = StatisticBackedValue<int64_t>; + /** Set to given value */ + IntStat& operator=(int64_t val); + /** Pre-increment for the integer */ + IntStat& operator++(); + /** Post-increment for the integer */ + IntStat& operator++(int); + /** Add `val` to the integer */ + IntStat& operator+=(int64_t val); + /** Assign the maximum of the current value and `val` */ + void maxAssign(int64_t val); + /** Assign the minimum of the current value and `val` */ + void minAssign(int64_t val); + + private: + /** Construct from a pointer to the internal data */ + IntStat(stat_type* data) : ValueStat(data) {} +}; + +} // namespace cvc5 + +#endif diff --git a/src/util/statistics_value.cpp b/src/util/statistics_value.cpp new file mode 100644 index 000000000..6db0b3cd3 --- /dev/null +++ b/src/util/statistics_value.cpp @@ -0,0 +1,126 @@ +/********************* */ +/*! \file statistics_value.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 Statistic data classes + ** + ** The statistic data classes that actually hold the data for the statistics. + ** + ** Conceptually, every statistic consists of a data object and a proxy object. + ** The data objects (statistic values) are derived from `StatisticBaseValue` + ** and live in the `StatisticsRegistry`. + ** They are solely exported to the proxy objects, which should be the sole + ** way to manipulate the data of a data object. + ** The data objects themselves need to implement printing (normal and safe) and + ** conversion to the API type `Stat`. + **/ + +#include "util/statistics_value.h" + +#include "util/ostream_util.h" + +namespace cvc5 { + +// standard helper, see https://en.cppreference.com/w/cpp/utility/variant/visit +template <class... Ts> +struct overloaded : Ts... +{ + using Ts::operator()...; +}; +template <class... Ts> +overloaded(Ts...) -> overloaded<Ts...>; + +namespace detail { +std::ostream& print(std::ostream& out, const StatExportData& sed) +{ + std::visit(overloaded{ + [&out](std::monostate v) { out << "<unset>"; }, + [&out](int64_t v) { out << v; }, + [&out](uint64_t v) { out << v; }, + [&out](double v) { out << v; }, + [&out](const std::string& v) { out << v; }, + [&out](const std::map<std::string, uint64_t>& v) { + out << "{ "; + bool first = true; + for (const auto& e : v) + { + if (!first) + out << ", "; + else + first = false; + out << e.first << ": " << e.second; + } + out << " }"; + }, + }, + sed); + return out; +} +} + +StatisticBaseValue::~StatisticBaseValue() {} + +std::ostream& operator<<(std::ostream& out, const StatisticBaseValue& sbv) +{ + return detail::print(out, sbv.hasValue() ? sbv.getViewer() : StatExportData{}); +} + +StatExportData StatisticAverageValue::getViewer() const { return get(); } + +bool StatisticAverageValue::hasValue() const { return d_count > 0; } + +void StatisticAverageValue::print(std::ostream& out) const { out << get(); } + +void StatisticAverageValue::printSafe(int fd) const +{ + safe_print<double>(fd, get()); +} + +double StatisticAverageValue::get() const { return d_sum / d_count; } + +StatExportData StatisticTimerValue::getViewer() const +{ + return static_cast<int64_t>(get() / std::chrono::milliseconds(1)); +} + +bool StatisticTimerValue::hasValue() const +{ + return d_running || d_duration.count() > 0; +} + +void StatisticTimerValue::print(std::ostream& out) const +{ + StreamFormatScope format_scope(out); + duration dur = get(); + + out << (dur / std::chrono::seconds(1)) << "." << std::setfill('0') + << std::setw(9) << std::right << (dur % std::chrono::seconds(1)).count(); +} + +void StatisticTimerValue::printSafe(int fd) const +{ + duration dur = get(); + safe_print<uint64_t>(fd, dur / std::chrono::seconds(1)); + safe_print(fd, "."); + safe_print_right_aligned(fd, (dur % std::chrono::seconds(1)).count(), 9); +} + +/** Make sure that we include the time of a currently running timer */ +StatisticTimerValue::duration StatisticTimerValue::get() const +{ + auto data = d_duration; + if (d_running) + { + data += clock::now() - d_start; + } + return data; +} + +} // namespace cvc5 diff --git a/src/util/statistics_value.h b/src/util/statistics_value.h new file mode 100644 index 000000000..a272c7a05 --- /dev/null +++ b/src/util/statistics_value.h @@ -0,0 +1,402 @@ +/********************* */ +/*! \file statistics_value.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 Statistic data classes + ** + ** The statistic data classes that actually hold the data for the statistics. + ** + ** Conceptually, every statistic consists of a data object and a proxy object. + ** The data objects (statistic values) are derived from `StatisticBaseValue` + ** and live in the `StatisticsRegistry`. + ** They are solely exported to the proxy objects, which should be the sole + ** way to manipulate the data of a data object. + ** The data objects themselves need to implement printing (normal and safe) and + ** conversion to the API type `Stat`. + **/ + +#include "cvc4_private_library.h" + +#ifndef CVC4__UTIL__STATISTICS_VALUE_H +#define CVC4__UTIL__STATISTICS_VALUE_H + +#include <chrono> +#include <iomanip> +#include <map> +#include <optional> +#include <sstream> +#include <variant> +#include <vector> + +#include "util/safe_print.h" + +namespace cvc5 { + +class StatisticsRegistry; + +using StatExportData = std::variant<std::monostate, + int64_t, + double, + std::string, + std::map<std::string, uint64_t>>; +namespace detail { + std::ostream& print(std::ostream& out, const StatExportData& sed); +} + +/** + * Base class for all statistic values. + */ +struct StatisticBaseValue +{ + virtual ~StatisticBaseValue(); + /** Checks whether the data holds a non-default value. */ + virtual bool hasValue() const = 0; + /** + * Converts the internal data to an instance of `StatExportData` that is + * suitable for printing and exporting to the API. + * Assumes that `hasValue` returns true. Otherwise, the return value should + * assumed to be `std::monostate`. + */ + virtual StatExportData getViewer() const = 0; + /** + * Writes the data to a regular `std::ostream`. + * Assumes that `hasValue` returns true. Otherwise, the user should write + * `<undef>` to the stream. + */ + virtual void print(std::ostream&) const = 0; + /** + * Safely writes the data to a file descriptor. Is suitable to be used + * within a signal handler. + * Assumes that `hasValue` returns true. Otherwise, the user should write + * `<undef>` to the file descriptor. + */ + virtual void printSafe(int fd) const = 0; + + bool d_expert = true; +}; +/** Writes the data to an output stream */ +std::ostream& operator<<(std::ostream& out, const StatisticBaseValue& sbv); + +/** Holds the data for an running average statistic */ +struct StatisticAverageValue : StatisticBaseValue +{ + StatExportData getViewer() const override; + bool hasValue() const override; + void print(std::ostream& out) const override; + void printSafe(int fd) const override; + double get() const; + + /** Sum of added values */ + double d_sum; + /** Number of added values */ + uint64_t d_count; +}; + +/** + * Holds some value of type `T`. + * + * To convert to the API representation in `getViewer`, `T` can only be one + * of the types listed in `Stat::d_data` (or be implicitly converted to + * one of them). + */ +template <typename T> +struct StatisticBackedValue : StatisticBaseValue +{ + StatExportData getViewer() const override { return d_value; } + bool hasValue() const override { return d_value != T(); } + void print(std::ostream& out) const override { out << d_value; } + void printSafe(int fd) const override { safe_print<T>(fd, d_value); } + + T d_value; +}; + +/** + * Holds the data for a histogram. We assume the type to be (convertible to) + * integral, and we can thus use a std::vector<uint64_t> for fast storage. + * The core idea is to track the minimum and maximum values `[a,b]` that have + * been added to the histogram and maintain a vector with `b-a+1` values. + * The vector is resized on demand to grow as necessary and supports negative + * values as well. + * Note that the template type needs to have a streaming operator to convert it + * to a string in `getViewer`. + */ +template <typename Integral> +struct StatisticHistogramValue : StatisticBaseValue +{ + static_assert(std::is_integral<Integral>::value + || std::is_enum<Integral>::value, + "Type should be a fundamental integral type."); + + /** + * Convert the internal representation to a `std::map<std::string, uint64_t>` + */ + StatExportData getViewer() const override + { + std::map<std::string, uint64_t> res; + for (size_t i = 0, n = d_hist.size(); i < n; ++i) + { + if (d_hist[i] > 0) + { + std::stringstream ss; + ss << static_cast<Integral>(i + d_offset); + res.emplace(ss.str(), d_hist[i]); + } + } + return res; + } + bool hasValue() const override { return d_hist.size() > 0; } + void print(std::ostream& out) const override + { + out << "["; + bool first = true; + for (size_t i = 0, n = d_hist.size(); i < n; ++i) + { + if (d_hist[i] > 0) + { + if (first) + { + first = false; + } + else + { + out << ", "; + } + out << "(" << static_cast<Integral>(i + d_offset) << " : " << d_hist[i] + << ")"; + } + } + out << "]"; + } + void printSafe(int fd) const override + { + safe_print(fd, "["); + bool first = true; + for (size_t i = 0, n = d_hist.size(); i < n; ++i) + { + if (d_hist[i] > 0) + { + if (first) + { + first = false; + } + else + { + safe_print(fd, ", "); + } + safe_print(fd, "("); + safe_print<Integral>(fd, static_cast<Integral>(i + d_offset)); + safe_print(fd, " : "); + safe_print<uint64_t>(fd, d_hist[i]); + safe_print(fd, ")"); + } + } + safe_print(fd, "]"); + } + + /** + * Add `val` to the histogram. Casts `val` to `int64_t`, then resizes and + * moves the vector entries as necessary. + */ + void add(Integral val) + { + int64_t v = static_cast<int64_t>(val); + if (d_hist.empty()) + { + d_offset = v; + } + if (v < d_offset) + { + d_hist.insert(d_hist.begin(), d_offset - v, 0); + d_offset = v; + } + if (static_cast<size_t>(v - d_offset) >= d_hist.size()) + { + d_hist.resize(v - d_offset + 1); + } + d_hist[v - d_offset]++; + } + + /** Actual data */ + std::vector<uint64_t> d_hist; + /** Offset of the entries. d_hist[i] corresponds to Interval(d_offset + i) */ + int64_t d_offset; +}; + +/** + * Holds the data for a `ReferenceStat`. + * When the `ReferenceStat` is destroyed the current value is copied into + * `d_committed`. Once `d_committed` is set, this value is returned, even if + * the reference is still valid. + */ +template <typename T> +struct StatisticReferenceValue : StatisticBaseValue +{ + StatExportData getViewer() const override + { + if (d_committed) + { + if constexpr (std::is_integral_v<T>) + { + return static_cast<int64_t>(*d_committed); + } + else + { + // this else branch is required to ensure compilation. + // if T is unsigned int, this return statement triggers a compiler error + return *d_committed; + } + } + else if (d_value != nullptr) + { + if constexpr (std::is_integral_v<T>) + { + return static_cast<int64_t>(*d_value); + } + else + { + // this else branch is required to ensure compilation. + // if T is unsigned int, this return statement triggers a compiler error + return *d_value; + } + } + return {}; + } + bool hasValue() const override { return d_committed || d_value != nullptr; } + void print(std::ostream& out) const override + { + if (d_committed) + { + out << *d_committed; + } + else if (d_value != nullptr) + { + out << *d_value; + } + } + void printSafe(int fd) const override + { + if (d_committed) + { + safe_print<T>(fd, *d_committed); + } + else if (d_value != nullptr) + { + safe_print<T>(fd, *d_value); + } + } + void commit() + { + if (d_value != nullptr) + { + d_committed = *d_value; + } + } + const T& get() const { return d_committed ? *d_committed : *d_value; } + + const T* d_value = nullptr; + std::optional<T> d_committed; +}; + +/** + * Holds the data for a `SizeStat`. + * When the `SizeStat` is destroyed the current size is copied into + * `d_committed`. Once `d_committed` is set, this value is returned, even if + * the reference is still valid. + */ +template <typename T> +struct StatisticSizeValue : StatisticBaseValue +{ + StatExportData getViewer() const override + { + if (d_committed) + { + return static_cast<int64_t>(*d_committed); + } + else if (d_value != nullptr) + { + return static_cast<int64_t>(d_value->size()); + } + return {}; + } + bool hasValue() const override { return d_committed || d_value != nullptr; } + void print(std::ostream& out) const override + { + if (d_committed) + { + out << *d_committed; + } + else if (d_value != nullptr) + { + out << d_value->size(); + } + } + void printSafe(int fd) const override + { + if (d_committed) + { + safe_print(fd, *d_committed); + } + else if (d_value != nullptr) + { + safe_print(fd, d_value->size()); + } + } + void commit() + { + if (d_value != nullptr) + { + d_committed = d_value->size(); + } + } + size_t get() const { return d_committed ? *d_committed : d_value->size(); } + + const T* d_value = nullptr; + std::optional<std::size_t> d_committed; +}; + +/** + * Holds the data for a `TimerStat`. + * Uses `std::chrono` to obtain the current time, store a time point and sum up + * the total durations. + */ +struct StatisticTimerValue : StatisticBaseValue +{ + using clock = std::chrono::steady_clock; + using time_point = clock::time_point; + struct duration : public std::chrono::nanoseconds + { + }; + /** Returns the number of milliseconds */ + StatExportData getViewer() const override; + bool hasValue() const override; + /** Prints seconds in fixed-point format */ + void print(std::ostream& out) const override; + /** Prints seconds in fixed-point format */ + void printSafe(int fd) const override; + /** Make sure that we include the time of a currently running timer */ + duration get() const; + + /** + * The cumulative duration of the timer so far. + * Does not include a currently running timer, but `get()` takes care of this. + */ + duration d_duration; + /** + * The start time of a currently running timer. + * May not be reset when the timer is stopped. + */ + time_point d_start; + /** Whether a timer is running right now. */ + bool d_running; +}; + +} // namespace cvc5 + +#endif |