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