diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-09-02 07:31:04 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-09-02 07:31:04 +0000 |
commit | 79015a017495691ddfe2a4479de8fb7d558e4228 (patch) | |
tree | bd985ccb0c453c26100f6420807072ed7d81d530 /src/util | |
parent | 81d178c1ca853754aaa614d0400e45a8900092b9 (diff) |
* add TimerStat statistic type
* add Stats black-box unit test
* new make target: "make units" now runs unit tests only
* revised make target: "make regress" now runs regressions only
* configure.ac: pull in librt for clock_gettime()
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/stats.h | 215 |
1 files changed, 165 insertions, 50 deletions
diff --git a/src/util/stats.h b/src/util/stats.h index f917e8b52..74afb5792 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -24,16 +24,19 @@ #include <string> #include <ostream> +#include <iomanip> #include <set> +#include <ctime> + #include "util/Assert.h" namespace CVC4 { #ifdef CVC4_STATISTICS_ON -# define USE_STATISTICS true +# define __CVC4_USE_STATISTICS true #else -# define USE_STATISTICS false +# define __CVC4_USE_STATISTICS false #endif class CVC4_PUBLIC Stat; @@ -48,8 +51,8 @@ private: public: static void flushStatistics(std::ostream& out); - static inline void registerStat(Stat* s) throw (AssertionException); - static inline void unregisterStat(Stat* s) throw (AssertionException); + static inline void registerStat(Stat* s) throw(AssertionException); + static inline void unregisterStat(Stat* s) throw(AssertionException); };/* class StatisticsRegistry */ @@ -61,9 +64,9 @@ private: public: - Stat(const std::string& s) throw (CVC4::AssertionException) : d_name(s) + Stat(const std::string& s) throw(CVC4::AssertionException) : d_name(s) { - if(USE_STATISTICS){ + if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_name.find(s_delim) == std::string::npos); } } @@ -71,8 +74,8 @@ public: virtual void flushInformation(std::ostream& out) const = 0; - void flushStat(std::ostream& out) const{ - if(USE_STATISTICS){ + void flushStat(std::ostream& out) const { + if(__CVC4_USE_STATISTICS) { out << d_name << s_delim; flushInformation(out); } @@ -81,27 +84,31 @@ public: const std::string& getName() const { return d_name; } -}; +};/* class Stat */ + struct StatisticsRegistry::StatCmp { bool operator()(const Stat* s1, const Stat* s2) const { return (s1->getName()) < (s2->getName()); } -}; +};/* class StatCmp */ + -inline void StatisticsRegistry::registerStat(Stat* s) throw (AssertionException){ - if(USE_STATISTICS){ +inline void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { + if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); d_registeredStats.insert(s); } -} -inline void StatisticsRegistry::unregisterStat(Stat* s) throw (AssertionException){ - if(USE_STATISTICS){ +}/* StatisticsRegistry::registerStat */ + + +inline void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { + if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end()); d_registeredStats.erase(s); } -} +}/* StatisticsRegistry::unregisterStat */ @@ -109,24 +116,25 @@ inline void StatisticsRegistry::unregisterStat(Stat* s) throw (AssertionExceptio * class T must have stream insertion operation defined. * std::ostream& operator<<(std::ostream&, const T&); */ -template<class T> -class DataStat : public Stat{ +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){ + void flushInformation(std::ostream& out) const { + if(__CVC4_USE_STATISTICS) { out << getData(); } } -}; +};/* class DataStat */ + /** T must have an assignment operator=(). */ template <class T> -class ReferenceStat: public DataStat<T>{ +class ReferenceStat : public DataStat<T> { private: const T* d_data; @@ -136,28 +144,29 @@ public: {} ReferenceStat(const std::string& s, const T& data): - DataStat<T>(s),d_data(NULL) + DataStat<T>(s), d_data(NULL) { setData(data); } - void setData(const T& t){ - if(USE_STATISTICS){ + void setData(const T& t) { + if(__CVC4_USE_STATISTICS) { d_data = &t; } } - const T& getData() const{ - if(USE_STATISTICS){ + const T& getData() const { + if(__CVC4_USE_STATISTICS) { return *d_data; - }else{ + } else { Unreachable(); } } -}; +};/* class ReferenceStat */ + /** T must have an operator=() and a copy constructor. */ template <class T> -class BackedStat: public DataStat<T>{ +class BackedStat : public DataStat<T> { protected: T d_data; @@ -167,65 +176,171 @@ public: {} void setData(const T& t) { - if(USE_STATISTICS){ + if(__CVC4_USE_STATISTICS) { d_data = t; } } - BackedStat<T>& operator=(const T& t){ - if(USE_STATISTICS){ + BackedStat<T>& operator=(const T& t) { + if(__CVC4_USE_STATISTICS) { d_data = t; } return *this; } - const T& getData() const{ - if(USE_STATISTICS){ + const T& getData() const { + if(__CVC4_USE_STATISTICS) { return d_data; - }else{ + } else { Unreachable(); } } -}; +};/* class BackedStat */ + -class IntStat : public BackedStat<int64_t>{ +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){ + IntStat& operator++() { + if(__CVC4_USE_STATISTICS) { ++d_data; } return *this; } - IntStat& operator+=(int64_t val){ - if(USE_STATISTICS){ + IntStat& operator+=(int64_t val) { + if(__CVC4_USE_STATISTICS) { d_data+= val; } return *this; } - void maxAssign(int64_t val){ - if(USE_STATISTICS){ - if(d_data < val){ + void maxAssign(int64_t val) { + if(__CVC4_USE_STATISTICS) { + if(d_data < val) { d_data = val; } } } - void minAssign(int64_t val){ - if(USE_STATISTICS){ - if(d_data > val){ + void minAssign(int64_t val) { + if(__CVC4_USE_STATISTICS) { + if(d_data > val) { d_data = val; } } } -}; +};/* class IntStat */ + + +// some utility functions for ::timespec +inline ::timespec& operator+=(::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + const long nsec_per_sec = 1000000000L; // one thousand million + a.tv_sec += b.tv_sec; + long nsec = a.tv_nsec + b.tv_nsec; + while(nsec < 0) { + nsec += nsec_per_sec; + ++a.tv_sec; + } + while(nsec >= nsec_per_sec) { + nsec -= nsec_per_sec; + --a.tv_sec; + } + a.tv_nsec = nsec; + return a; +} +inline ::timespec& operator-=(::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + const long nsec_per_sec = 1000000000L; // one thousand million + a.tv_sec -= b.tv_sec; + long nsec = a.tv_nsec - b.tv_nsec; + while(nsec < 0) { + nsec += nsec_per_sec; + ++a.tv_sec; + } + while(nsec >= nsec_per_sec) { + nsec -= nsec_per_sec; + --a.tv_sec; + } + a.tv_nsec = nsec; + return a; +} +inline ::timespec operator+(const ::timespec& a, const ::timespec& b) { + ::timespec result = a; + return result += b; +} +inline ::timespec operator-(const ::timespec& a, const ::timespec& b) { + ::timespec result = a; + return result -= b; +} +inline bool operator==(const ::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec; +} +inline bool operator!=(const ::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a == b); +} +inline bool operator<(const ::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec < b.tv_sec || + (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec); +} +inline bool operator>(const ::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec > b.tv_sec || + (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec); +} +inline bool operator<=(const ::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a > b); +} +inline bool operator>=(const ::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a < b); +} +inline std::ostream& operator<<(std::ostream& os, const ::timespec& t) { + // assumes t.tv_nsec is in range + return os << t.tv_sec << "." + << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec; +} + + +class TimerStat : public BackedStat< ::timespec > { + // strange: timespec isn't placed in 'std' namespace ?! + ::timespec d_start; + bool d_running; + +public: + + TimerStat(const std::string& s) : + BackedStat< ::timespec >(s, ::timespec()), + d_running(false) { + } + + void start() { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(!d_running); + clock_gettime(CLOCK_REALTIME, &d_start); + } + } + + void stop() { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(d_running); + ::timespec end; + clock_gettime(CLOCK_REALTIME, &end); + d_data += end - d_start; + } + } +};/* class TimerStat */ + -#undef USE_STATISTICS +#undef __CVC4_USE_STATISTICS }/* CVC4 namespace */ |