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