summaryrefslogtreecommitdiff
path: root/src/util/stats.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/stats.h')
-rw-r--r--src/util/stats.h215
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback