Removing StatisticsRegistry's static functions current() and registerStat().

- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit.
- Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor.
- The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit.
- The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope.
- Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead.
- The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h.
- Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added.
- Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang.
- Most of the really confusing ifdef's in util/statistics_registry.h are gone.

1 files changed, 245 insertions, 0 deletions

diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
new file mode 100644
index 000000000..c9051cc0e
--- /dev/null
+++ b/src/util/statistics_registry.cpp
@@ -0,0 +1,245 @@
+/*********************                                                        */
+/*! \file statistics_registry.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Kshitij Bansal, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "util/statistics_registry.h"
+
+#include "base/cvc4_assert.h"
+#include "lib/clock_gettime.h"
+
+
+#ifdef CVC4_STATISTICS_ON
+#  define __CVC4_USE_STATISTICS true
+#else
+#  define __CVC4_USE_STATISTICS false
+#endif
+
+
+/****************************************************************************/
+/* Some utility functions for timespec                                    */
+/****************************************************************************/
+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
+  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)
+  throw(CVC4::IllegalArgumentException) :
+  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) throw(CVC4::IllegalArgumentException) {
+#ifdef CVC4_STATISTICS_ON
+  PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s,
+                "Statistic `%s' was not registered with this registry.",
+                s->getName().c_str());
+  d_stats.insert(s);
+#endif /* CVC4_STATISTICS_ON */
+}/* StatisticsRegistry::registerStat_() */
+
+void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) {
+#ifdef CVC4_STATISTICS_ON
+  PrettyCheckArgument(d_stats.find(s) != d_stats.end(), s,
+                "Statistic `%s' was not registered with this registry.",
+                s->getName().c_str());
+  d_stats.erase(s);
+#endif /* CVC4_STATISTICS_ON */
+}/* StatisticsRegistry::unregisterStat_() */
+
+void StatisticsRegistry::flushStat(std::ostream &out) const {
+#ifdef CVC4_STATISTICS_ON
+  flushInformation(out);
+#endif /* CVC4_STATISTICS_ON */
+}
+
+void StatisticsRegistry::flushInformation(std::ostream &out) const {
+#ifdef CVC4_STATISTICS_ON
+  this->StatisticsBase::flushInformation(out);
+#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) {
+    PrettyCheckArgument(d_running, *this, "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) {
+  CheckArgument(reg != NULL, reg,
+                "You need to specify a statistics registry"
+                "on which to set the statistic");
+  d_reg->registerStat(d_stat);
+}
+
+RegisterStatistic::~RegisterStatistic() {
+  d_reg->unregisterStat(d_stat);
+}
+
+}/* CVC4 namespace */
+
+#undef __CVC4_USE_STATISTICS