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 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 "util/statistics_value.h" |
27 |
|
|
28 |
|
#include "util/ostream_util.h" |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
|
32 |
|
// standard helper, see https://en.cppreference.com/w/cpp/utility/variant/visit |
33 |
|
template <class... Ts> |
34 |
|
struct overloaded : Ts... |
35 |
|
{ |
36 |
|
using Ts::operator()...; |
37 |
|
}; |
38 |
|
template <class... Ts> |
39 |
|
overloaded(Ts...) -> overloaded<Ts...>; |
40 |
|
|
41 |
|
namespace detail { |
42 |
80 |
std::ostream& print(std::ostream& out, const StatExportData& sed) |
43 |
|
{ |
44 |
80 |
std::visit(overloaded{ |
45 |
8 |
[&out](int64_t v) { out << v; }, |
46 |
|
[&out](uint64_t v) { out << v; }, |
47 |
9 |
[&out](double v) { out << v; }, |
48 |
15 |
[&out](const std::string& v) { out << v; }, |
49 |
113 |
[&out](const std::map<std::string, uint64_t>& v) { |
50 |
48 |
out << "{ "; |
51 |
48 |
bool first = true; |
52 |
59 |
for (const auto& e : v) |
53 |
|
{ |
54 |
11 |
if (!first) |
55 |
6 |
out << ", "; |
56 |
|
else |
57 |
5 |
first = false; |
58 |
11 |
out << e.first << ": " << e.second; |
59 |
|
} |
60 |
48 |
out << " }"; |
61 |
48 |
}, |
62 |
|
}, |
63 |
|
sed); |
64 |
80 |
return out; |
65 |
|
} |
66 |
|
} |
67 |
|
|
68 |
4963924 |
StatisticBaseValue::~StatisticBaseValue() {} |
69 |
|
|
70 |
80 |
std::ostream& operator<<(std::ostream& out, const StatisticBaseValue& sbv) |
71 |
|
{ |
72 |
80 |
return detail::print(out, sbv.getViewer()); |
73 |
|
} |
74 |
|
|
75 |
2 |
StatExportData StatisticAverageValue::getViewer() const { return get(); } |
76 |
|
|
77 |
|
bool StatisticAverageValue::isDefault() const { return d_count == 0; } |
78 |
|
|
79 |
|
void StatisticAverageValue::printSafe(int fd) const |
80 |
|
{ |
81 |
|
safe_print<double>(fd, get()); |
82 |
|
} |
83 |
|
|
84 |
2 |
double StatisticAverageValue::get() const { return d_sum / d_count; } |
85 |
|
|
86 |
7 |
StatExportData StatisticTimerValue::getViewer() const |
87 |
|
{ |
88 |
7 |
return std::to_string(get()) + "ms"; |
89 |
|
} |
90 |
|
|
91 |
|
bool StatisticTimerValue::isDefault() const |
92 |
|
{ |
93 |
|
return !d_running && d_duration.count() == 0; |
94 |
|
} |
95 |
|
|
96 |
|
void StatisticTimerValue::printSafe(int fd) const |
97 |
|
{ |
98 |
|
safe_print<uint64_t>(fd, get()); |
99 |
|
safe_print<std::string>(fd, "ms"); |
100 |
|
} |
101 |
|
|
102 |
|
/** Make sure that we include the time of a currently running timer */ |
103 |
7 |
uint64_t StatisticTimerValue::get() const |
104 |
|
{ |
105 |
7 |
auto data = d_duration; |
106 |
7 |
if (d_running) |
107 |
|
{ |
108 |
|
data += clock::now() - d_start; |
109 |
|
} |
110 |
7 |
return static_cast<int64_t>(data / std::chrono::milliseconds(1)); |
111 |
|
} |
112 |
|
|
113 |
|
} // namespace cvc5 |