Add new IntegralHistogramStat (#5898)

This PR adds a new statistics class that improves on HistogramStat if we know that the type is integral (also supporting enums).
Instead of using a comparably slow std::map like HistogramStat, IntegralHistogramStat uses a std::vector that is resized appropriately.
The integral values are simply cast to std::int64_t and used as indices into the vector.

1 files changed, 104 insertions, 0 deletions

diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index f706f3321..d2f7244f9 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -639,6 +639,110 @@ public:
 
 };/* class HistogramStat */
 
+/**
+ * A histogram statistic class for integral types.
+ * Avoids using an std::map (like the generic HistogramStat) in favor of a
+ * faster std::vector by casting the integral values to indices into the
+ * vector. Requires the type to be an integral type that is convertible to
+ * std::int64_t, also supporting appropriate enum types.
+ * The vector is resized on demand to grow as necessary and supports negative
+ * values as well.
+ */
+template <typename Integral>
+class IntegralHistogramStat : public Stat
+{
+  static_assert(std::is_integral<Integral>::value
+                    || std::is_enum<Integral>::value,
+                "Type should be a fundamental integral type.");
+
+ private:
+  std::vector<std::uint64_t> d_hist;
+  std::int64_t d_offset;
+
+ public:
+  /** Construct a histogram of a stream of entries. */
+  IntegralHistogramStat(const std::string& name) : Stat(name) {}
+  ~IntegralHistogramStat() {}
+
+  void flushInformation(std::ostream& out) const override
+  {
+    if (CVC4_USE_STATISTICS)
+    {
+      out << "[";
+      bool first = true;
+      for (std::size_t i = 0, n = d_hist.size(); i < n; ++i)
+      {
+        if (d_hist[i] > 0)
+        {
+          if (first)
+          {
+            first = false;
+          }
+          else
+          {
+            out << ", ";
+          }
+          out << "(" << static_cast<Integral>(i + d_offset) << " : "
+              << d_hist[i] << ")";
+        }
+      }
+      out << "]";
+    }
+  }
+
+  void safeFlushInformation(int fd) const override
+  {
+    if (CVC4_USE_STATISTICS)
+    {
+      safe_print(fd, "[");
+      bool first = true;
+      for (std::size_t i = 0, n = d_hist.size(); i < n; ++i)
+      {
+        if (d_hist[i] > 0)
+        {
+          if (first)
+          {
+            first = false;
+          }
+          else
+          {
+            safe_print(fd, ", ");
+          }
+          safe_print(fd, "(");
+          safe_print<Integral>(fd, static_cast<Integral>(i + d_offset));
+          safe_print(fd, " : ");
+          safe_print<std::uint64_t>(fd, d_hist[i]);
+          safe_print(fd, ")");
+        }
+      }
+      safe_print(fd, "]");
+    }
+  }
+
+  IntegralHistogramStat& operator<<(Integral val)
+  {
+    if (CVC4_USE_STATISTICS)
+    {
+      std::int64_t v = static_cast<std::int64_t>(val);
+      if (d_hist.empty())
+      {
+        d_offset = v;
+      }
+      if (v < d_offset)
+      {
+        d_hist.insert(d_hist.begin(), d_offset - v, 0);
+        d_offset = v;
+      }
+      if (static_cast<std::size_t>(v - d_offset) >= d_hist.size())
+      {
+        d_hist.resize(v - d_offset + 1);
+      }
+      d_hist[v - d_offset]++;
+    }
+    return (*this);
+  }
+}; /* class IntegralHistogramStat */
+
 /****************************************************************************/
 /* Statistics Registry                                                      */
 /****************************************************************************/