summaryrefslogtreecommitdiff
path: root/src/util/statistics_registry.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/statistics_registry.h')
-rw-r--r--src/util/statistics_registry.h766
1 files changed, 766 insertions, 0 deletions
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
new file mode 100644
index 000000000..f4f00e444
--- /dev/null
+++ b/src/util/statistics_registry.h
@@ -0,0 +1,766 @@
+/********************* */
+/*! \file statistics_registry.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: Tim King
+ ** Minor contributors (to current version): Kshitij Bansal
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Statistics utility classes
+ **
+ ** Statistics utility classes, including classes for holding (and referring
+ ** to) statistics, the statistics registry, and some other associated
+ ** classes.
+ **
+ ** This file is somewhat unique in that it is a "cvc4_private_library.h"
+ ** header. Because of this, most classes need to be marked as CVC4_PUBLIC.
+ ** This is because CVC4_PUBLIC is connected to the visibility of the linkage
+ ** in the object files for the class. It does not dictate what headers are
+ ** installed.
+ ** Because the StatisticsRegistry and associated classes are built into
+ ** libutil, which is used by libcvc4, and then later used by the libmain
+ ** without referring to libutil as well. Thus the without marking these as
+ ** CVC4_PUBLIC the symbols would be external in libutil, internal in libcvc4,
+ ** and not be visible to libmain and linking would fail.
+ ** You can debug this using "nm" on the .so and .o files in the builds/
+ ** directory. See
+ ** http://eli.thegreenplace.net/2013/07/09/library-order-in-static-linking
+ ** for a longer discussion on symbol visibility.
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef __CVC4__STATISTICS_REGISTRY_H
+#define __CVC4__STATISTICS_REGISTRY_H
+
+#include <stdint.h>
+
+#include <cassert>
+#include <ctime>
+#include <iomanip>
+#include <map>
+#include <sstream>
+#include <vector>
+
+#include "base/exception.h"
+#include "lib/clock_gettime.h"
+#include "util/statistics.h"
+
+namespace CVC4 {
+
+/**
+ * Prints a timespec.
+ *
+ * This is used in the implementation of TimerStat. This needs to be available
+ * before Stat due to ordering constraints in clang for TimerStat.
+ */
+std::ostream& operator<<(std::ostream& os, const timespec& t) CVC4_PUBLIC;
+
+#ifdef CVC4_STATISTICS_ON
+# define __CVC4_USE_STATISTICS true
+#else
+# define __CVC4_USE_STATISTICS false
+#endif
+
+
+/**
+ * The base class for all statistics.
+ *
+ * This base class keeps the name of the statistic and declares the (pure)
+ * virtual function flushInformation(). Derived classes must implement
+ * this function and pass their name to the base class constructor.
+ *
+ * This class also (statically) maintains the delimiter used to separate
+ * the name and the value when statistics are output.
+ */
+class Stat {
+protected:
+ /** The name of this statistic */
+ std::string d_name;
+
+public:
+
+ /** Nullary constructor, does nothing */
+ Stat() { }
+
+ /**
+ * Construct a statistic with the given name. Debug builds of CVC4
+ * will throw an assertion exception if the given name contains the
+ * statistic delimiter string.
+ */
+ Stat(const std::string& name) throw(CVC4::IllegalArgumentException) :
+ d_name(name) {
+ if(__CVC4_USE_STATISTICS) {
+ CheckArgument(d_name.find(", ") == std::string::npos, name,
+ "Statistics names cannot include a comma (',')");
+ }
+ }
+
+ /** Destruct a statistic. This base-class version does nothing. */
+ virtual ~Stat() {}
+
+ /**
+ * Flush the value of this statistic to an output stream. Should
+ * finish the output with an end-of-line character.
+ */
+ virtual void flushInformation(std::ostream& out) const = 0;
+
+ /**
+ * Flush the name,value pair of this statistic to an output stream.
+ * Uses the statistic delimiter string between name and value.
+ *
+ * May be redefined by a child class
+ */
+ virtual void flushStat(std::ostream& out) const {
+ if(__CVC4_USE_STATISTICS) {
+ out << d_name << ", ";
+ flushInformation(out);
+ }
+ }
+
+ /** Get the name of this statistic. */
+ const std::string& getName() const {
+ return d_name;
+ }
+
+ /** Get the value of this statistic as a string. */
+ virtual SExpr getValue() const {
+ std::stringstream ss;
+ flushInformation(ss);
+ return SExpr(ss.str());
+ }
+
+};/* class Stat */
+
+// A generic way of making a SExpr from templated stats code.
+// for example, the uint64_t version ensures that we create
+// Integer-SExprs for ReadOnlyDataStats (like those inside
+// Minisat) without having to specialize the entire
+// ReadOnlyDataStat class template.
+template <class T>
+inline SExpr mkSExpr(const T& x) {
+ std::stringstream ss;
+ ss << x;
+ return SExpr(ss.str());
+}
+
+template <>
+inline SExpr mkSExpr(const uint64_t& x) {
+ return SExpr(Integer(x));
+}
+
+template <>
+inline SExpr mkSExpr(const int64_t& x) {
+ return SExpr(Integer(x));
+}
+
+template <>
+inline SExpr mkSExpr(const int& x) {
+ return SExpr(Integer(x));
+}
+
+template <>
+inline SExpr mkSExpr(const Integer& x) {
+ return SExpr(x);
+}
+
+template <>
+inline SExpr mkSExpr(const double& x) {
+ // roundabout way to get a Rational from a double
+ std::stringstream ss;
+ ss << std::fixed << std::setprecision(8) << x;
+ return SExpr(Rational::fromDecimal(ss.str()));
+}
+
+template <>
+inline SExpr mkSExpr(const Rational& x) {
+ return SExpr(x);
+}
+
+/**
+ * A class to represent a "read-only" data statistic of type T. Adds to
+ * the Stat base class the pure virtual function getData(), which returns
+ * type T, and flushInformation(), which outputs the statistic value to an
+ * output stream (using the same existing stream insertion operator).
+ *
+ * Template class T must have stream insertion operation defined:
+ * std::ostream& operator<<(std::ostream&, const T&)
+ */
+template <class T>
+class ReadOnlyDataStat : public Stat {
+public:
+ /** The "payload" type of this data statistic (that is, T). */
+ typedef T payload_t;
+
+ /** Construct a read-only data statistic with the given name. */
+ ReadOnlyDataStat(const std::string& name) :
+ Stat(name) {
+ }
+
+ /** Get the value of the statistic. */
+ virtual T getData() const = 0;
+
+ /** Flush the value of the statistic to the given output stream. */
+ void flushInformation(std::ostream& out) const {
+ if(__CVC4_USE_STATISTICS) {
+ out << getData();
+ }
+ }
+
+ SExpr getValue() const {
+ return mkSExpr(getData());
+ }
+
+};/* class ReadOnlyDataStat<T> */
+
+
+/**
+ * A data statistic class. This class extends a read-only data statistic
+ * with assignment (the statistic can be set as well as read). This class
+ * adds to the read-only case a pure virtual function setData(), thus
+ * providing the basic interface for a data statistic: getData() to get the
+ * statistic value, and setData() to set it.
+ *
+ * As with the read-only data statistic class, template class T must have
+ * stream insertion operation defined:
+ * std::ostream& operator<<(std::ostream&, const T&)
+ */
+template <class T>
+class DataStat : public ReadOnlyDataStat<T> {
+public:
+
+ /** Construct a data statistic with the given name. */
+ DataStat(const std::string& name) :
+ ReadOnlyDataStat<T>(name) {
+ }
+
+ /** Set the data statistic. */
+ virtual void setData(const T&) = 0;
+
+};/* class DataStat<T> */
+
+
+/**
+ * A data statistic that references a data cell of type T,
+ * implementing getData() by referencing that memory cell, and
+ * setData() by reassigning the statistic to point to the new
+ * data cell. The referenced data cell is kept as a const
+ * reference, meaning the referenced data is never actually
+ * modified by this class (it must be externally modified for
+ * a reference statistic to make sense). A common use for
+ * this type of statistic is to output a statistic that is kept
+ * outside the statistics package (for example, one that's kept
+ * by a theory implementation for internal heuristic purposes,
+ * which is important to keep even if statistics are turned off).
+ *
+ * Template class T must have an assignment operator=().
+ */
+template <class T>
+class ReferenceStat : public DataStat<T> {
+private:
+ /** The referenced data cell */
+ const T* d_data;
+
+public:
+ /**
+ * Construct a reference stat with the given name and a reference
+ * to NULL.
+ */
+ ReferenceStat(const std::string& name) :
+ DataStat<T>(name),
+ d_data(NULL) {
+ }
+
+ /**
+ * Construct a reference stat with the given name and a reference to
+ * the given data.
+ */
+ ReferenceStat(const std::string& name, const T& data) :
+ DataStat<T>(name),
+ d_data(NULL) {
+ setData(data);
+ }
+
+ /** Set this reference statistic to refer to the given data cell. */
+ void setData(const T& t) {
+ if(__CVC4_USE_STATISTICS) {
+ d_data = &t;
+ }
+ }
+
+ /** Get the value of the referenced data cell. */
+ T getData() const {
+ return *d_data;
+ }
+
+};/* class ReferenceStat<T> */
+
+
+/**
+ * A data statistic that keeps a T and sets it with setData().
+ *
+ * Template class T must have an operator=() and a copy constructor.
+ */
+template <class T>
+class BackedStat : public DataStat<T> {
+protected:
+ /** The internally-kept statistic value */
+ T d_data;
+
+public:
+
+ /** Construct a backed statistic with the given name and initial value. */
+ BackedStat(const std::string& name, const T& init) :
+ DataStat<T>(name),
+ d_data(init) {
+ }
+
+ /** Set the underlying data value to the given value. */
+ void setData(const T& t) {
+ if(__CVC4_USE_STATISTICS) {
+ d_data = t;
+ }
+ }
+
+ /** Identical to setData(). */
+ BackedStat<T>& operator=(const T& t) {
+ if(__CVC4_USE_STATISTICS) {
+ d_data = t;
+ }
+ return *this;
+ }
+
+ /** Get the underlying data value. */
+ T getData() const {
+ return d_data;
+ }
+
+};/* class BackedStat<T> */
+
+
+/**
+ * A wrapper Stat for another Stat.
+ *
+ * This type of Stat is useful in cases where a module (like the
+ * CongruenceClosure module) might keep its own statistics, but might
+ * be instantiated in many contexts by many clients. This makes such
+ * a statistic inappopriate to register with the StatisticsRegistry
+ * directly, as all would be output with the same name (and may be
+ * unregistered too quickly anyway). A WrappedStat allows the calling
+ * client (say, TheoryUF) to wrap the Stat from the client module,
+ * giving it a globally unique name.
+ */
+template <class Stat>
+class WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> {
+ typedef typename Stat::payload_t T;
+
+ const ReadOnlyDataStat<T>& d_stat;
+
+ /** Private copy constructor undefined (no copy permitted). */
+ WrappedStat(const WrappedStat&) CVC4_UNDEFINED;
+ /** Private assignment operator undefined (no copy permitted). */
+ WrappedStat<T>& operator=(const WrappedStat&) CVC4_UNDEFINED;
+
+public:
+
+ /**
+ * Construct a wrapped statistic with the given name that wraps the
+ * given statistic.
+ */
+ WrappedStat(const std::string& name, const ReadOnlyDataStat<T>& stat) :
+ ReadOnlyDataStat<T>(name),
+ d_stat(stat) {
+ }
+
+ /** Get the data of the underlying (wrapped) statistic. */
+ T getData() const {
+ return d_stat.getData();
+ }
+
+ SExpr getValue() const {
+ return d_stat.getValue();
+ }
+
+};/* class WrappedStat<T> */
+
+/**
+ * A backed integer-valued (64-bit signed) statistic.
+ * This doesn't functionally differ from its base class BackedStat<int64_t>,
+ * except for adding convenience functions for dealing with integers.
+ */
+class IntStat : public BackedStat<int64_t> {
+public:
+
+ /**
+ * Construct an integer-valued statistic with the given name and
+ * initial value.
+ */
+ IntStat(const std::string& name, int64_t init) :
+ BackedStat<int64_t>(name, init) {
+ }
+
+ /** Increment the underlying integer statistic. */
+ IntStat& operator++() {
+ if(__CVC4_USE_STATISTICS) {
+ ++d_data;
+ }
+ return *this;
+ }
+
+ /** Increment the underlying integer statistic by the given amount. */
+ IntStat& operator+=(int64_t val) {
+ if(__CVC4_USE_STATISTICS) {
+ d_data += val;
+ }
+ return *this;
+ }
+
+ /** Keep the maximum of the current statistic value and the given one. */
+ void maxAssign(int64_t val) {
+ if(__CVC4_USE_STATISTICS) {
+ if(d_data < val) {
+ d_data = val;
+ }
+ }
+ }
+
+ /** Keep the minimum of the current statistic value and the given one. */
+ void minAssign(int64_t val) {
+ if(__CVC4_USE_STATISTICS) {
+ if(d_data > val) {
+ d_data = val;
+ }
+ }
+ }
+
+ SExpr getValue() const {
+ return SExpr(Integer(d_data));
+ }
+
+};/* class IntStat */
+
+template <class T>
+class SizeStat : public Stat {
+private:
+ const T& d_sized;
+public:
+ SizeStat(const std::string&name, const T& sized) :
+ Stat(name), d_sized(sized) {}
+ ~SizeStat() {}
+
+ void flushInformation(std::ostream& out) const {
+ out << d_sized.size();
+ }
+
+ SExpr getValue() const {
+ return SExpr(Integer(d_sized.size()));
+ }
+
+};/* class SizeStat */
+
+/**
+ * The value for an AverageStat is the running average of (e1, e_2, ..., e_n),
+ * (e1 + e_2 + ... + e_n)/n,
+ * where e_i is an entry added by an addEntry(e_i) call.
+ * The value is initially always 0.
+ * (This is to avoid making parsers confused.)
+ *
+ * A call to setData() will change the running average but not reset the
+ * running count, so should generally be avoided. Call addEntry() to add
+ * an entry to the average calculation.
+ */
+class AverageStat : public BackedStat<double> {
+private:
+ /**
+ * The number of accumulations of the running average that we
+ * have seen so far.
+ */
+ uint32_t d_count;
+ double d_sum;
+
+public:
+ /** Construct an average statistic with the given name. */
+ AverageStat(const std::string& name) :
+ BackedStat<double>(name, 0.0), d_count(0), d_sum(0.0) {
+ }
+
+ /** Add an entry to the running-average calculation. */
+ void addEntry(double e) {
+ if(__CVC4_USE_STATISTICS) {
+ ++d_count;
+ d_sum += e;
+ setData(d_sum / d_count);
+ }
+ }
+
+ SExpr getValue() const {
+ std::stringstream ss;
+ ss << std::fixed << std::setprecision(8) << d_data;
+ return SExpr(Rational::fromDecimal(ss.str()));
+ }
+
+};/* class AverageStat */
+
+/** A statistic that contains a SExpr. */
+class SExprStat : public Stat {
+private:
+ SExpr d_data;
+
+public:
+
+ /**
+ * Construct a SExpr-valued statistic with the given name and
+ * initial value.
+ */
+ SExprStat(const std::string& name, const SExpr& init) :
+ Stat(name), d_data(init){}
+
+ virtual void flushInformation(std::ostream& out) const {
+ out << d_data << std::endl;
+ }
+
+ SExpr getValue() const {
+ return d_data;
+ }
+
+};/* 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;
+ 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 */
+/****************************************************************************/
+
+/**
+ * The main statistics registry. This registry maintains the list of
+ * currently active statistics and is able to "flush" them all.
+ */
+class CVC4_PUBLIC StatisticsRegistry : public StatisticsBase, public Stat {
+private:
+
+ /** Private copy constructor undefined (no copy permitted). */
+ StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED;
+
+public:
+
+ /** Construct an nameless statistics registry */
+ StatisticsRegistry() {}
+
+ /** Construct a statistics registry */
+ StatisticsRegistry(const std::string& name)
+ throw(CVC4::IllegalArgumentException);
+
+ /**
+ * Set the name of this statistic registry, used as prefix during
+ * output. (This version overrides StatisticsBase::setPrefix().)
+ */
+ void setPrefix(const std::string& name) {
+ d_prefix = d_name = name;
+ }
+
+ /** Overridden to avoid the name being printed */
+ void flushStat(std::ostream &out) const;
+
+ virtual void flushInformation(std::ostream& out) const;
+
+ SExpr getValue() const {
+ std::vector<SExpr> v;
+ for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
+ std::vector<SExpr> w;
+ w.push_back(SExpr((*i)->getName()));
+ w.push_back((*i)->getValue());
+ v.push_back(SExpr(w));
+ }
+ return SExpr(v);
+ }
+
+ /** Register a new statistic */
+ void registerStat(Stat* s) throw(CVC4::IllegalArgumentException);
+
+ /** Unregister a new statistic */
+ void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException);
+
+};/* class StatisticsRegistry */
+
+class CodeTimer;
+
+/**
+ * A timer statistic. The timer can be started and stopped
+ * arbitrarily, like a stopwatch; the value of the statistic at the
+ * end is the accumulated time over all (start,stop) pairs.
+ */
+class CVC4_PUBLIC TimerStat : public BackedStat<timespec> {
+
+ // strange: timespec isn't placed in 'std' namespace ?!
+ /** The last start time of this timer */
+ timespec d_start;
+
+ /** Whether this timer is currently running */
+ bool d_running;
+
+public:
+
+ typedef CVC4::CodeTimer CodeTimer;
+
+ /**
+ * Construct a timer statistic with the given name. Newly-constructed
+ * timers have a 0.0 value and are not running.
+ */
+ TimerStat(const std::string& name) :
+ BackedStat< timespec >(name, timespec()),
+ d_running(false) {
+ /* timespec is POD and so may not be initialized to zero;
+ * here, ensure it is */
+ d_data.tv_sec = d_data.tv_nsec = 0;
+ }
+
+ /** Start the timer. */
+ void start();
+
+ /**
+ * Stop the timer and update the statistic value with the
+ * accumulated time.
+ */
+ void stop();
+
+ /** If the timer is currently running */
+ bool running() const;
+
+ timespec getData() const;
+
+ SExpr getValue() const;
+
+};/* class TimerStat */
+
+/**
+ * Utility class to make it easier to call stop() at the end of a
+ * code block. When constructed, it starts the timer. When
+ * destructed, it stops the timer.
+ */
+class CodeTimer {
+ TimerStat& d_timer;
+ bool d_reentrant;
+
+ /** Private copy constructor undefined (no copy permitted). */
+ CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED;
+ /** Private assignment operator undefined (no copy permitted). */
+ CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED;
+
+public:
+ CodeTimer(TimerStat& timer, bool allow_reentrant = false) : d_timer(timer), d_reentrant(false) {
+ if(!allow_reentrant || !(d_reentrant = d_timer.running())) {
+ d_timer.start();
+ }
+ }
+ ~CodeTimer() {
+ if(!d_reentrant) {
+ d_timer.stop();
+ }
+ }
+};/* class CodeTimer */
+
+/**
+ * Resource-acquisition-is-initialization idiom for statistics
+ * registry. Useful for stack-based statistics (like in the driver).
+ * Generally, for statistics kept in a member field of class, it's
+ * better to use the above KEEP_STATISTIC(), which does declaration of
+ * the member, construction of the statistic, and
+ * registration/unregistration. This RAII class only does
+ * registration and unregistration.
+ */
+class CVC4_PUBLIC RegisterStatistic {
+public:
+ RegisterStatistic(StatisticsRegistry* reg, Stat* stat);
+ ~RegisterStatistic();
+
+private:
+ StatisticsRegistry* d_reg;
+ Stat* d_stat;
+
+};/* class RegisterStatistic */
+
+#undef __CVC4_USE_STATISTICS
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__STATISTICS_REGISTRY_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback