1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Gereon Kremer |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Statistic proxy objects |
14 |
|
* |
15 |
|
* Conceptually, every statistic consists of a data object and a proxy |
16 |
|
* object. The proxy objects are issued by the `StatisticsRegistry` and |
17 |
|
* maintained by the user. They only hold a pointer to a matching data |
18 |
|
* object. The purpose of proxy objects is to implement methods to easily |
19 |
|
* change the statistic data, but shield the regular user from the internals. |
20 |
|
*/ |
21 |
|
|
22 |
|
#include "cvc5_private_library.h" |
23 |
|
|
24 |
|
#ifndef CVC5__UTIL__STATISTICS_STATS_H |
25 |
|
#define CVC5__UTIL__STATISTICS_STATS_H |
26 |
|
|
27 |
|
#include <optional> |
28 |
|
|
29 |
|
#include "base/configuration.h" |
30 |
|
|
31 |
|
namespace cvc5 { |
32 |
|
|
33 |
|
// forward declare all values to avoid inclusion |
34 |
|
struct StatisticAverageValue; |
35 |
|
template <typename T> |
36 |
|
struct StatisticBackedValue; |
37 |
|
template <typename T> |
38 |
|
struct StatisticHistogramValue; |
39 |
|
template <typename T> |
40 |
|
struct StatisticReferenceValue; |
41 |
|
template <typename T> |
42 |
|
struct StatisticSizeValue; |
43 |
|
struct StatisticTimerValue; |
44 |
|
|
45 |
|
class StatisticsRegistry; |
46 |
|
|
47 |
|
/** |
48 |
|
* Collects the average of a series of double values. |
49 |
|
* New values are added by |
50 |
|
* AverageStat stat; |
51 |
|
* stat << 1.0 << 2.0; |
52 |
|
*/ |
53 |
|
class AverageStat |
54 |
|
{ |
55 |
|
public: |
56 |
|
/** Allow access to private constructor */ |
57 |
|
friend class StatisticsRegistry; |
58 |
|
/** Value stored for this statistic */ |
59 |
|
using stat_type = StatisticAverageValue; |
60 |
|
/** Add the value `v` to the running average */ |
61 |
|
AverageStat& operator<<(double v); |
62 |
|
|
63 |
|
private: |
64 |
|
/** Construct from a pointer to the internal data */ |
65 |
39666 |
AverageStat(stat_type* data) : d_data(data) {} |
66 |
|
/** The actual data that lives in the registry */ |
67 |
|
stat_type* d_data; |
68 |
|
}; |
69 |
|
|
70 |
|
/** |
71 |
|
* Collects a histogram over some type. |
72 |
|
* The type needs to be (convertible to) integral and support streaming to |
73 |
|
* an `std::ostream`. |
74 |
|
* New values are added by |
75 |
|
* HistogramStat<Kind> stat; |
76 |
|
* stat << Kind::PLUS << Kind::AND; |
77 |
|
*/ |
78 |
|
template <typename Integral> |
79 |
|
class HistogramStat |
80 |
|
{ |
81 |
|
public: |
82 |
|
/** Allow access to private constructor */ |
83 |
|
friend class StatisticsRegistry; |
84 |
|
/** Value stored for this statistic */ |
85 |
|
using stat_type = StatisticHistogramValue<Integral>; |
86 |
|
/** Add the value `val` to the histogram */ |
87 |
99428484 |
HistogramStat& operator<<(Integral val) |
88 |
|
{ |
89 |
|
if constexpr (Configuration::isStatisticsBuild()) |
90 |
|
{ |
91 |
99428484 |
d_data->add(val); |
92 |
|
} |
93 |
99428484 |
return *this; |
94 |
|
} |
95 |
|
|
96 |
|
private: |
97 |
|
/** Construct from a pointer to the internal data */ |
98 |
1076292 |
HistogramStat(stat_type* data) : d_data(data) {} |
99 |
|
/** The actual data that lives in the registry */ |
100 |
|
stat_type* d_data; |
101 |
|
}; |
102 |
|
|
103 |
|
/** |
104 |
|
* Stores the reference to some value that exists outside of this statistic. |
105 |
|
* Despite being called `ReferenceStat`, the reference is held as a pointer |
106 |
|
* and can thus be reset using `set`. |
107 |
|
* Note that the referenced object must have a lifetime that is longer than |
108 |
|
* the lifetime of the `ReferenceStat` object. Upon destruction of the |
109 |
|
* `ReferenceStat` the current value of the referenced object is copied into |
110 |
|
* the `StatisticsRegistry`. |
111 |
|
* |
112 |
|
* To convert to the API representation in `api::Stat`, `T` can only be one |
113 |
|
* of the types accepted by the `api::Stat` constructors (or be implicitly |
114 |
|
* converted to one of them). |
115 |
|
*/ |
116 |
|
template <typename T> |
117 |
|
class ReferenceStat |
118 |
|
{ |
119 |
|
public: |
120 |
|
/** Allow access to private constructor */ |
121 |
|
friend class StatisticsRegistry; |
122 |
|
/** Value stored for this statistic */ |
123 |
|
using stat_type = StatisticReferenceValue<T>; |
124 |
|
/** Reset the reference to point to `t`. */ |
125 |
|
template <typename TT> |
126 |
132814 |
void set(const TT& t) |
127 |
|
{ |
128 |
|
static_assert(std::is_same_v<T, TT>, "Incorrect type for ReferenceStat"); |
129 |
|
if constexpr (Configuration::isStatisticsBuild()) |
130 |
|
{ |
131 |
132814 |
d_data->d_value = &t; |
132 |
|
} |
133 |
132814 |
} |
134 |
|
/** Commit the value currently pointed to and release it. */ |
135 |
89851 |
void reset() |
136 |
|
{ |
137 |
|
if constexpr (Configuration::isStatisticsBuild()) |
138 |
|
{ |
139 |
89851 |
d_data->commit(); |
140 |
89851 |
d_data->d_value = nullptr; |
141 |
|
} |
142 |
89851 |
} |
143 |
|
/** Copy the current value of the referenced object. */ |
144 |
130136 |
~ReferenceStat() |
145 |
|
{ |
146 |
|
if constexpr (Configuration::isStatisticsBuild()) |
147 |
|
{ |
148 |
130136 |
d_data->commit(); |
149 |
|
} |
150 |
130136 |
} |
151 |
|
|
152 |
|
private: |
153 |
|
/** Construct from a pointer to the internal data */ |
154 |
132814 |
ReferenceStat(StatisticReferenceValue<T>* data) : d_data(data) {} |
155 |
|
/** The actual data that lives in the registry */ |
156 |
|
StatisticReferenceValue<T>* d_data; |
157 |
|
}; |
158 |
|
|
159 |
|
/** |
160 |
|
* Stores the size of some container that exists outside of this statistic. |
161 |
|
* Note that the referenced container must have a lifetime that is longer than |
162 |
|
* the lifetime of the `SizeStat` object. Upon destruction of the `SizeStat` |
163 |
|
* the current size of the referenced container is copied into the |
164 |
|
* `StatisticsRegistry`. |
165 |
|
*/ |
166 |
|
template <typename T> |
167 |
|
class SizeStat |
168 |
|
{ |
169 |
|
public: |
170 |
|
/** Allow access to private constructor */ |
171 |
|
friend class StatisticsRegistry; |
172 |
|
/** Value stored for this statistic */ |
173 |
|
using stat_type = StatisticSizeValue<T>; |
174 |
|
/** Reset the reference to point to `t`. */ |
175 |
9919 |
void set(const T& t) |
176 |
|
{ |
177 |
|
if constexpr (Configuration::isStatisticsBuild()) |
178 |
|
{ |
179 |
9919 |
d_data->d_value = &t; |
180 |
|
} |
181 |
9919 |
} |
182 |
|
/** Copy the current size of the referenced container. */ |
183 |
9916 |
~SizeStat() |
184 |
|
{ |
185 |
|
if constexpr (Configuration::isStatisticsBuild()) |
186 |
|
{ |
187 |
9916 |
d_data->commit(); |
188 |
|
} |
189 |
9916 |
} |
190 |
|
|
191 |
|
private: |
192 |
|
/** Construct from a pointer to the internal data */ |
193 |
9919 |
SizeStat(stat_type* data) : d_data(data) {} |
194 |
|
/** The actual data that lives in the registry */ |
195 |
|
stat_type* d_data; |
196 |
|
}; |
197 |
|
|
198 |
|
class CodeTimer; |
199 |
|
/** |
200 |
|
* Collects cumulative runtimes. The timer can be started and stopped |
201 |
|
* arbitrarily like a stopwatch. The value of the statistic is the |
202 |
|
* accumulated time over all (start,stop) pairs. |
203 |
|
* While the runtimes are stored in nanosecond precision internally, |
204 |
|
* the API exports runtimes as integral numbers in millisecond |
205 |
|
* precision. |
206 |
|
* |
207 |
|
* Note that it is recommended to use it in an RAII fashion using the |
208 |
|
* `CodeTimer` class. |
209 |
|
*/ |
210 |
|
class TimerStat |
211 |
|
{ |
212 |
|
public: |
213 |
|
/** Utility for RAII-style timing of code blocks */ |
214 |
|
using CodeTimer = cvc5::CodeTimer; |
215 |
|
/** Allow access to private constructor */ |
216 |
|
friend class StatisticsRegistry; |
217 |
|
/** Value stored for this statistic */ |
218 |
|
using stat_type = StatisticTimerValue; |
219 |
|
|
220 |
|
/** Start the timer. Assumes it is not already running. */ |
221 |
|
void start(); |
222 |
|
/** Stop the timer. Assumes it is running. */ |
223 |
|
void stop(); |
224 |
|
/** Checks whether the timer is running. */ |
225 |
|
bool running() const; |
226 |
|
|
227 |
|
private: |
228 |
|
/** Construct from a pointer to the internal data */ |
229 |
1129321 |
TimerStat(stat_type* data) : d_data(data) {} |
230 |
|
/** The actual data that lives in the registry */ |
231 |
|
stat_type* d_data; |
232 |
|
}; |
233 |
|
|
234 |
|
/** |
235 |
|
* Utility class to make it easier to call `stop` at the end of a code |
236 |
|
* block. When constructed, it starts the timer. When destructed, it stops |
237 |
|
* the timer. |
238 |
|
* |
239 |
|
* Allows for reentrant usage. If `allow_reentrant` is true, we check |
240 |
|
* whether the timer is already running. If so, this particular instance |
241 |
|
* of `CodeTimer` neither starts nor stops the actual timer, but leaves |
242 |
|
* this to the first (or outermost) `CodeTimer`. |
243 |
|
*/ |
244 |
|
class CodeTimer |
245 |
|
{ |
246 |
|
public: |
247 |
|
/** Disallow copying */ |
248 |
|
CodeTimer(const CodeTimer& timer) = delete; |
249 |
|
/** Disallow assignment */ |
250 |
|
CodeTimer& operator=(const CodeTimer& timer) = delete; |
251 |
|
/** |
252 |
|
* Start the timer. |
253 |
|
* If `allow_reentrant` is true we check whether the timer is already |
254 |
|
* running. If so, this particular instance of `CodeTimer` neither starts |
255 |
|
* nor stops the actual timer, but leaves this to the first (or outermost) |
256 |
|
* `CodeTimer`. |
257 |
|
*/ |
258 |
|
CodeTimer(TimerStat& timer, bool allow_reentrant = false); |
259 |
|
/** Stop the timer */ |
260 |
|
~CodeTimer(); |
261 |
|
|
262 |
|
private: |
263 |
|
/** Reference to the timer this utility works on */ |
264 |
|
TimerStat& d_timer; |
265 |
|
/** Whether this timer is reentrant (i.e. does not do anything) */ |
266 |
|
bool d_reentrant; |
267 |
|
}; |
268 |
|
|
269 |
|
/** |
270 |
|
* Stores a simple value that can be set manually using regular assignment |
271 |
|
* or the `set` method. |
272 |
|
* |
273 |
|
* To convert to the API representation in `api::Stat`, `T` can only be one |
274 |
|
* of the types accepted by the `api::Stat` constructors (or be implicitly |
275 |
|
* converted to one of them). |
276 |
|
*/ |
277 |
|
template <typename T> |
278 |
|
class ValueStat |
279 |
|
{ |
280 |
|
public: |
281 |
|
/** Allow access to private constructor */ |
282 |
|
friend class StatisticsRegistry; |
283 |
|
friend class IntStat; |
284 |
|
/** Value stored for this statistic */ |
285 |
|
using stat_type = StatisticBackedValue<T>; |
286 |
|
/** Set to `t` */ |
287 |
6227 |
void set(const T& t) |
288 |
|
{ |
289 |
|
if constexpr (Configuration::isStatisticsBuild()) |
290 |
|
{ |
291 |
6227 |
d_data->d_value = t; |
292 |
|
} |
293 |
6227 |
} |
294 |
|
/** Set to `t` */ |
295 |
|
ValueStat<T>& operator=(const T& t) |
296 |
|
{ |
297 |
|
if constexpr (Configuration::isStatisticsBuild()) |
298 |
|
{ |
299 |
|
set(t); |
300 |
|
} |
301 |
|
return *this; |
302 |
|
} |
303 |
68457 |
T get() const |
304 |
|
{ |
305 |
|
if constexpr (Configuration::isStatisticsBuild()) |
306 |
|
{ |
307 |
68457 |
return d_data->d_value; |
308 |
|
} |
309 |
|
return T(); |
310 |
|
} |
311 |
|
|
312 |
|
private: |
313 |
|
/** Construct from a pointer to the internal data */ |
314 |
3095558 |
ValueStat(StatisticBackedValue<T>* data) : d_data(data) {} |
315 |
|
/** The actual data that lives in the registry */ |
316 |
|
StatisticBackedValue<T>* d_data; |
317 |
|
}; |
318 |
|
|
319 |
|
/** |
320 |
|
* Stores an integer value as int64_t. |
321 |
|
* Supports the most useful standard operators (assignment, pre- and |
322 |
|
* post-increment, addition assignment) and some custom ones (maximum |
323 |
|
* assignment, minimum assignment). |
324 |
|
*/ |
325 |
|
class IntStat : public ValueStat<int64_t> |
326 |
|
{ |
327 |
|
public: |
328 |
|
/** Allow access to private constructor */ |
329 |
|
friend class StatisticsRegistry; |
330 |
|
/** Value stored for this statistic */ |
331 |
|
using stat_type = StatisticBackedValue<int64_t>; |
332 |
|
/** Set to given value */ |
333 |
|
IntStat& operator=(int64_t val); |
334 |
|
/** Pre-increment for the integer */ |
335 |
|
IntStat& operator++(); |
336 |
|
/** Post-increment for the integer */ |
337 |
|
IntStat& operator++(int); |
338 |
|
/** Add `val` to the integer */ |
339 |
|
IntStat& operator+=(int64_t val); |
340 |
|
/** Assign the maximum of the current value and `val` */ |
341 |
|
void maxAssign(int64_t val); |
342 |
|
/** Assign the minimum of the current value and `val` */ |
343 |
|
void minAssign(int64_t val); |
344 |
|
|
345 |
|
private: |
346 |
|
/** Construct from a pointer to the internal data */ |
347 |
3076152 |
IntStat(stat_type* data) : ValueStat(data) {} |
348 |
|
}; |
349 |
|
|
350 |
|
} // namespace cvc5 |
351 |
|
|
352 |
|
#endif |