diff options
author | Tim King <taking@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
commit | 9098391fe334d829ec4101f190b8f1fa21c30752 (patch) | |
tree | b134fc1fe1c767a50013e1449330ca6a7ee18a3d /src/util/statistics_registry.h | |
parent | a9174ce4dc3939bbe14c9aa1fd11c79c7877eb16 (diff) |
FCSimplex branch merge
Diffstat (limited to 'src/util/statistics_registry.h')
-rw-r--r-- | src/util/statistics_registry.h | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index e0bc81d91..3bec559d5 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -29,6 +29,7 @@ #include <iomanip> #include <ctime> #include <vector> +#include <map> #include <stdint.h> #include <cassert> @@ -537,6 +538,47 @@ public: };/* class ListStat */ +template <class T> +class HistogramStat : public Stat { +private: + typedef std::map<T, unsigned int> Histogram; + Histogram d_hist; +public: + + /** Construct a histogram of a stream of entries. */ + HistogramStat(const std::string& name) : Stat(name) {} + ~HistogramStat() {} + + void flushInformation(std::ostream& out) const{ + if(__CVC4_USE_STATISTICS) { + typename Histogram::const_iterator i = d_hist.begin(); + typename Histogram::const_iterator end = d_hist.end(); + out << "["; + while(i != end){ + const T& key = (*i).first; + unsigned int count = (*i).second; + out << "("<<key<<" : "<<count<< ")"; + ++i; + if(i != end){ + out << ", "; + } + } + out << "]"; + } + } + + 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); + } + +};/* class HistogramStat */ + /****************************************************************************/ /* Statistics Registry */ /****************************************************************************/ |