Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Gereon Kremer, Andrew Reynolds, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 data classes.
14 : : *
15 : : * The statistic data classes that actually hold the data for the statistics.
16 : : *
17 : : * Conceptually, every statistic consists of a data object and a proxy object.
18 : : * The data objects (statistic values) are derived from `StatisticBaseValue`
19 : : * and live in the `StatisticsRegistry`.
20 : : * They are solely exported to the proxy objects, which should be the sole
21 : : * way to manipulate the data of a data object.
22 : : * The data objects themselves need to implement printing (normal and safe) and
23 : : * conversion to the API type `Stat`.
24 : : */
25 : :
26 : : #include "cvc5_private_library.h"
27 : :
28 : : #ifndef CVC5__UTIL__STATISTICS_VALUE_H
29 : : #define CVC5__UTIL__STATISTICS_VALUE_H
30 : :
31 : : #include <chrono>
32 : : #include <iomanip>
33 : : #include <map>
34 : : #include <optional>
35 : : #include <sstream>
36 : : #include <variant>
37 : : #include <vector>
38 : :
39 : : #include "util/safe_print.h"
40 : :
41 : : namespace cvc5::internal {
42 : :
43 : : class StatisticsRegistry;
44 : :
45 : : using StatExportData =
46 : : std::variant<int64_t, double, std::string, std::map<std::string, uint64_t>>;
47 : : namespace detail {
48 : : std::ostream& print(std::ostream& out, const StatExportData& sed);
49 : : }
50 : :
51 : : /**
52 : : * Base class for all statistic values.
53 : : */
54 : : struct StatisticBaseValue
55 : : {
56 : : virtual ~StatisticBaseValue();
57 : : /** Checks whether the data holds the default value. */
58 : : virtual bool isDefault() const = 0;
59 : : /**
60 : : * Converts the internal data to an instance of `StatExportData` that is
61 : : * suitable for printing and exporting to the API.
62 : : */
63 : : virtual StatExportData getViewer() const = 0;
64 : : /**
65 : : * Safely writes the data to a file descriptor. Is suitable to be used
66 : : * within a signal handler.
67 : : */
68 : : virtual void printSafe(int fd) const = 0;
69 : :
70 : : bool d_internal = true;
71 : : };
72 : : /** Writes the data to an output stream */
73 : : std::ostream& operator<<(std::ostream& out, const StatisticBaseValue& sbv);
74 : :
75 : : /** Holds the data for an running average statistic */
76 : : struct StatisticAverageValue : StatisticBaseValue
77 : : {
78 : : StatExportData getViewer() const override;
79 : : bool isDefault() const override;
80 : : void printSafe(int fd) const override;
81 : : double get() const;
82 : :
83 : : /** Sum of added values */
84 : : double d_sum;
85 : : /** Number of added values */
86 : : uint64_t d_count;
87 : : };
88 : :
89 : : /**
90 : : * Holds some value of type `T`.
91 : : *
92 : : * To convert to the API representation in `getViewer`, `T` can only be one
93 : : * of the types listed in `Stat::d_data` (or be implicitly converted to
94 : : * one of them).
95 : : */
96 : : template <typename T>
97 : : struct StatisticBackedValue : StatisticBaseValue
98 : : {
99 : 90940 : StatExportData getViewer() const override { return d_value; }
100 : 90938 : bool isDefault() const override { return d_value == T(); }
101 : 0 : void printSafe(int fd) const override { safe_print<T>(fd, d_value); }
102 : :
103 : : T d_value;
104 : : };
105 : :
106 : : /**
107 : : * Holds the data for a histogram. We assume the type to be (convertible to)
108 : : * integral, and we can thus use a std::vector<uint64_t> for fast storage.
109 : : * The core idea is to track the minimum and maximum values `[a,b]` that have
110 : : * been added to the histogram and maintain a vector with `b-a+1` values.
111 : : * The vector is resized on demand to grow as necessary and supports negative
112 : : * values as well.
113 : : * Note that the template type needs to have a streaming operator to convert it
114 : : * to a string in `getViewer`.
115 : : */
116 : : template <typename Integral>
117 : : struct StatisticHistogramValue : StatisticBaseValue
118 : : {
119 : : static_assert(std::is_integral<Integral>::value
120 : : || std::is_enum<Integral>::value,
121 : : "Type should be a fundamental integral type.");
122 : :
123 : : /**
124 : : * Convert the internal representation to a `std::map<std::string, uint64_t>`
125 : : */
126 : 16478 : StatExportData getViewer() const override
127 : : {
128 : 32956 : std::map<std::string, uint64_t> res;
129 [ + + ]: 20713 : for (size_t i = 0, n = d_hist.size(); i < n; ++i)
130 : : {
131 [ + + ]: 4235 : if (d_hist[i] > 0)
132 : : {
133 : 2068 : std::stringstream ss;
134 : 2068 : ss << static_cast<Integral>(i + d_offset);
135 : 2068 : res.emplace(ss.str(), d_hist[i]);
136 : : }
137 : : }
138 : 32956 : return res;
139 : : }
140 : 17057 : bool isDefault() const override { return d_hist.size() == 0; }
141 : 2 : void printSafe(int fd) const override
142 : : {
143 : 2 : safe_print(fd, "{ ");
144 : 2 : bool first = true;
145 [ + + ]: 11 : for (size_t i = 0, n = d_hist.size(); i < n; ++i)
146 : : {
147 [ + + ]: 9 : if (d_hist[i] > 0)
148 : : {
149 [ + + ]: 3 : if (first)
150 : : {
151 : 2 : first = false;
152 : : }
153 : : else
154 : : {
155 : 1 : safe_print(fd, ", ");
156 : : }
157 : 3 : safe_print<Integral>(fd, static_cast<Integral>(i + d_offset));
158 : 3 : safe_print(fd, ": ");
159 : 3 : safe_print<uint64_t>(fd, d_hist[i]);
160 : : }
161 : : }
162 : 2 : safe_print(fd, " }");
163 : 2 : }
164 : :
165 : : /**
166 : : * Add `val` to the histogram. Casts `val` to `int64_t`, then resizes and
167 : : * moves the vector entries as necessary.
168 : : */
169 : 209682497 : void add(Integral val)
170 : : {
171 : 209682497 : int64_t v = static_cast<int64_t>(val);
172 [ + + ]: 209682497 : if (d_hist.empty())
173 : : {
174 : 233970 : d_offset = v;
175 : : }
176 [ + + ]: 209682497 : if (v < d_offset)
177 : : {
178 : 157699 : d_hist.insert(d_hist.begin(), d_offset - v, 0);
179 : 157699 : d_offset = v;
180 : : }
181 [ + + ]: 209682497 : if (static_cast<size_t>(v - d_offset) >= d_hist.size())
182 : : {
183 : 488449 : d_hist.resize(v - d_offset + 1);
184 : : }
185 : 209682497 : d_hist[v - d_offset]++;
186 : 209682497 : }
187 : : /** Get the value stored for key val */
188 : 0 : uint64_t getValue(Integral val)
189 : : {
190 : 0 : int64_t index = static_cast<int64_t>(val);
191 [ - - ]: 0 : if (index < d_offset)
192 : : {
193 : 0 : return 0;
194 : : }
195 : 0 : index = index - d_offset;
196 [ - - ]: 0 : return static_cast<size_t>(index) < d_hist.size() ? d_hist[index] : 0;
197 : : }
198 : :
199 : : /** Actual data */
200 : : std::vector<uint64_t> d_hist;
201 : : /** Offset of the entries. d_hist[i] corresponds to Integral(d_offset + i) */
202 : : int64_t d_offset;
203 : : };
204 : :
205 : : /**
206 : : * Holds the data for a `ReferenceStat`.
207 : : * When the `ReferenceStat` is destroyed the current value is copied into
208 : : * `d_committed`. Once `d_committed` is set, this value is returned, even if
209 : : * the reference is still valid.
210 : : */
211 : : template <typename T>
212 : : struct StatisticReferenceValue : StatisticBaseValue
213 : : {
214 : 3710 : StatExportData getViewer() const override
215 : : {
216 [ - + ]: 3710 : if (d_committed)
217 : : {
218 : : if constexpr (std::is_integral_v<T>)
219 : : {
220 : 0 : return static_cast<int64_t>(*d_committed);
221 : : }
222 : : else
223 : : {
224 : : // this else branch is required to ensure compilation.
225 : : // if T is unsigned int, this return statement triggers a compiler error
226 : 0 : return *d_committed;
227 : : }
228 : : }
229 [ + - ]: 3710 : else if (d_value != nullptr)
230 : : {
231 : : if constexpr (std::is_integral_v<T>)
232 : : {
233 : 3708 : return static_cast<int64_t>(*d_value);
234 : : }
235 : : else
236 : : {
237 : : // this else branch is required to ensure compilation.
238 : : // if T is unsigned int, this return statement triggers a compiler error
239 : 2 : return *d_value;
240 : : }
241 : : }
242 : : if constexpr (std::is_integral_v<T>)
243 : : {
244 : 0 : return static_cast<int64_t>(0);
245 : : }
246 : : else
247 : : {
248 : : // this else branch is required to ensure compilation.
249 : : // if T is unsigned int, this return statement triggers a compiler error
250 : 0 : return T();
251 : : }
252 : : }
253 : 3706 : bool isDefault() const override
254 : : {
255 [ - + ]: 3706 : if (d_committed)
256 : : {
257 : 0 : return *d_committed == T();
258 : : }
259 [ + - ][ + + ]: 3706 : return d_value == nullptr || *d_value == T();
[ - - ]
260 : : }
261 : 0 : void printSafe(int fd) const override
262 : : {
263 [ - - ]: 0 : if (d_committed)
264 : : {
265 : 0 : safe_print<T>(fd, *d_committed);
266 : : }
267 [ - - ]: 0 : else if (d_value != nullptr)
268 : : {
269 : 0 : safe_print<T>(fd, *d_value);
270 : : }
271 : : else
272 : : {
273 : 0 : safe_print<T>(fd, T());
274 : : }
275 : 0 : }
276 : 1152021 : void commit()
277 : : {
278 [ + + ]: 1152021 : if (d_value != nullptr)
279 : : {
280 : 686595 : d_committed = *d_value;
281 : : }
282 : 1152021 : }
283 : : const T& get() const { return d_committed ? *d_committed : *d_value; }
284 : :
285 : : const T* d_value = nullptr;
286 : : std::optional<T> d_committed;
287 : : };
288 : :
289 : : /**
290 : : * Holds the data for a `SizeStat`.
291 : : * When the `SizeStat` is destroyed the current size is copied into
292 : : * `d_committed`. Once `d_committed` is set, this value is returned, even if
293 : : * the reference is still valid.
294 : : */
295 : : template <typename T>
296 : : struct StatisticSizeValue : StatisticBaseValue
297 : : {
298 : 285 : StatExportData getViewer() const override
299 : : {
300 [ - + ]: 285 : if (d_committed)
301 : : {
302 : 0 : return static_cast<int64_t>(*d_committed);
303 : : }
304 [ + - ]: 285 : else if (d_value != nullptr)
305 : : {
306 : 285 : return static_cast<int64_t>(d_value->size());
307 : : }
308 : 0 : return static_cast<int64_t>(0);
309 : : }
310 : 285 : bool isDefault() const override
311 : : {
312 [ - + ]: 285 : if (d_committed)
313 : : {
314 : 0 : return *d_committed == 0;
315 : : }
316 [ + - ][ + + ]: 285 : return d_value == nullptr || d_value->size() == 0;
317 : : }
318 : 0 : void printSafe(int fd) const override
319 : : {
320 [ - - ]: 0 : if (d_committed)
321 : : {
322 : 0 : safe_print(fd, *d_committed);
323 : : }
324 [ - - ]: 0 : else if (d_value != nullptr)
325 : : {
326 : 0 : safe_print(fd, d_value->size());
327 : : }
328 : : else
329 : : {
330 : 0 : safe_print(fd, 0);
331 : : }
332 : 0 : }
333 : 51132 : void commit()
334 : : {
335 [ + - ]: 51132 : if (d_value != nullptr)
336 : : {
337 : 51132 : d_committed = d_value->size();
338 : : }
339 : 51132 : }
340 : : size_t get() const { return d_committed ? *d_committed : d_value->size(); }
341 : :
342 : : const T* d_value = nullptr;
343 : : std::optional<std::size_t> d_committed;
344 : : };
345 : :
346 : : /**
347 : : * Holds the data for a `TimerStat`.
348 : : * Uses `std::chrono` to obtain the current time, store a time point and sum up
349 : : * the total durations.
350 : : */
351 : : struct StatisticTimerValue : StatisticBaseValue
352 : : {
353 : : using clock = std::chrono::steady_clock;
354 : : using time_point = clock::time_point;
355 : : struct duration : public std::chrono::nanoseconds
356 : : {
357 : : };
358 : : /** Returns the number of milliseconds */
359 : : StatExportData getViewer() const override;
360 : : bool isDefault() const override;
361 : : /** Prints seconds in fixed-point format */
362 : : void printSafe(int fd) const override;
363 : : /**
364 : : * Returns the elapsed time in milliseconds.
365 : : * Make sure that we include the time of a currently running timer
366 : : */
367 : : uint64_t get() const;
368 : :
369 : : /**
370 : : * The cumulative duration of the timer so far.
371 : : * Does not include a currently running timer, but `get()` takes care of this.
372 : : */
373 : : duration d_duration;
374 : : /**
375 : : * The start time of a currently running timer.
376 : : * May not be reset when the timer is stopped.
377 : : */
378 : : time_point d_start;
379 : : /** Whether a timer is running right now. */
380 : : bool d_running;
381 : : };
382 : :
383 : : } // namespace cvc5::internal
384 : :
385 : : #endif
|
