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.

diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index f706f3321feb60fed9589908375fd3df46794489..d2f7244f97a703c87c12dd4b6ee1fab537b2f849 100644 (file)
--- 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                                                      */
 /****************************************************************************/

diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h
index 02f6dc2020d3a0cd27a7b76efc4169ed55dcca2b..370b1d65d7fdf432427fe2101095517fd6f89760 100644 (file)
--- a/test/unit/util/stats_black.h
+++ b/test/unit/util/stats_black.h
@@ -21,6 +21,7 @@
 #include <string>
 
 #include "lib/clock_gettime.h"
+#include "expr/proof_rule.h"
 #include "util/statistics_registry.h"
 
 using namespace CVC4;
@@ -75,6 +76,10 @@ public:
     histStat << 10;
     histStat << 10;
     histStat << 0;
+    IntegralHistogramStat<std::int64_t> histIntStat("hist-int");
+    histIntStat << 15 << 16 << 15 << 14 << 16;
+    IntegralHistogramStat<CVC4::PfRule> histPfRuleStat("hist-pfrule");
+    histPfRuleStat << PfRule::ASSUME << PfRule::SCOPE << PfRule::ASSUME;
 
     // A statistic with no safe_print support
     BackedStat<string*> backedUnsupported("backedUnsupported", &bar);
@@ -87,6 +92,8 @@ public:
     TS_ASSERT_EQUALS(backedStr.getName(), "backed");
     TS_ASSERT_EQUALS(sInt.getName(), "my int");
     TS_ASSERT_EQUALS(sTimer.getName(), "a timer ! for measuring time");
+    TS_ASSERT_EQUALS(histIntStat.getName(), "hist-int");
+    TS_ASSERT_EQUALS(histPfRuleStat.getName(), "hist-pfrule");
 
     TS_ASSERT_EQUALS(refStr.getData(), empty);
     TS_ASSERT_EQUALS(refStr2.getData(), bar);
@@ -148,6 +155,10 @@ public:
     safe_print(fd, "\n");
     histStat.safeFlushInformation(fd);
     safe_print(fd, "\n");
+    histIntStat.safeFlushInformation(fd);
+    safe_print(fd, "\n");
+    histPfRuleStat.safeFlushInformation(fd);
+    safe_print(fd, "\n");
     backedUnsupported.safeFlushInformation(fd);
     off_t file_size = lseek(fd, 0, SEEK_CUR);
     close(fd);
@@ -171,6 +182,8 @@ public:
         "0xdeadbeef\n"
         "true\n"
         "[(0 : 1), (5 : 2), (6 : 1), (10 : 2)]\n"
+        "[(14 : 1), (15 : 2), (16 : 2)]\n"
+        "[(ASSUME : 2), (SCOPE : 1)]\n"
         "<unsupported>";
     TS_ASSERT(strncmp(expected, buf, file_size) == 0);
     delete[] buf;