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 |
|
* Basic statistics representation. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "util/statistics_stats.h" |
17 |
|
|
18 |
|
#include "base/check.h" |
19 |
|
#include "util/statistics_value.h" |
20 |
|
|
21 |
|
namespace cvc5 { |
22 |
|
|
23 |
1794835 |
AverageStat& AverageStat::operator<<(double v) |
24 |
|
{ |
25 |
|
if constexpr (Configuration::isStatisticsBuild()) |
26 |
|
{ |
27 |
1794835 |
d_data->d_sum += v; |
28 |
1794835 |
d_data->d_count++; |
29 |
|
} |
30 |
1794835 |
return *this; |
31 |
|
} |
32 |
|
|
33 |
15239 |
IntStat& IntStat::operator=(int64_t val) |
34 |
|
{ |
35 |
|
if constexpr (Configuration::isStatisticsBuild()) |
36 |
|
{ |
37 |
15239 |
d_data->d_value = val; |
38 |
|
} |
39 |
15239 |
return *this; |
40 |
|
} |
41 |
|
|
42 |
169677251 |
IntStat& IntStat::operator++() |
43 |
|
{ |
44 |
|
if constexpr (Configuration::isStatisticsBuild()) |
45 |
|
{ |
46 |
169677251 |
d_data->d_value++; |
47 |
|
} |
48 |
169677251 |
return *this; |
49 |
|
} |
50 |
|
|
51 |
2 |
IntStat& IntStat::operator++(int) |
52 |
|
{ |
53 |
|
if constexpr (Configuration::isStatisticsBuild()) |
54 |
|
{ |
55 |
2 |
d_data->d_value++; |
56 |
|
} |
57 |
2 |
return *this; |
58 |
|
} |
59 |
|
|
60 |
5004 |
IntStat& IntStat::operator+=(int64_t val) |
61 |
|
{ |
62 |
|
if constexpr (Configuration::isStatisticsBuild()) |
63 |
|
{ |
64 |
5004 |
d_data->d_value += val; |
65 |
|
} |
66 |
5004 |
return *this; |
67 |
|
} |
68 |
|
|
69 |
3402881 |
void IntStat::maxAssign(int64_t val) |
70 |
|
{ |
71 |
|
if constexpr (Configuration::isStatisticsBuild()) |
72 |
|
{ |
73 |
3402881 |
if (d_data->d_value < val) |
74 |
|
{ |
75 |
256946 |
d_data->d_value = val; |
76 |
|
} |
77 |
|
} |
78 |
3402881 |
} |
79 |
|
|
80 |
5633 |
void IntStat::minAssign(int64_t val) |
81 |
|
{ |
82 |
|
if constexpr (Configuration::isStatisticsBuild()) |
83 |
|
{ |
84 |
5633 |
if (d_data->d_value > val) |
85 |
|
{ |
86 |
1667 |
d_data->d_value = val; |
87 |
|
} |
88 |
|
} |
89 |
5633 |
} |
90 |
|
|
91 |
16066396 |
void TimerStat::start() |
92 |
|
{ |
93 |
|
if constexpr (Configuration::isStatisticsBuild()) |
94 |
|
{ |
95 |
16066396 |
Assert(!d_data->d_running) << "timer is already running"; |
96 |
16066396 |
d_data->d_start = StatisticTimerValue::clock::now(); |
97 |
16066396 |
d_data->d_running = true; |
98 |
|
} |
99 |
16066396 |
} |
100 |
16053214 |
void TimerStat::stop() |
101 |
|
{ |
102 |
|
if constexpr (Configuration::isStatisticsBuild()) |
103 |
|
{ |
104 |
16053214 |
Assert(d_data->d_running) << "timer is not running"; |
105 |
16053214 |
d_data->d_duration += StatisticTimerValue::clock::now() - d_data->d_start; |
106 |
16053214 |
d_data->d_running = false; |
107 |
|
} |
108 |
16053214 |
} |
109 |
3978867 |
bool TimerStat::running() const |
110 |
|
{ |
111 |
|
if constexpr (Configuration::isStatisticsBuild()) |
112 |
|
{ |
113 |
3978867 |
return d_data->d_running; |
114 |
|
} |
115 |
|
return false; |
116 |
|
} |
117 |
|
|
118 |
16083279 |
CodeTimer::CodeTimer(TimerStat& timer, bool allow_reentrant) |
119 |
16083279 |
: d_timer(timer), d_reentrant(false) |
120 |
|
{ |
121 |
|
if constexpr (Configuration::isStatisticsBuild()) |
122 |
|
{ |
123 |
16083279 |
if (!allow_reentrant || !(d_reentrant = d_timer.running())) |
124 |
|
{ |
125 |
16053214 |
d_timer.start(); |
126 |
|
} |
127 |
|
} |
128 |
16083279 |
} |
129 |
32166558 |
CodeTimer::~CodeTimer() |
130 |
|
{ |
131 |
|
if constexpr (Configuration::isStatisticsBuild()) |
132 |
|
{ |
133 |
16083279 |
if (!d_reentrant) |
134 |
|
{ |
135 |
16053214 |
d_timer.stop(); |
136 |
|
} |
137 |
|
} |
138 |
16083279 |
} |
139 |
|
|
140 |
|
} // namespace cvc5 |