GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/stats_base.h Lines: 40 46 87.0 %
Date: 2021-03-22 Branches: 39 106 36.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file stats_base.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Base statistic classes
13
 **
14
 ** Base statistic classes
15
 **/
16
17
#include "cvc4_private_library.h"
18
19
#ifndef CVC4__UTIL__STATS_BASE_H
20
#define CVC4__UTIL__STATS_BASE_H
21
22
#include <iomanip>
23
#include <sstream>
24
#include <string>
25
26
#include "cvc4_export.h"
27
#include "util/safe_print.h"
28
#include "util/sexpr.h"
29
#include "util/stats_utils.h"
30
31
#ifdef CVC4_STATISTICS_ON
32
#define CVC4_USE_STATISTICS true
33
#else
34
#define CVC4_USE_STATISTICS false
35
#endif
36
37
namespace CVC4 {
38
39
/**
40
 * The base class for all statistics.
41
 *
42
 * This base class keeps the name of the statistic and declares the (pure)
43
 * virtual functions flushInformation() and safeFlushInformation().
44
 * Derived classes must implement these function and pass their name to
45
 * the base class constructor.
46
 */
47
class CVC4_EXPORT Stat
48
{
49
 public:
50
  /**
51
   * Construct a statistic with the given name.  Debug builds of CVC4
52
   * will throw an assertion exception if the given name contains the
53
   * statistic delimiter string.
54
   */
55
  Stat(const std::string& name);
56
57
  /** Destruct a statistic.  This base-class version does nothing. */
58
4795456
  virtual ~Stat() = default;
59
60
  /**
61
   * Flush the value of this statistic to an output stream.  Should
62
   * finish the output with an end-of-line character.
63
   */
64
  virtual void flushInformation(std::ostream& out) const = 0;
65
66
  /**
67
   * Flush the value of this statistic to a file descriptor. Should finish the
68
   * output with an end-of-line character. Should be safe to use in a signal
69
   * handler.
70
   */
71
  virtual void safeFlushInformation(int fd) const = 0;
72
73
  /** Get the name of this statistic. */
74
316227544
  const std::string& getName() const { return d_name; }
75
76
  /** Get the value of this statistic as a string. */
77
8
  virtual SExpr getValue() const
78
  {
79
16
    std::stringstream ss;
80
8
    flushInformation(ss);
81
16
    return SExpr(ss.str());
82
  }
83
84
 protected:
85
  /** The name of this statistic */
86
  std::string d_name;
87
}; /* class Stat */
88
89
/**
90
 * A data statistic that keeps a T and sets it with setData().
91
 *
92
 * Template class T must have an operator=() and a copy constructor.
93
 */
94
template <class T>
95
4153046
class BackedStat : public Stat
96
{
97
 public:
98
  /** Construct a backed statistic with the given name and initial value. */
99
4157462
  BackedStat(const std::string& name, const T& init) : Stat(name), d_data(init)
100
  {
101
4157462
  }
102
103
  /** Set the underlying data value to the given value. */
104
1853928
  void set(const T& t)
105
  {
106
    if (CVC4_USE_STATISTICS)
107
    {
108
1853928
      d_data = t;
109
    }
110
1853928
  }
111
112
66672
  const T& get() const { return d_data; }
113
114
  /** Flush the value of the statistic to the given output stream. */
115
4
  virtual void flushInformation(std::ostream& out) const override
116
  {
117
4
    out << d_data;
118
4
  }
119
120
16
  virtual void safeFlushInformation(int fd) const override
121
  {
122
16
    safe_print<T>(fd, d_data);
123
16
  }
124
125
 protected:
126
  /** The internally-kept statistic value */
127
  T d_data;
128
}; /* class BackedStat<T> */
129
130
/**
131
 * A data statistic that references a data cell of type T,
132
 * implementing get() by referencing that memory cell, and
133
 * setData() by reassigning the statistic to point to the new
134
 * data cell.  The referenced data cell is kept as a const
135
 * reference, meaning the referenced data is never actually
136
 * modified by this class (it must be externally modified for
137
 * a reference statistic to make sense).  A common use for
138
 * this type of statistic is to output a statistic that is kept
139
 * outside the statistics package (for example, one that's kept
140
 * by a theory implementation for internal heuristic purposes,
141
 * which is important to keep even if statistics are turned off).
142
 *
143
 * Template class T must have an assignment operator=().
144
 */
145
template <class T>
146
218408
class ReferenceStat : public Stat
147
{
148
 public:
149
  /**
150
   * Construct a reference stat with the given name and a reference
151
   * to nullptr.
152
   */
153
180613
  ReferenceStat(const std::string& name) : Stat(name) {}
154
155
  /**
156
   * Construct a reference stat with the given name and a reference to
157
   * the given data.
158
   */
159
37882
  ReferenceStat(const std::string& name, const T& data) : Stat(name)
160
  {
161
37882
    set(data);
162
37882
  }
163
164
  /** Set this reference statistic to refer to the given data cell. */
165
218495
  void set(const T& t)
166
  {
167
    if (CVC4_USE_STATISTICS)
168
    {
169
218495
      d_data = &t;
170
    }
171
218495
  }
172
8
  const T& get() const { return *d_data; }
173
174
  /** Flush the value of the statistic to the given output stream. */
175
6
  virtual void flushInformation(std::ostream& out) const override
176
  {
177
6
    out << *d_data;
178
6
  }
179
180
4
  virtual void safeFlushInformation(int fd) const override
181
  {
182
4
    safe_print<T>(fd, *d_data);
183
4
  }
184
185
 private:
186
  /** The referenced data cell */
187
  const T* d_data = nullptr;
188
}; /* class ReferenceStat<T> */
189
190
/**
191
 * A backed integer-valued (64-bit signed) statistic.
192
 * This doesn't functionally differ from its base class BackedStat<int64_t>,
193
 * except for adding convenience functions for dealing with integers.
194
 */
195
117897153
class IntStat : public BackedStat<int64_t>
196
{
197
 public:
198
  /**
199
   * Construct an integer-valued statistic with the given name and
200
   * initial value.
201
   */
202
  IntStat(const std::string& name, int64_t init);
203
204
  /** Increment the underlying integer statistic. */
205
  IntStat& operator++();
206
  /** Increment the underlying integer statistic. */
207
  IntStat& operator++(int);
208
209
  /** Increment the underlying integer statistic by the given amount. */
210
  IntStat& operator+=(int64_t val);
211
212
  /** Keep the maximum of the current statistic value and the given one. */
213
  void maxAssign(int64_t val);
214
215
  /** Keep the minimum of the current statistic value and the given one. */
216
  void minAssign(int64_t val);
217
218
48
  SExpr getValue() const override { return SExpr(Integer(d_data)); }
219
220
}; /* class IntStat */
221
222
/**
223
 * The value for an AverageStat is the running average of (e1, e_2, ..., e_n),
224
 *   (e1 + e_2 + ... + e_n)/n,
225
 * where e_i is an entry added by an addEntry(e_i) call.
226
 * The value is initially always 0.
227
 * (This is to avoid making parsers confused.)
228
 *
229
 * A call to setData() will change the running average but not reset the
230
 * running count, so should generally be avoided.  Call addEntry() to add
231
 * an entry to the average calculation.
232
 */
233
31887578
class AverageStat : public BackedStat<double>
234
{
235
 public:
236
  /** Construct an average statistic with the given name. */
237
  AverageStat(const std::string& name);
238
239
  /** Add an entry to the running-average calculation. */
240
  AverageStat& operator<<(double e);
241
242
  SExpr getValue() const override;
243
244
 private:
245
  /**
246
   * The number of accumulations of the running average that we
247
   * have seen so far.
248
   */
249
  uint32_t d_count = 0;
250
  double d_sum = 0;
251
}; /* class AverageStat */
252
253
template <class T>
254
class SizeStat : public Stat
255
{
256
 public:
257
8995
  SizeStat(const std::string& name, const T& sized) : Stat(name), d_sized(sized)
258
  {
259
8995
  }
260
8992
  ~SizeStat() {}
261
262
  /** Flush the value of the statistic to the given output stream. */
263
  void flushInformation(std::ostream& out) const override
264
  {
265
    out << d_sized.size();
266
  }
267
268
  void safeFlushInformation(int fd) const override
269
  {
270
    safe_print(fd, d_sized.size());
271
  }
272
273
 private:
274
  const T& d_sized;
275
}; /* class SizeStat */
276
277
}  // namespace CVC4
278
279
#endif