Replace HistogramStat by IntegralHistogramStat (#6126)

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

diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index 21ffd63b82116a696cabbfd411e7c2268ca3c907..a84f17c28d7977c8fd9e7547a2cd0f37e5ea941b 100644 (file)
--- 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 856e3be5852640e6e9145d5f024d346b60829339..90c240478c40988461a9adcf48a60ef11bb69f71 100644 (file)
--- 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 0882ee2b6446eb604ae9b9e440ea59d3737a1d72..d16f8259ec94c672ccceef497671cd4753cfc5cb 100644 (file)
--- 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 e045dd2edc3b0d04582d7adf68880e8badded64d..78c367881a31fde3856f2dd0d527f4aba4a6fc6f 100644 (file)
--- 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 5cbf957604063193014e3f635f735b10934ff7c1..4f261bc00cdee5eafd36cdf12ad84a1bf993df7e 100644 (file)
--- 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 314a0498dfbb6f495f0e2ccfb7b1f83a5236f14f..54b279e66dedef590dcbf3a70f72e9bc29202bb1 100644 (file)
--- 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 309b06009647c315a3c50a8e87765ce1c20dd595..6c440c51254d7e491fe66a00f801e9d3b567ecbd 100644 (file)
--- 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 c6b6c7e7a9387135d5f8d5433e6fa2f8cd9618b3..c8f7ed420fd4040ffa9978e330934ff1f8ede826 100644 (file)
--- 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 b19e98bbdea787a317672ff8867ab22dd65008a3..869c40ad8a2f72acb5e4cc0f519cde237ef1b72d 100644 (file)
--- 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 6f7338a431fb11a7804feb997cbb4d77bf6d0910..9f5b002af581e23922782a79f126df117a923736 100644 (file)
--- 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 e4d122faf9ad235f1f783cc3adca9c3e1ca4d502..01075eb26ad435af22b051f1bb08712d536e73b3 100644 (file)
--- 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 8e5416629b0fb64d6194d03e498a6bf254c5337f..33e7cd8950332978aa5883027fffd146574bd829 100644 (file)
--- 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 18e3ce12904f9786a4c45cc79f5e22ee9ad366cc..1398d4703760f25538dc832cadab22ecc4ff3c5b 100644 (file)
--- 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 5aed07fc33db6ea1ee07eed65334ab2106b9dd8e..d6fa91f348d5c752c503f7ee94038c4d77c01358 100644 (file)
--- 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 fc615d1710d70e965d66960bf1142eff9f4c8b69..a947c6da69225f7fb75ed2cc69c9f46cf47a70a2 100644 (file)
--- 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 5528cf0109ace49a94d02b64ce2545dd76df9877..49306ba28c2b4b579bf0de735b62237b8886dc68 100644 (file)
--- 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.

diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp
index 3363ba1324ad8f4edbaefc94cc096c9c0550b43c..71cde7e5a3aeba1b2b78691ed1e42c058e72a810 100644 (file)
--- a/test/unit/util/stats_black.cpp
+++ b/test/unit/util/stats_black.cpp
@@ -47,13 +47,6 @@ TEST_F(TestUtilBlackStats, stats)
   BackedStat<double> backedDoubleNoDec("backedDoubleNoDec", 2.0);
   BackedStat<bool> backedBool("backedBool", true);
   BackedStat<void*> backedAddr("backedDouble", (void*)0xDEADBEEF);
-  HistogramStat<int64_t> histStat("hist");
-  histStat << 5;
-  histStat << 6;
-  histStat << 5;
-  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");
@@ -131,8 +124,6 @@ TEST_F(TestUtilBlackStats, stats)
   safe_print(fd, "\n");
   backedBool.safeFlushInformation(fd);
   safe_print(fd, "\n");
-  histStat.safeFlushInformation(fd);
-  safe_print(fd, "\n");
   histIntStat.safeFlushInformation(fd);
   safe_print(fd, "\n");
   histPfRuleStat.safeFlushInformation(fd);
@@ -159,7 +150,6 @@ TEST_F(TestUtilBlackStats, stats)
       "2.0\n"
       "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>";