11 files changed, 21 insertions, 21 deletions
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;
   /**