Replace HistogramStat by IntegralHistogramStat (#6126)

This PR uses IntegralHistogramStat instead of HistogramStat when appropriate, that is everywhere.

16 files changed, 29 insertions, 96 deletions

diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index 21ffd63b8..a84f17c28 100644
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -93,7 +93,7 @@ class ProofCheckerStatistics
   ProofCheckerStatistics();
   ~ProofCheckerStatistics();
   /** Counts the number of checks for each kind of proof rule */
-  HistogramStat<PfRule> d_ruleChecks;
+  IntegralHistogramStat<PfRule> d_ruleChecks;
   /** Total number of rule checks */
   IntStat d_totalRuleChecks;
 };
diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h
index 856e3be58..90c240478 100644
--- a/src/preprocessing/util/ite_utilities.h
+++ b/src/preprocessing/util/ite_utilities.h
@@ -306,7 +306,7 @@ class ITESimplifier
     IntStat d_specialEqualityFolds;
     IntStat d_simpITEVisits;
 
-    HistogramStat<uint32_t> d_inSmaller;
+    IntegralHistogramStat<uint32_t> d_inSmaller;
 
     Statistics();
     ~Statistics();
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 0882ee2b6..d16f8259e 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -286,10 +286,10 @@ class TSatProof {
     IntStat d_numLearnedInProof;
     IntStat d_numLemmasInProof;
     AverageStat d_avgChainLength;
-    HistogramStat<uint64_t> d_resChainLengths;
-    HistogramStat<uint64_t> d_usedResChainLengths;
-    HistogramStat<uint64_t> d_clauseGlue;
-    HistogramStat<uint64_t> d_usedClauseGlue;
+    IntegralHistogramStat<uint64_t> d_resChainLengths;
+    IntegralHistogramStat<uint64_t> d_usedResChainLengths;
+    IntegralHistogramStat<uint64_t> d_clauseGlue;
+    IntegralHistogramStat<uint64_t> d_usedClauseGlue;
     Statistics(const std::string& name);
     ~Statistics();
   };
diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index e045dd2ed..78c367881 100644
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -250,7 +250,7 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
 
  private:
   /** Counts number of postprocessed proof nodes for each kind of proof rule */
-  HistogramStat<PfRule> d_ruleCount;
+  IntegralHistogramStat<PfRule> d_ruleCount;
   /** Total number of postprocessed rule applications */
   IntStat d_totalRuleCount;
   /** The minimum pedantic level of any rule encountered */
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 5cbf95760..4f261bc00 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -855,9 +855,9 @@ private:
     IntStat d_cutsRejectedDuringReplay;
     IntStat d_cutsRejectedDuringLemmas;
 
-    HistogramStat<uint32_t> d_satPivots;
-    HistogramStat<uint32_t> d_unsatPivots;
-    HistogramStat<uint32_t> d_unknownPivots;
+    IntegralHistogramStat<uint32_t> d_satPivots;
+    IntegralHistogramStat<uint32_t> d_unsatPivots;
+    IntegralHistogramStat<uint32_t> d_unknownPivots;
 
 
     IntStat d_solveIntModelsAttempts;
diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp
index 314a0498d..54b279e66 100644
--- a/src/theory/bags/bags_rewriter.cpp
+++ b/src/theory/bags/bags_rewriter.cpp
@@ -37,7 +37,7 @@ BagsRewriteResponse::BagsRewriteResponse(const BagsRewriteResponse& r)
 {
 }
 
-BagsRewriter::BagsRewriter(HistogramStat<Rewrite>* statistics)
+BagsRewriter::BagsRewriter(IntegralHistogramStat<Rewrite>* statistics)
     : d_statistics(statistics)
 {
   d_nm = NodeManager::currentNM();
diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index 309b06009..6c440c512 100644
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -42,7 +42,7 @@ struct BagsRewriteResponse
 class BagsRewriter : public TheoryRewriter
 {
  public:
-  BagsRewriter(HistogramStat<Rewrite>* statistics = nullptr);
+  BagsRewriter(IntegralHistogramStat<Rewrite>* statistics = nullptr);
 
   /**
    * postRewrite nodes with kinds: MK_BAG, BAG_COUNT, UNION_MAX, UNION_DISJOINT,
@@ -218,7 +218,7 @@ class BagsRewriter : public TheoryRewriter
   Node d_zero;
   Node d_one;
   /** Reference to the rewriter statistics. */
-  HistogramStat<Rewrite>* d_statistics;
+  IntegralHistogramStat<Rewrite>* d_statistics;
 }; /* class TheoryBagsRewriter */
 
 }  // namespace bags
diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h
index c6b6c7e7a..c8f7ed420 100644
--- a/src/theory/bags/bags_statistics.h
+++ b/src/theory/bags/bags_statistics.h
@@ -35,7 +35,7 @@ class BagsStatistics
   ~BagsStatistics();
 
   /** Counts the number of applications of each type of rewrite rule */
-  HistogramStat<Rewrite> d_rewrites;
+  IntegralHistogramStat<Rewrite> d_rewrites;
 };
 
 }  // namespace bags
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index b19e98bbd..869c40ad8 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -33,7 +33,7 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-SequencesRewriter::SequencesRewriter(HistogramStat<Rewrite>* statistics)
+SequencesRewriter::SequencesRewriter(IntegralHistogramStat<Rewrite>* statistics)
     : d_statistics(statistics), d_stringsEntail(*this)
 {
 }
diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h
index 6f7338a43..9f5b002af 100644
--- a/src/theory/strings/sequences_rewriter.h
+++ b/src/theory/strings/sequences_rewriter.h
@@ -33,7 +33,7 @@ namespace strings {
 class SequencesRewriter : public TheoryRewriter
 {
  public:
-  SequencesRewriter(HistogramStat<Rewrite>* statistics);
+  SequencesRewriter(IntegralHistogramStat<Rewrite>* statistics);
 
  protected:
   /** rewrite regular expression concatenation
@@ -288,7 +288,7 @@ class SequencesRewriter : public TheoryRewriter
   static Node canonicalStrForSymbolicLength(Node n, TypeNode stype);
 
   /** Reference to the rewriter statistics. */
-  HistogramStat<Rewrite>* d_statistics;
+  IntegralHistogramStat<Rewrite>* d_statistics;
 
   /** Instance of the entailment checker for strings. */
   StringsEntail d_stringsEntail;
diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h
index e4d122faf..01075eb26 100644
--- a/src/theory/strings/sequences_stats.h
+++ b/src/theory/strings/sequences_stats.h
@@ -67,29 +67,29 @@ class SequencesStatistics
    * TheoryInferenceManager, i.e.
    * (theory::strings::inferences{Facts,Lemmas,Conflicts}).
    */
-  HistogramStat<InferenceId> d_inferencesNoPf;
+  IntegralHistogramStat<InferenceId> d_inferencesNoPf;
   /**
    * Counts the number of applications of each type of context-dependent
    * simplification. The sum of this map is equal to the number of EXTF or
    * EXTF_N inferences.
    */
-  HistogramStat<Kind> d_cdSimplifications;
+  IntegralHistogramStat<Kind> d_cdSimplifications;
   /**
    * Counts the number of applications of each type of reduction. The sum of
    * this map is equal to the number of REDUCTION inferences (when
    * options::stringLazyPreproc is true).
    */
-  HistogramStat<Kind> d_reductions;
+  IntegralHistogramStat<Kind> d_reductions;
   /**
    * Counts the number of applications of each type of regular expression
    * positive (resp. negative) unfoldings. The sum of this map is equal to the
    * number of RE_UNFOLD_POS (resp. RE_UNFOLD_NEG) inferences.
    */
-  HistogramStat<Kind> d_regexpUnfoldingsPos;
-  HistogramStat<Kind> d_regexpUnfoldingsNeg;
+  IntegralHistogramStat<Kind> d_regexpUnfoldingsPos;
+  IntegralHistogramStat<Kind> d_regexpUnfoldingsNeg;
   //--------------- end of inferences
   /** Counts the number of applications of each type of rewrite rule */
-  HistogramStat<Rewrite> d_rewrites;
+  IntegralHistogramStat<Rewrite> d_rewrites;
   //--------------- conflicts, partition of calls to OutputChannel::conflict
   /** Number of equality engine conflicts */
   IntStat d_conflictsEqEngine;
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp
index 8e5416629..33e7cd895 100644
--- a/src/theory/strings/strings_rewriter.cpp
+++ b/src/theory/strings/strings_rewriter.cpp
@@ -25,7 +25,7 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-StringsRewriter::StringsRewriter(HistogramStat<Rewrite>* statistics)
+StringsRewriter::StringsRewriter(IntegralHistogramStat<Rewrite>* statistics)
     : SequencesRewriter(statistics)
 {
 }
diff --git a/src/theory/strings/strings_rewriter.h b/src/theory/strings/strings_rewriter.h
index 18e3ce129..1398d4703 100644
--- a/src/theory/strings/strings_rewriter.h
+++ b/src/theory/strings/strings_rewriter.h
@@ -32,7 +32,7 @@ namespace strings {
 class StringsRewriter : public SequencesRewriter
 {
  public:
-  StringsRewriter(HistogramStat<Rewrite>* statistics);
+  StringsRewriter(IntegralHistogramStat<Rewrite>* statistics);
 
   RewriteResponse postRewrite(TNode node) override;
 
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 5aed07fc3..d6fa91f34 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -41,7 +41,7 @@ struct QInternalVarAttributeId
 typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
 
 StringsPreprocess::StringsPreprocess(SkolemCache* sc,
-                                     HistogramStat<Kind>* statReductions)
+                                     IntegralHistogramStat<Kind>* statReductions)
     : d_sc(sc), d_statReductions(statReductions)
 {
 }
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index fc615d171..a947c6da6 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -41,7 +41,7 @@ namespace strings {
 class StringsPreprocess {
  public:
   StringsPreprocess(SkolemCache* sc,
-                    HistogramStat<Kind>* statReductions = nullptr);
+                    IntegralHistogramStat<Kind>* statReductions = nullptr);
   ~StringsPreprocess();
   /** The reduce routine
    *
@@ -83,7 +83,7 @@ class StringsPreprocess {
   /** pointer to the skolem cache used by this class */
   SkolemCache* d_sc;
   /** Reference to the statistics for the theory of strings/sequences. */
-  HistogramStat<Kind>* d_statReductions;
+  IntegralHistogramStat<Kind>* d_statReductions;
   /** visited cache */
   std::map<Node, Node> d_visited;
   /**
diff --git a/src/util/stats_histogram.h b/src/util/stats_histogram.h
index 5528cf010..49306ba28 100644
--- a/src/util/stats_histogram.h
+++ b/src/util/stats_histogram.h
@@ -26,76 +26,9 @@
 
 namespace CVC4 {
 
-template <class T>
-class HistogramStat : public Stat
-{
-  using Histogram = std::map<T, uint64_t>;
- public:
-  /** Construct a histogram of a stream of entries. */
-  HistogramStat(const std::string& name) : Stat(name) {}
-
-  void flushInformation(std::ostream& out) const override
-  {
-    auto i = d_hist.begin();
-    auto end = d_hist.end();
-    out << "[";
-    while (i != end)
-    {
-      const T& key = (*i).first;
-      uint64_t count = (*i).second;
-      out << "(" << key << " : " << count << ")";
-      ++i;
-      if (i != end)
-      {
-        out << ", ";
-      }
-    }
-    out << "]";
-  }
-
-  void safeFlushInformation(int fd) const override
-  {
-    auto i = d_hist.begin();
-    auto end = d_hist.end();
-    safe_print(fd, "[");
-    while (i != end)
-    {
-      const T& key = (*i).first;
-      uint64_t count = (*i).second;
-      safe_print(fd, "(");
-      safe_print<T>(fd, key);
-      safe_print(fd, " : ");
-      safe_print<uint64_t>(fd, count);
-      safe_print(fd, ")");
-      ++i;
-      if (i != end)
-      {
-        safe_print(fd, ", ");
-      }
-    }
-    safe_print(fd, "]");
-  }
-
-  HistogramStat& operator<<(const T& val)
-  {
-    if (CVC4_USE_STATISTICS)
-    {
-      if (d_hist.find(val) == d_hist.end())
-      {
-        d_hist.insert(std::make_pair(val, 0));
-      }
-      d_hist[val]++;
-    }
-    return (*this);
-  }
-
- private:
-  Histogram d_hist;
-}; /* class HistogramStat */
-
 /**
  * A histogram statistic class for integral types.
- * Avoids using an std::map (like the generic HistogramStat) in favor of a
+ * Avoids using an std::map (like we would do for generic types) 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
  * int64_t, also supporting appropriate enum types.