diff options
Diffstat (limited to 'src/util/statistics_registry.h')
-rw-r--r-- | src/util/statistics_registry.h | 106 |
1 files changed, 66 insertions, 40 deletions
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 4f2c356e8..1206a3e4a 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -47,6 +47,7 @@ #include "base/exception.h" #include "lib/clock_gettime.h" +#include "util/safe_print.h" #include "util/statistics.h" namespace CVC4 { @@ -109,6 +110,13 @@ public: virtual void flushInformation(std::ostream& out) const = 0; /** + * Flush the value of this statistic to a file descriptor. Should finish the + * output with an end-of-line character. Should be safe to use in a signal + * handler. + */ + virtual void safeFlushInformation(int fd) const = 0; + + /** * Flush the name,value pair of this statistic to an output stream. * Uses the statistic delimiter string between name and value. * @@ -121,6 +129,20 @@ public: } } + /** + * Flush the name,value pair of this statistic to a file descriptor. Uses the + * statistic delimiter string between name and value. + * + * May be redefined by a child class + */ + virtual void safeFlushStat(int fd) const { + if (__CVC4_USE_STATISTICS) { + safe_print(fd, d_name.c_str()); + safe_print(fd, ", "); + safeFlushInformation(fd); + } + } + /** Get the name of this statistic. */ const std::string& getName() const { return d_name; @@ -210,6 +232,12 @@ public: } } + virtual void safeFlushInformation(int fd) const { + if (__CVC4_USE_STATISTICS) { + safe_print<T>(fd, getData()); + } + } + SExpr getValue() const { return mkSExpr(getData()); } @@ -298,7 +326,6 @@ public: };/* class ReferenceStat<T> */ - /** * A data statistic that keeps a T and sets it with setData(). * @@ -340,7 +367,6 @@ public: };/* class BackedStat<T> */ - /** * A wrapper Stat for another Stat. * @@ -455,6 +481,10 @@ public: out << d_sized.size(); } + void safeFlushInformation(int fd) const { + safe_print<uint64_t>(fd, d_sized.size()); + } + SExpr getValue() const { return SExpr(Integer(d_sized.size())); } @@ -522,6 +552,12 @@ public: out << d_data << std::endl; } + virtual void safeFlushInformation(int fd) const { + // SExprStat is only used in statistics.cpp in copyFrom, which we cannot + // do in a signal handler anyway. + safe_print(fd, "<unsupported>"); + } + SExpr getValue() const { return d_data; } @@ -529,44 +565,6 @@ public: };/* class SExprStat */ template <class T> -class ListStat : public Stat { -private: - typedef std::vector<T> List; - List d_list; -public: - - /** - * Construct an integer-valued statistic with the given name and - * initial value. - */ - ListStat(const std::string& name) : Stat(name) {} - ~ListStat() {} - - void flushInformation(std::ostream& out) const{ - if(__CVC4_USE_STATISTICS) { - typename List::const_iterator i = d_list.begin(), end = d_list.end(); - out << "["; - if(i != end){ - out << *i; - ++i; - for(; i != end; ++i){ - out << ", " << *i; - } - } - out << "]"; - } - } - - ListStat& operator<<(const T& val){ - if(__CVC4_USE_STATISTICS) { - d_list.push_back(val); - } - return (*this); - } - -};/* class ListStat */ - -template <class T> class HistogramStat : public Stat { private: typedef std::map<T, unsigned int> Histogram; @@ -595,6 +593,28 @@ public: } } + virtual void safeFlushInformation(int fd) const { + if (__CVC4_USE_STATISTICS) { + typename Histogram::const_iterator i = d_hist.begin(); + typename Histogram::const_iterator end = d_hist.end(); + safe_print(fd, "["); + while (i != end) { + const T& key = (*i).first; + unsigned int 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()){ @@ -643,6 +663,8 @@ public: virtual void flushInformation(std::ostream& out) const; + virtual void safeFlushInformation(int fd) const; + SExpr getValue() const { std::vector<SExpr> v; for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { @@ -708,6 +730,10 @@ public: timespec getData() const; + virtual void safeFlushInformation(int fd) const { + safe_print<timespec>(fd, d_data); + } + SExpr getValue() const; };/* class TimerStat */ |