src/util/statistics_registry.cpp

   1 /*********************                                                        */
   2 /*! \file statistics_registry.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King, Kshitij Bansal
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "util/statistics_registry.h"
  19
  20 #include <cstdlib>
  21 #include <iostream>
  22
  23 #include "base/check.h"
  24 #include "lib/clock_gettime.h"
  25 #include "util/ostream_util.h"
  26
  27 #ifdef CVC4_STATISTICS_ON
  28 #  define CVC4_USE_STATISTICS true
  29 #else
  30 #  define CVC4_USE_STATISTICS false
  31 #endif
  32
  33
  34 /****************************************************************************/
  35 /* Some utility functions for timespec                                    */
  36 /****************************************************************************/
  37 namespace CVC4 {
  38
  39 /** Compute the sum of two timespecs. */
  40 inline timespec& operator+=(timespec& a, const timespec& b) {
  41   using namespace CVC4;
  42   // assumes a.tv_nsec and b.tv_nsec are in range
  43   const long nsec_per_sec = 1000000000L; // one thousand million
  44   CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
  45   CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
  46   a.tv_sec += b.tv_sec;
  47   long nsec = a.tv_nsec + b.tv_nsec;
  48   Assert(nsec >= 0);
  49   if(nsec < 0) {
  50     nsec += nsec_per_sec;
  51     --a.tv_sec;
  52   }
  53   if(nsec >= nsec_per_sec) {
  54     nsec -= nsec_per_sec;
  55     ++a.tv_sec;
  56   }
  57   Assert(nsec >= 0 && nsec < nsec_per_sec);
  58   a.tv_nsec = nsec;
  59   return a;
  60 }
  61
  62 /** Compute the difference of two timespecs. */
  63 inline timespec& operator-=(timespec& a, const timespec& b) {
  64   using namespace CVC4;
  65   // assumes a.tv_nsec and b.tv_nsec are in range
  66   const long nsec_per_sec = 1000000000L; // one thousand million
  67   CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
  68   CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
  69   a.tv_sec -= b.tv_sec;
  70   long nsec = a.tv_nsec - b.tv_nsec;
  71   if(nsec < 0) {
  72     nsec += nsec_per_sec;
  73     --a.tv_sec;
  74   }
  75   if(nsec >= nsec_per_sec) {
  76     nsec -= nsec_per_sec;
  77     ++a.tv_sec;
  78   }
  79   Assert(nsec >= 0 && nsec < nsec_per_sec);
  80   a.tv_nsec = nsec;
  81   return a;
  82 }
  83
  84 /** Add two timespecs. */
  85 inline timespec operator+(const timespec& a, const timespec& b) {
  86   timespec result = a;
  87   return result += b;
  88 }
  89
  90 /** Subtract two timespecs. */
  91 inline timespec operator-(const timespec& a, const timespec& b) {
  92   timespec result = a;
  93   return result -= b;
  94 }
  95
  96 /**
  97  * Compare two timespecs for equality.
  98  * This must be kept in sync with the copy in test/util/stats_black.h
  99  */
 100 inline bool operator==(const timespec& a, const timespec& b) {
 101   // assumes a.tv_nsec and b.tv_nsec are in range
 102   return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec;
 103 }
 104
 105 /** Compare two timespecs for disequality. */
 106 inline bool operator!=(const timespec& a, const timespec& b) {
 107   // assumes a.tv_nsec and b.tv_nsec are in range
 108   return !(a == b);
 109 }
 110
 111 /** Compare two timespecs, returning true iff a < b. */
 112 inline bool operator<(const timespec& a, const timespec& b) {
 113   // assumes a.tv_nsec and b.tv_nsec are in range
 114   return a.tv_sec < b.tv_sec ||
 115     (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec);
 116 }
 117
 118 /** Compare two timespecs, returning true iff a > b. */
 119 inline bool operator>(const timespec& a, const timespec& b) {
 120   // assumes a.tv_nsec and b.tv_nsec are in range
 121   return a.tv_sec > b.tv_sec ||
 122     (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec);
 123 }
 124
 125 /** Compare two timespecs, returning true iff a <= b. */
 126 inline bool operator<=(const timespec& a, const timespec& b) {
 127   // assumes a.tv_nsec and b.tv_nsec are in range
 128   return !(a > b);
 129 }
 130
 131 /** Compare two timespecs, returning true iff a >= b. */
 132 inline bool operator>=(const timespec& a, const timespec& b) {
 133   // assumes a.tv_nsec and b.tv_nsec are in range
 134   return !(a < b);
 135 }
 136
 137 /** Output a timespec on an output stream. */
 138 std::ostream& operator<<(std::ostream& os, const timespec& t) {
 139   // assumes t.tv_nsec is in range
 140   StreamFormatScope format_scope(os);
 141   return os << t.tv_sec << "."
 142             << std::setfill('0') << std::setw(9) << std::right << t.tv_nsec;
 143 }
 144
 145
 146 /** Construct a statistics registry */
 147 StatisticsRegistry::StatisticsRegistry(const std::string& name) : Stat(name)
 148 {
 149   d_prefix = name;
 150   if(CVC4_USE_STATISTICS) {
 151     PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
 152                         "StatisticsRegistry names cannot contain the string \"%s\"",
 153                     s_regDelim.c_str());
 154   }
 155 }
 156
 157 void StatisticsRegistry::registerStat(Stat* s)
 158 {
 159 #ifdef CVC4_STATISTICS_ON
 160   PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s,
 161                 "Statistic `%s' was not registered with this registry.",
 162                 s->getName().c_str());
 163   d_stats.insert(s);
 164 #endif /* CVC4_STATISTICS_ON */
 165 }/* StatisticsRegistry::registerStat_() */
 166
 167 void StatisticsRegistry::unregisterStat(Stat* s)
 168 {
 169 #ifdef CVC4_STATISTICS_ON
 170   AlwaysAssert(s != nullptr);
 171   AlwaysAssert(d_stats.erase(s) > 0)
 172       << "Statistic `" << s->getName()
 173       << "' was not registered with this registry.";
 174 #endif /* CVC4_STATISTICS_ON */
 175 } /* StatisticsRegistry::unregisterStat() */
 176
 177 void StatisticsRegistry::flushStat(std::ostream &out) const {
 178 #ifdef CVC4_STATISTICS_ON
 179   flushInformation(out);
 180 #endif /* CVC4_STATISTICS_ON */
 181 }
 182
 183 void StatisticsRegistry::flushInformation(std::ostream &out) const {
 184 #ifdef CVC4_STATISTICS_ON
 185   this->StatisticsBase::flushInformation(out);
 186 #endif /* CVC4_STATISTICS_ON */
 187 }
 188
 189 void StatisticsRegistry::safeFlushInformation(int fd) const {
 190 #ifdef CVC4_STATISTICS_ON
 191   this->StatisticsBase::safeFlushInformation(fd);
 192 #endif /* CVC4_STATISTICS_ON */
 193 }
 194
 195 void TimerStat::start() {
 196   if(CVC4_USE_STATISTICS) {
 197     PrettyCheckArgument(!d_running, *this, "timer already running");
 198     clock_gettime(CLOCK_MONOTONIC, &d_start);
 199     d_running = true;
 200   }
 201 }/* TimerStat::start() */
 202
 203 void TimerStat::stop() {
 204   if(CVC4_USE_STATISTICS) {
 205     AlwaysAssert(d_running) << "timer not running";
 206     ::timespec end;
 207     clock_gettime(CLOCK_MONOTONIC, &end);
 208     d_data += end - d_start;
 209     d_running = false;
 210   }
 211 }/* TimerStat::stop() */
 212
 213 bool TimerStat::running() const {
 214   return d_running;
 215 }/* TimerStat::running() */
 216
 217 timespec TimerStat::getData() const {
 218   ::timespec data = d_data;
 219   if(CVC4_USE_STATISTICS && d_running) {
 220     ::timespec end;
 221     clock_gettime(CLOCK_MONOTONIC, &end);
 222     data += end - d_start;
 223   }
 224   return data;
 225 }
 226
 227 SExpr TimerStat::getValue() const {
 228   ::timespec data = d_data;
 229   if(CVC4_USE_STATISTICS && d_running) {
 230     ::timespec end;
 231     clock_gettime(CLOCK_MONOTONIC, &end);
 232     data += end - d_start;
 233   }
 234   std::stringstream ss;
 235   ss << std::fixed << std::setprecision(8) << data;
 236   return SExpr(Rational::fromDecimal(ss.str()));
 237 }/* TimerStat::getValue() */
 238
 239
 240 RegisterStatistic::RegisterStatistic(StatisticsRegistry* reg, Stat* stat)
 241     : d_reg(reg),
 242       d_stat(stat) {
 243   CheckArgument(reg != NULL, reg,
 244                 "You need to specify a statistics registry"
 245                 "on which to set the statistic");
 246   d_reg->registerStat(d_stat);
 247 }
 248
 249 RegisterStatistic::~RegisterStatistic() {
 250   d_reg->unregisterStat(d_stat);
 251 }
 252
 253 }/* CVC4 namespace */
 254
 255 #undef CVC4_USE_STATISTICS