1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
/******************************************************************************
* Top contributors (to current version):
* Gereon Kremer, Mathias Preiner, Tim King
*
* This file is part of the cvc5 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.
* ****************************************************************************
*
* Histogram statistics.
*
* Stat classes that represent histograms.
*/
#include "cvc4_private_library.h"
#ifndef CVC5__UTIL__STATS_HISTOGRAM_H
#define CVC5__UTIL__STATS_HISTOGRAM_H
#include <map>
#include <vector>
#include "util/stats_base.h"
namespace cvc5 {
/**
* A histogram statistic class for integral types.
* Avoids using an std::map (like we would do for generic types) 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
* 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.");
public:
/** Construct a histogram of a stream of entries. */
IntegralHistogramStat(const std::string& name) : Stat(name) {}
void flushInformation(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 safeFlushInformation(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, "]");
}
IntegralHistogramStat& operator<<(Integral val)
{
if (CVC5_USE_STATISTICS)
{
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]++;
}
return (*this);
}
private:
std::vector<uint64_t> d_hist;
int64_t d_offset;
}; /* class IntegralHistogramStat */
} // namespace cvc5
#endif
|
