projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 20d266f) | patch
Add new IntegralHistogramStat (#5898)
authorGereon Kremer <gkremer@stanford.edu>
Wed, 17 Feb 2021 08:17:03 +0000 (09:17 +0100)
committerGitHub <noreply@github.com>
Wed, 17 Feb 2021 08:17:03 +0000 (09:17 +0100)
commita1a2d9389730ed46ab246865e320108db07c30ff
treeb48fa21590963c378a39e1f8a54e696a588f3179tree
parent20d266f9e641062004633e24e74878791be2b919commit | 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.
src/util/statistics_registry.h diff | blob | history
test/unit/util/stats_black.h diff | blob | history