summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/proof_checker.h2
-rw-r--r--src/preprocessing/util/ite_utilities.h2
-rw-r--r--src/proof/sat_proof.h8
-rw-r--r--src/smt/proof_post_processor.h2
-rw-r--r--src/theory/arith/theory_arith_private.h6
-rw-r--r--src/theory/bags/bags_rewriter.cpp2
-rw-r--r--src/theory/bags/bags_rewriter.h4
-rw-r--r--src/theory/bags/bags_statistics.h2
-rw-r--r--src/theory/strings/sequences_rewriter.cpp2
-rw-r--r--src/theory/strings/sequences_rewriter.h4
-rw-r--r--src/theory/strings/sequences_stats.h12
-rw-r--r--src/theory/strings/strings_rewriter.cpp2
-rw-r--r--src/theory/strings/strings_rewriter.h2
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp2
-rw-r--r--src/theory/strings/theory_strings_preprocess.h4
-rw-r--r--src/util/stats_histogram.h69
-rw-r--r--test/unit/util/stats_black.cpp10
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<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.
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<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>";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback