src/util/stats.h

   1 /*********************                                                        */
   2 /*! \file stats.h
   3  ** \verbatim
   4  ** Original author: taking
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): mdeters
   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 <set>
  28 #include "util/Assert.h"
  29
  30 namespace CVC4 {
  31
  32
  33 #ifdef CVC4_STATISTICS_ON
  34 #  define USE_STATISTICS true
  35 #else
  36 #  define USE_STATISTICS false
  37 #endif
  38
  39 class CVC4_PUBLIC Stat;
  40
  41 class CVC4_PUBLIC StatisticsRegistry {
  42 private:
  43   struct StatCmp;
  44
  45   typedef std::set< Stat*, StatCmp > StatSet;
  46   static StatSet d_registeredStats;
  47
  48 public:
  49   static void flushStatistics(std::ostream& out);
  50
  51   static inline void registerStat(Stat* s) throw (AssertionException);
  52   static inline void unregisterStat(Stat* s) throw (AssertionException);
  53 };/* class StatisticsRegistry */
  54
  55
  56 class CVC4_PUBLIC Stat {
  57 private:
  58   std::string d_name;
  59
  60   static std::string s_delim;
  61
  62 public:
  63
  64   Stat(const std::string& s) throw (CVC4::AssertionException) : d_name(s)
  65   {
  66     if(USE_STATISTICS){
  67       AlwaysAssert(d_name.find(s_delim) == std::string::npos);
  68     }
  69   }
  70   virtual ~Stat() {}
  71
  72   virtual void flushInformation(std::ostream& out) const = 0;
  73
  74   void flushStat(std::ostream& out) const{
  75     if(USE_STATISTICS){
  76       out << d_name << s_delim;
  77       flushInformation(out);
  78     }
  79   }
  80
  81   const std::string& getName() const {
  82     return d_name;
  83   }
  84 };
  85
  86 struct StatisticsRegistry::StatCmp {
  87   bool operator()(const Stat* s1, const Stat* s2) const
  88   {
  89     return (s1->getName()) < (s2->getName());
  90   }
  91 };
  92
  93 inline void StatisticsRegistry::registerStat(Stat* s) throw (AssertionException){
  94   if(USE_STATISTICS){
  95     AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end());
  96     d_registeredStats.insert(s);
  97   }
  98 }
  99 inline void StatisticsRegistry::unregisterStat(Stat* s) throw (AssertionException){
 100   if(USE_STATISTICS){
 101     AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end());
 102     d_registeredStats.erase(s);
 103   }
 104 }
 105
 106
 107
 108 /**
 109  * class T must have stream insertion operation defined.
 110  * std::ostream& operator<<(std::ostream&, const T&);
 111  */
 112 template<class T>
 113 class DataStat : public Stat{
 114 public:
 115   DataStat(const std::string& s) : Stat(s) {}
 116
 117   virtual const T& getData() const = 0;
 118   virtual void setData(const T&) = 0;
 119
 120   void flushInformation(std::ostream& out) const{
 121     if(USE_STATISTICS){
 122       out << getData();
 123     }
 124   }
 125 };
 126
 127 /** T must have an assignment operator=(). */
 128 template <class T>
 129 class ReferenceStat: public DataStat<T>{
 130 private:
 131   const T* d_data;
 132
 133 public:
 134   ReferenceStat(const std::string& s):
 135     DataStat<T>(s), d_data(NULL)
 136   {}
 137
 138   ReferenceStat(const std::string& s, const T& data):
 139     DataStat<T>(s),d_data(NULL)
 140   {
 141     setData(data);
 142   }
 143
 144   void setData(const T& t){
 145     if(USE_STATISTICS){
 146       d_data = &t;
 147     }
 148   }
 149   const T& getData() const{
 150     if(USE_STATISTICS){
 151       return *d_data;
 152     }else{
 153       Unreachable();
 154     }
 155   }
 156 };
 157
 158 /** T must have an operator=() and a copy constructor. */
 159 template <class T>
 160 class BackedStat: public DataStat<T>{
 161 protected:
 162   T d_data;
 163
 164 public:
 165
 166   BackedStat(const std::string& s, const T& init): DataStat<T>(s), d_data(init)
 167   {}
 168
 169   void setData(const T& t) {
 170     if(USE_STATISTICS){
 171       d_data = t;
 172     }
 173   }
 174
 175   BackedStat<T>& operator=(const T& t){
 176     if(USE_STATISTICS){
 177       d_data = t;
 178     }
 179     return *this;
 180   }
 181
 182   const T& getData() const{
 183     if(USE_STATISTICS){
 184       return d_data;
 185     }else{
 186       Unreachable();
 187     }
 188   }
 189 };
 190
 191 class IntStat : public BackedStat<int64_t>{
 192 public:
 193
 194   IntStat(const std::string& s, int64_t init): BackedStat<int64_t>(s, init)
 195   {}
 196
 197   IntStat& operator++(){
 198     if(USE_STATISTICS){
 199       ++d_data;
 200     }
 201     return *this;
 202   }
 203
 204   IntStat& operator+=(int64_t val){
 205     if(USE_STATISTICS){
 206       d_data+= val;
 207     }
 208     return *this;
 209   }
 210
 211   void maxAssign(int64_t val){
 212     if(USE_STATISTICS){
 213       if(d_data < val){
 214         d_data = val;
 215       }
 216     }
 217   }
 218
 219   void minAssign(int64_t val){
 220     if(USE_STATISTICS){
 221       if(d_data > val){
 222         d_data = val;
 223       }
 224     }
 225   }
 226 };
 227
 228 #undef USE_STATISTICS
 229
 230 }/* CVC4 namespace */
 231
 232 #endif /* __CVC4__STATS_H */