From 429514c9cb6d187adca027ffc7542cf35543e85d Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 15 Mar 2021 20:58:57 +0100 Subject: [PATCH] Replace HistogramStat by IntegralHistogramStat (#6126) This PR uses IntegralHistogramStat instead of HistogramStat when appropriate, that is everywhere. --- src/expr/proof_checker.h | 2 +- src/preprocessing/util/ite_utilities.h | 2 +- src/proof/sat_proof.h | 8 +-- src/smt/proof_post_processor.h | 2 +- src/theory/arith/theory_arith_private.h | 6 +- src/theory/bags/bags_rewriter.cpp | 2 +- src/theory/bags/bags_rewriter.h | 4 +- src/theory/bags/bags_statistics.h | 2 +- src/theory/strings/sequences_rewriter.cpp | 2 +- src/theory/strings/sequences_rewriter.h | 4 +- src/theory/strings/sequences_stats.h | 12 ++-- src/theory/strings/strings_rewriter.cpp | 2 +- src/theory/strings/strings_rewriter.h | 2 +- .../strings/theory_strings_preprocess.cpp | 2 +- .../strings/theory_strings_preprocess.h | 4 +- src/util/stats_histogram.h | 69 +------------------ test/unit/util/stats_black.cpp | 10 --- 17 files changed, 29 insertions(+), 106 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 d_ruleChecks; + IntegralHistogramStat 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 d_inSmaller; + IntegralHistogramStat 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 d_resChainLengths; - HistogramStat d_usedResChainLengths; - HistogramStat d_clauseGlue; - HistogramStat d_usedClauseGlue; + IntegralHistogramStat d_resChainLengths; + IntegralHistogramStat d_usedResChainLengths; + IntegralHistogramStat d_clauseGlue; + IntegralHistogramStat 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 d_ruleCount; + IntegralHistogramStat 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 d_satPivots; - HistogramStat d_unsatPivots; - HistogramStat d_unknownPivots; + IntegralHistogramStat d_satPivots; + IntegralHistogramStat d_unsatPivots; + IntegralHistogramStat 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* statistics) +BagsRewriter::BagsRewriter(IntegralHistogramStat* 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* statistics = nullptr); + BagsRewriter(IntegralHistogramStat* 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* d_statistics; + IntegralHistogramStat* 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 d_rewrites; + IntegralHistogramStat 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* statistics) +SequencesRewriter::SequencesRewriter(IntegralHistogramStat* 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* statistics); + SequencesRewriter(IntegralHistogramStat* 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* d_statistics; + IntegralHistogramStat* 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 d_inferencesNoPf; + IntegralHistogramStat 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 d_cdSimplifications; + IntegralHistogramStat 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 d_reductions; + IntegralHistogramStat 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 d_regexpUnfoldingsPos; - HistogramStat d_regexpUnfoldingsNeg; + IntegralHistogramStat d_regexpUnfoldingsPos; + IntegralHistogramStat d_regexpUnfoldingsNeg; //--------------- end of inferences /** Counts the number of applications of each type of rewrite rule */ - HistogramStat d_rewrites; + IntegralHistogramStat 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* statistics) +StringsRewriter::StringsRewriter(IntegralHistogramStat* 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* statistics); + StringsRewriter(IntegralHistogramStat* 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 QInternalVarAttribute; StringsPreprocess::StringsPreprocess(SkolemCache* sc, - HistogramStat* statReductions) + IntegralHistogramStat* 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* statReductions = nullptr); + IntegralHistogramStat* 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* d_statReductions; + IntegralHistogramStat* d_statReductions; /** visited cache */ std::map 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 HistogramStat : public Stat -{ - using Histogram = std::map; - 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(fd, key); - safe_print(fd, " : "); - safe_print(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 3363ba132..71cde7e5a 100644 --- a/test/unit/util/stats_black.cpp +++ b/test/unit/util/stats_black.cpp @@ -47,13 +47,6 @@ TEST_F(TestUtilBlackStats, stats) BackedStat backedDoubleNoDec("backedDoubleNoDec", 2.0); BackedStat backedBool("backedBool", true); BackedStat backedAddr("backedDouble", (void*)0xDEADBEEF); - HistogramStat histStat("hist"); - histStat << 5; - histStat << 6; - histStat << 5; - histStat << 10; - histStat << 10; - histStat << 0; IntegralHistogramStat histIntStat("hist-int"); histIntStat << 15 << 16 << 15 << 14 << 16; IntegralHistogramStat 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" ""; -- 2.30.2