diff options
Diffstat (limited to 'src/util/stats.h')
-rw-r--r-- | src/util/stats.h | 214 |
1 files changed, 214 insertions, 0 deletions
diff --git a/src/util/stats.h b/src/util/stats.h new file mode 100644 index 000000000..b9f0fdf61 --- /dev/null +++ b/src/util/stats.h @@ -0,0 +1,214 @@ +/********************* */ +/*! \file stats.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** rief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__STATS_H +#define __CVC4__STATS_H + +#include <string> +#include <ostream> +#include <set> +#include "util/Assert.h" + +namespace CVC4 { + + +#ifdef CVC4_STATISTICS_ON +#define USE_STATISTICS true +#else +#define USE_STATISTICS false +#endif + +class CVC4_PUBLIC Stat; + +class CVC4_PUBLIC StatisticsRegistry { +private: + struct StatCmp; + + typedef std::set< Stat*, StatCmp > StatSet; + static StatSet d_registeredStats; + +public: + static void flushStatistics(std::ostream& out); + + static inline void registerStat(Stat* s) throw (AssertionException); +}; /* class StatisticsRegistry */ + + +class CVC4_PUBLIC Stat { +private: + std::string d_name; + + static std::string s_delim; + +public: + + Stat(const std::string& s) throw (CVC4::AssertionException) : d_name(s) + { + if(USE_STATISTICS){ + AlwaysAssert(d_name.find(s_delim) == std::string::npos); + } + } + + virtual void flushInformation(std::ostream& out) const = 0; + + void flushStat(std::ostream& out) const{ + if(USE_STATISTICS){ + out << d_name << s_delim; + flushInformation(out); + } + } + + const std::string& getName() const { + return d_name; + } +}; + +struct StatisticsRegistry::StatCmp { + bool operator()(const Stat* s1, const Stat* s2) const + { + return (s1->getName()) < (s2->getName()); + } +}; + +inline void StatisticsRegistry::registerStat(Stat* s) throw (AssertionException){ + if(USE_STATISTICS){ + AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); + d_registeredStats.insert(s); + } +} + + +template<class T> +class DataStat : public Stat{ +public: + DataStat(const std::string& s) : Stat(s) {} + + virtual const T& getData() const = 0; + virtual void setData(const T&) = 0; + + void flushInformation(std::ostream& out) const{ + if(USE_STATISTICS){ + out << getData(); + } + } +}; + +template <class T> +class ReferenceStat: public DataStat<T>{ +private: + const T* d_data; + +public: + ReferenceStat(const std::string& s): DataStat<T>(s), d_data(NULL){} + + ReferenceStat(const std::string& s, const T& data):ReferenceStat<T>(s){ + setData(data); + } + + void setData(const T& t){ + if(USE_STATISTICS){ + d_data = &t; + } + } + const T& getData() const{ + if(USE_STATISTICS){ + return *d_data; + }else{ + Unreachable(); + } + } +}; + +/** T must have an operator=() and a copy constructor. */ +template <class T> +class BackedStat: public DataStat<T>{ +protected: + T d_data; + +public: + + BackedStat(const std::string& s, const T& init): DataStat<T>(s), d_data(init) + {} + + void setData(const T& t) { + if(USE_STATISTICS){ + d_data = t; + } + } + + BackedStat<T>& operator=(const T& t){ + if(USE_STATISTICS){ + d_data = t; + } + return *this; + } + + const T& getData() const{ + if(USE_STATISTICS){ + return d_data; + }else{ + Unreachable(); + } + } +}; + +class IntStat : public BackedStat<int64_t>{ +public: + + IntStat(const std::string& s, int64_t init): BackedStat<int64_t>(s, init) + {} + + IntStat& operator++(){ + if(USE_STATISTICS){ + ++d_data; + } + return *this; + } + + IntStat& operator+=(int64_t val){ + if(USE_STATISTICS){ + d_data+= val; + } + return *this; + } + + void maxAssign(int64_t val){ + if(USE_STATISTICS){ + if(d_data < val){ + d_data = val; + } + } + } + + void minAssign(int64_t val){ + if(USE_STATISTICS){ + if(d_data > val){ + d_data = val; + } + } + } +}; + +#undef USE_STATISTICS + +}/* CVC4 namespace */ + +#endif /* __CVC4__STATS_H */ |