src/util/stats.h

   1 /*********************                                                        */
   2 /*! \file stats.h
   3  ** \verbatim
   4  ** Original author: taking
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief [[ Add one-line brief description here ]]
  15  **
  16  ** [[ Add lengthier description here ]]
  17  ** \todo document this file
  18  **/
  19
  20 #include "cvc4_public.h"
  21
  22 #ifndef __CVC4__STATS_H
  23 #define __CVC4__STATS_H
  24
  25 #include <string>
  26 #include <ostream>
  27 #include <iomanip>
  28 #include <set>
  29 #include <ctime>
  30
  31 #include "util/Assert.h"
  32 #include "lib/clock_gettime.h"
  33
  34 namespace CVC4 {
  35
  36
  37 #ifdef CVC4_STATISTICS_ON
  38 #  define __CVC4_USE_STATISTICS true
  39 #else
  40 #  define __CVC4_USE_STATISTICS false
  41 #endif
  42
  43 class CVC4_PUBLIC Stat;
  44
  45 class CVC4_PUBLIC StatisticsRegistry {
  46 private:
  47   struct StatCmp;
  48
  49   typedef std::set< Stat*, StatCmp > StatSet;
  50   static StatSet d_registeredStats;
  51
  52 public:
  53   static void flushStatistics(std::ostream& out);
  54
  55   static inline void registerStat(Stat* s) throw(AssertionException);
  56   static inline void unregisterStat(Stat* s) throw(AssertionException);
  57 };/* class StatisticsRegistry */
  58
  59
  60 class CVC4_PUBLIC Stat {
  61 private:
  62   std::string d_name;
  63
  64   static std::string s_delim;
  65
  66 public:
  67
  68   Stat(const std::string& s) throw(CVC4::AssertionException) : d_name(s)
  69   {
  70     if(__CVC4_USE_STATISTICS) {
  71       AlwaysAssert(d_name.find(s_delim) == std::string::npos);
  72     }
  73   }
  74   virtual ~Stat() {}
  75
  76   virtual void flushInformation(std::ostream& out) const = 0;
  77
  78   void flushStat(std::ostream& out) const {
  79     if(__CVC4_USE_STATISTICS) {
  80       out << d_name << s_delim;
  81       flushInformation(out);
  82     }
  83   }
  84
  85   const std::string& getName() const {
  86     return d_name;
  87   }
  88 };/* class Stat */
  89
  90
  91 struct StatisticsRegistry::StatCmp {
  92   bool operator()(const Stat* s1, const Stat* s2) const
  93   {
  94     return (s1->getName()) < (s2->getName());
  95   }
  96 };/* class StatCmp */
  97
  98
  99 inline void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
 100   if(__CVC4_USE_STATISTICS) {
 101     AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end());
 102     d_registeredStats.insert(s);
 103   }
 104 }/* StatisticsRegistry::registerStat */
 105
 106
 107 inline void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
 108   if(__CVC4_USE_STATISTICS) {
 109     AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end());
 110     d_registeredStats.erase(s);
 111   }
 112 }/* StatisticsRegistry::unregisterStat */
 113
 114
 115
 116 /**
 117  * class T must have stream insertion operation defined.
 118  * std::ostream& operator<<(std::ostream&, const T&);
 119  */
 120 template <class T>
 121 class DataStat : public Stat {
 122 public:
 123   DataStat(const std::string& s) : Stat(s) {}
 124
 125   virtual const T& getData() const = 0;
 126   virtual void setData(const T&) = 0;
 127
 128   void flushInformation(std::ostream& out) const {
 129     if(__CVC4_USE_STATISTICS) {
 130       out << getData();
 131     }
 132   }
 133 };/* class DataStat */
 134
 135
 136 /** T must have an assignment operator=(). */
 137 template <class T>
 138 class ReferenceStat : public DataStat<T> {
 139 private:
 140   const T* d_data;
 141
 142 public:
 143   ReferenceStat(const std::string& s):
 144     DataStat<T>(s), d_data(NULL)
 145   {}
 146
 147   ReferenceStat(const std::string& s, const T& data):
 148     DataStat<T>(s), d_data(NULL)
 149   {
 150     setData(data);
 151   }
 152
 153   void setData(const T& t) {
 154     if(__CVC4_USE_STATISTICS) {
 155       d_data = &t;
 156     }
 157   }
 158   const T& getData() const {
 159     if(__CVC4_USE_STATISTICS) {
 160       return *d_data;
 161     } else {
 162       Unreachable();
 163     }
 164   }
 165 };/* class ReferenceStat */
 166
 167
 168 /** T must have an operator=() and a copy constructor. */
 169 template <class T>
 170 class BackedStat : public DataStat<T> {
 171 protected:
 172   T d_data;
 173
 174 public:
 175
 176   BackedStat(const std::string& s, const T& init): DataStat<T>(s), d_data(init)
 177   {}
 178
 179   void setData(const T& t) {
 180     if(__CVC4_USE_STATISTICS) {
 181       d_data = t;
 182     }
 183   }
 184
 185   BackedStat<T>& operator=(const T& t) {
 186     if(__CVC4_USE_STATISTICS) {
 187       d_data = t;
 188     }
 189     return *this;
 190   }
 191
 192   const T& getData() const {
 193     if(__CVC4_USE_STATISTICS) {
 194       return d_data;
 195     } else {
 196       Unreachable();
 197     }
 198   }
 199 };/* class BackedStat */
 200
 201
 202 class IntStat : public BackedStat<int64_t> {
 203 public:
 204
 205   IntStat(const std::string& s, int64_t init): BackedStat<int64_t>(s, init)
 206   {}
 207
 208   IntStat& operator++() {
 209     if(__CVC4_USE_STATISTICS) {
 210       ++d_data;
 211     }
 212     return *this;
 213   }
 214
 215   IntStat& operator+=(int64_t val) {
 216     if(__CVC4_USE_STATISTICS) {
 217       d_data+= val;
 218     }
 219     return *this;
 220   }
 221
 222   void maxAssign(int64_t val) {
 223     if(__CVC4_USE_STATISTICS) {
 224       if(d_data < val) {
 225         d_data = val;
 226       }
 227     }
 228   }
 229
 230   void minAssign(int64_t val) {
 231     if(__CVC4_USE_STATISTICS) {
 232       if(d_data > val) {
 233         d_data = val;
 234       }
 235     }
 236   }
 237 };/* class IntStat */
 238
 239
 240 // some utility functions for ::timespec
 241 inline ::timespec& operator+=(::timespec& a, const ::timespec& b) {
 242   // assumes a.tv_nsec and b.tv_nsec are in range
 243   const long nsec_per_sec = 1000000000L; // one thousand million
 244   a.tv_sec += b.tv_sec;
 245   long nsec = a.tv_nsec + b.tv_nsec;
 246   while(nsec < 0) {
 247     nsec += nsec_per_sec;
 248     ++a.tv_sec;
 249   }
 250   while(nsec >= nsec_per_sec) {
 251     nsec -= nsec_per_sec;
 252     --a.tv_sec;
 253   }
 254   a.tv_nsec = nsec;
 255   return a;
 256 }
 257 inline ::timespec& operator-=(::timespec& a, const ::timespec& b) {
 258   // assumes a.tv_nsec and b.tv_nsec are in range
 259   const long nsec_per_sec = 1000000000L; // one thousand million
 260   a.tv_sec -= b.tv_sec;
 261   long nsec = a.tv_nsec - b.tv_nsec;
 262   while(nsec < 0) {
 263     nsec += nsec_per_sec;
 264     ++a.tv_sec;
 265   }
 266   while(nsec >= nsec_per_sec) {
 267     nsec -= nsec_per_sec;
 268     --a.tv_sec;
 269   }
 270   a.tv_nsec = nsec;
 271   return a;
 272 }
 273 inline ::timespec operator+(const ::timespec& a, const ::timespec& b) {
 274   ::timespec result = a;
 275   return result += b;
 276 }
 277 inline ::timespec operator-(const ::timespec& a, const ::timespec& b) {
 278   ::timespec result = a;
 279   return result -= b;
 280 }
 281 inline bool operator==(const ::timespec& a, const ::timespec& b) {
 282   // assumes a.tv_nsec and b.tv_nsec are in range
 283   return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec;
 284 }
 285 inline bool operator!=(const ::timespec& a, const ::timespec& b) {
 286   // assumes a.tv_nsec and b.tv_nsec are in range
 287   return !(a == b);
 288 }
 289 inline bool operator<(const ::timespec& a, const ::timespec& b) {
 290   // assumes a.tv_nsec and b.tv_nsec are in range
 291   return a.tv_sec < b.tv_sec ||
 292     (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec);
 293 }
 294 inline bool operator>(const ::timespec& a, const ::timespec& b) {
 295   // assumes a.tv_nsec and b.tv_nsec are in range
 296   return a.tv_sec > b.tv_sec ||
 297     (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec);
 298 }
 299 inline bool operator<=(const ::timespec& a, const ::timespec& b) {
 300   // assumes a.tv_nsec and b.tv_nsec are in range
 301   return !(a > b);
 302 }
 303 inline bool operator>=(const ::timespec& a, const ::timespec& b) {
 304   // assumes a.tv_nsec and b.tv_nsec are in range
 305   return !(a < b);
 306 }
 307 inline std::ostream& operator<<(std::ostream& os, const ::timespec& t) {
 308   // assumes t.tv_nsec is in range
 309   return os << t.tv_sec << "."
 310             << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec;
 311 }
 312
 313
 314 class TimerStat : public BackedStat< ::timespec > {
 315   // strange: timespec isn't placed in 'std' namespace ?!
 316   ::timespec d_start;
 317   bool d_running;
 318
 319 public:
 320
 321   TimerStat(const std::string& s) :
 322     BackedStat< ::timespec >(s, ::timespec()),
 323     d_running(false) {
 324   }
 325
 326   void start() {
 327     if(__CVC4_USE_STATISTICS) {
 328       AlwaysAssert(!d_running);
 329       clock_gettime(CLOCK_MONOTONIC, &d_start);
 330       d_running = true;
 331     }
 332   }
 333
 334   void stop() {
 335     if(__CVC4_USE_STATISTICS) {
 336       AlwaysAssert(d_running);
 337       ::timespec end;
 338       clock_gettime(CLOCK_MONOTONIC, &end);
 339       d_data += end - d_start;
 340       d_running = false;
 341     }
 342   }
 343 };/* class TimerStat */
 344
 345
 346 #undef __CVC4_USE_STATISTICS
 347
 348 }/* CVC4 namespace */
 349
 350 #endif /* __CVC4__STATS_H */