GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/stats_histogram.h Lines: 39 40 97.5 %
Date: 2021-03-23 Branches: 31 58 53.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file stats_histogram.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 Histogram statistics
13
 **
14
 ** Stat classes that represent histograms
15
 **/
16
17
#include "cvc4_private_library.h"
18
19
#ifndef CVC4__UTIL__STATS_HISTOGRAM_H
20
#define CVC4__UTIL__STATS_HISTOGRAM_H
21
22
#include <map>
23
#include <vector>
24
25
#include "util/stats_base.h"
26
27
namespace CVC4 {
28
29
/**
30
 * A histogram statistic class for integral types.
31
 * Avoids using an std::map (like we would do for generic types) in favor of a
32
 * faster std::vector by casting the integral values to indices into the
33
 * vector. Requires the type to be an integral type that is convertible to
34
 * int64_t, also supporting appropriate enum types.
35
 * The vector is resized on demand to grow as necessary and supports negative
36
 * values as well.
37
 */
38
template <typename Integral>
39
414272
class IntegralHistogramStat : public Stat
40
{
41
  static_assert(std::is_integral<Integral>::value
42
                    || std::is_enum<Integral>::value,
43
                "Type should be a fundamental integral type.");
44
45
 public:
46
  /** Construct a histogram of a stream of entries. */
47
414464
  IntegralHistogramStat(const std::string& name) : Stat(name) {}
48
49
6
  void flushInformation(std::ostream& out) const override
50
  {
51
6
    out << "[";
52
6
    bool first = true;
53
8
    for (size_t i = 0, n = d_hist.size(); i < n; ++i)
54
    {
55
2
      if (d_hist[i] > 0)
56
      {
57
2
        if (first)
58
        {
59
2
          first = false;
60
        }
61
        else
62
        {
63
          out << ", ";
64
        }
65
4
        out << "(" << static_cast<Integral>(i + d_offset) << " : "
66
2
            << d_hist[i] << ")";
67
      }
68
    }
69
6
    out << "]";
70
6
  }
71
72
4
  void safeFlushInformation(int fd) const override
73
  {
74
4
    safe_print(fd, "[");
75
4
    bool first = true;
76
14
    for (size_t i = 0, n = d_hist.size(); i < n; ++i)
77
    {
78
10
      if (d_hist[i] > 0)
79
      {
80
10
        if (first)
81
        {
82
4
          first = false;
83
        }
84
        else
85
        {
86
6
          safe_print(fd, ", ");
87
        }
88
10
        safe_print(fd, "(");
89
10
        safe_print<Integral>(fd, static_cast<Integral>(i + d_offset));
90
10
        safe_print(fd, " : ");
91
10
        safe_print<uint64_t>(fd, d_hist[i]);
92
10
        safe_print(fd, ")");
93
      }
94
    }
95
4
    safe_print(fd, "]");
96
4
  }
97
98
11072722
  IntegralHistogramStat& operator<<(Integral val)
99
  {
100
    if (CVC4_USE_STATISTICS)
101
    {
102
11072722
      int64_t v = static_cast<int64_t>(val);
103
11072722
      if (d_hist.empty())
104
      {
105
29751
        d_offset = v;
106
      }
107
11072722
      if (v < d_offset)
108
      {
109
24279
        d_hist.insert(d_hist.begin(), d_offset - v, 0);
110
24279
        d_offset = v;
111
      }
112
11072722
      if (static_cast<size_t>(v - d_offset) >= d_hist.size())
113
      {
114
49009
        d_hist.resize(v - d_offset + 1);
115
      }
116
11072722
      d_hist[v - d_offset]++;
117
    }
118
11072722
    return (*this);
119
  }
120
121
 private:
122
  std::vector<uint64_t> d_hist;
123
  int64_t d_offset;
124
}; /* class IntegralHistogramStat */
125
126
}  // namespace CVC4
127
128
#endif