diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-17 09:17:03 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-17 09:17:03 +0100 |
commit | a1a2d9389730ed46ab246865e320108db07c30ff (patch) | |
tree | b48fa21590963c378a39e1f8a54e696a588f3179 /src | |
parent | 20d266f9e641062004633e24e74878791be2b919 (diff) |
Add new IntegralHistogramStat (#5898)
This PR adds a new statistics class that improves on HistogramStat if we know that the type is integral (also supporting enums).
Instead of using a comparably slow std::map like HistogramStat, IntegralHistogramStat uses a std::vector that is resized appropriately.
The integral values are simply cast to std::int64_t and used as indices into the vector.
Diffstat (limited to 'src')
-rw-r--r-- | src/util/statistics_registry.h | 104 |
1 files changed, 104 insertions, 0 deletions
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index f706f3321..d2f7244f9 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -639,6 +639,110 @@ public: };/* class HistogramStat */ +/** + * A histogram statistic class for integral types. + * Avoids using an std::map (like the generic HistogramStat) in favor of a + * faster std::vector by casting the integral values to indices into the + * vector. Requires the type to be an integral type that is convertible to + * std::int64_t, also supporting appropriate enum types. + * The vector is resized on demand to grow as necessary and supports negative + * values as well. + */ +template <typename Integral> +class IntegralHistogramStat : public Stat +{ + static_assert(std::is_integral<Integral>::value + || std::is_enum<Integral>::value, + "Type should be a fundamental integral type."); + + private: + std::vector<std::uint64_t> d_hist; + std::int64_t d_offset; + + public: + /** Construct a histogram of a stream of entries. */ + IntegralHistogramStat(const std::string& name) : Stat(name) {} + ~IntegralHistogramStat() {} + + void flushInformation(std::ostream& out) const override + { + if (CVC4_USE_STATISTICS) + { + out << "["; + bool first = true; + for (std::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 safeFlushInformation(int fd) const override + { + if (CVC4_USE_STATISTICS) + { + safe_print(fd, "["); + bool first = true; + for (std::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<std::uint64_t>(fd, d_hist[i]); + safe_print(fd, ")"); + } + } + safe_print(fd, "]"); + } + } + + IntegralHistogramStat& operator<<(Integral val) + { + if (CVC4_USE_STATISTICS) + { + std::int64_t v = static_cast<std::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<std::size_t>(v - d_offset) >= d_hist.size()) + { + d_hist.resize(v - d_offset + 1); + } + d_hist[v - d_offset]++; + } + return (*this); + } +}; /* class IntegralHistogramStat */ + /****************************************************************************/ /* Statistics Registry */ /****************************************************************************/ |