First refactoring of statistics classes (#6105)

This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.

Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.

1 files changed, 0 insertions, 165 deletions

diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index e169d8745..b439daba8 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -36,124 +36,6 @@
 /****************************************************************************/
 namespace CVC4 {
 
-/** Compute the sum of two timespecs. */
-inline timespec& operator+=(timespec& a, const timespec& b) {
-  using namespace CVC4;
-  // assumes a.tv_nsec and b.tv_nsec are in range
-  const long nsec_per_sec = 1000000000L; // one thousand million
-  CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
-  CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
-  a.tv_sec += b.tv_sec;
-  long nsec = a.tv_nsec + b.tv_nsec;
-  Assert(nsec >= 0);
-  if(nsec < 0) {
-    nsec += nsec_per_sec;
-    --a.tv_sec;
-  }
-  if(nsec >= nsec_per_sec) {
-    nsec -= nsec_per_sec;
-    ++a.tv_sec;
-  }
-  Assert(nsec >= 0 && nsec < nsec_per_sec);
-  a.tv_nsec = nsec;
-  return a;
-}
-
-/** Compute the difference of two timespecs. */
-inline timespec& operator-=(timespec& a, const timespec& b) {
-  using namespace CVC4;
-  // assumes a.tv_nsec and b.tv_nsec are in range
-  const long nsec_per_sec = 1000000000L; // one thousand million
-  CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
-  CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
-  a.tv_sec -= b.tv_sec;
-  long nsec = a.tv_nsec - b.tv_nsec;
-  if(nsec < 0) {
-    nsec += nsec_per_sec;
-    --a.tv_sec;
-  }
-  if(nsec >= nsec_per_sec) {
-    nsec -= nsec_per_sec;
-    ++a.tv_sec;
-  }
-  Assert(nsec >= 0 && nsec < nsec_per_sec);
-  a.tv_nsec = nsec;
-  return a;
-}
-
-/** Add two timespecs. */
-inline timespec operator+(const timespec& a, const timespec& b) {
-  timespec result = a;
-  return result += b;
-}
-
-/** Subtract two timespecs. */
-inline timespec operator-(const timespec& a, const timespec& b) {
-  timespec result = a;
-  return result -= b;
-}
-
-/**
- * Compare two timespecs for equality.
- * This must be kept in sync with the copy in test/util/stats_black.h
- */
-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;
-}
-
-/** Compare two timespecs for disequality. */
-inline bool operator!=(const timespec& a, const timespec& b) {
-  // assumes a.tv_nsec and b.tv_nsec are in range
-  return !(a == b);
-}
-
-/** Compare two timespecs, returning true iff 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);
-}
-
-/** Compare two timespecs, returning true iff 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);
-}
-
-/** Compare two timespecs, returning true iff 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);
-}
-
-/** Compare two timespecs, returning true iff 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);
-}
-
-/** Output a timespec on an output stream. */
-std::ostream& operator<<(std::ostream& os, const timespec& t) {
-  // assumes t.tv_nsec is in range
-  StreamFormatScope format_scope(os);
-  return os << t.tv_sec << "."
-            << std::setfill('0') << std::setw(9) << std::right << t.tv_nsec;
-}
-
-
-/** Construct a statistics registry */
-StatisticsRegistry::StatisticsRegistry(const std::string& name) : Stat(name)
-{
-  d_prefix = name;
-  if(CVC4_USE_STATISTICS) {
-    PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
-                        "StatisticsRegistry names cannot contain the string \"%s\"",
-                    s_regDelim.c_str());
-  }
-}
-
 void StatisticsRegistry::registerStat(Stat* s)
 {
 #ifdef CVC4_STATISTICS_ON
@@ -194,51 +76,6 @@ void StatisticsRegistry::safeFlushInformation(int fd) const {
 #endif /* CVC4_STATISTICS_ON */
 }
 
-void TimerStat::start() {
-  if(CVC4_USE_STATISTICS) {
-    PrettyCheckArgument(!d_running, *this, "timer already running");
-    clock_gettime(CLOCK_MONOTONIC, &d_start);
-    d_running = true;
-  }
-}/* TimerStat::start() */
-
-void TimerStat::stop() {
-  if(CVC4_USE_STATISTICS) {
-    AlwaysAssert(d_running) << "timer not running";
-    ::timespec end;
-    clock_gettime(CLOCK_MONOTONIC, &end);
-    d_data += end - d_start;
-    d_running = false;
-  }
-}/* TimerStat::stop() */
-
-bool TimerStat::running() const {
-  return d_running;
-}/* TimerStat::running() */
-
-timespec TimerStat::getData() const {
-  ::timespec data = d_data;
-  if(CVC4_USE_STATISTICS && d_running) {
-    ::timespec end;
-    clock_gettime(CLOCK_MONOTONIC, &end);
-    data += end - d_start;
-  }
-  return data;
-}
-
-SExpr TimerStat::getValue() const {
-  ::timespec data = d_data;
-  if(CVC4_USE_STATISTICS && d_running) {
-    ::timespec end;
-    clock_gettime(CLOCK_MONOTONIC, &end);
-    data += end - d_start;
-  }
-  std::stringstream ss;
-  ss << std::fixed << std::setprecision(8) << data;
-  return SExpr(Rational::fromDecimal(ss.str()));
-}/* TimerStat::getValue() */
-
-
 RegisterStatistic::RegisterStatistic(StatisticsRegistry* reg, Stat* stat)
     : d_reg(reg),
       d_stat(stat) {
@@ -253,5 +90,3 @@ RegisterStatistic::~RegisterStatistic() {
 }
 
 }/* CVC4 namespace */
-
-#undef CVC4_USE_STATISTICS