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.

6 files changed, 1358 insertions, 0 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index d086e3068..e1c593243 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -49,6 +49,10 @@ libutil_la_SOURCES = \
 	sexpr.h \
 	smt2_quote_string.cpp \
 	smt2_quote_string.h \
+	statistics.cpp \
+	statistics.h \
+	statistics_registry.cpp \
+	statistics_registry.h \
 	subrange_bound.cpp \
 	subrange_bound.h \
 	tuple.h \
@@ -95,6 +99,7 @@ EXTRA_DIST = \
 	regexp.i \
 	result.i \
 	sexpr.i \
+	statistics.i \
 	subrange_bound.i \
 	tuple.i \
 	unsafe_interrupt_exception.i
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
new file mode 100644
index 000000000..371872454
--- /dev/null
+++ b/src/util/statistics.cpp
@@ -0,0 +1,134 @@
+/*********************                                                        */
+/*! \file statistics.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** 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.h"
+
+#include <typeinfo>
+
+#include "util/statistics_registry.h" // for details about class Stat
+
+
+namespace CVC4 {
+
+std::string StatisticsBase::s_regDelim("::");
+
+bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const {
+  return s1->getName() < s2->getName();
+}
+
+StatisticsBase::iterator::value_type StatisticsBase::iterator::operator*() const {
+  return std::make_pair((*d_it)->getName(), (*d_it)->getValue());
+}
+
+StatisticsBase::StatisticsBase() :
+  d_prefix(),
+  d_stats() {
+}
+
+StatisticsBase::StatisticsBase(const StatisticsBase& stats) :
+  d_prefix(stats.d_prefix),
+  d_stats() {
+}
+
+StatisticsBase& StatisticsBase::operator=(const StatisticsBase& stats) {
+  d_prefix = stats.d_prefix;
+  return *this;
+}
+
+void Statistics::copyFrom(const StatisticsBase& stats) {
+  // This is ugly, but otherwise we have to introduce a "friend" relation for
+  // Base to its derived class (really obnoxious).
+  StatSet::const_iterator i_begin = ((const Statistics*) &stats)->d_stats.begin();
+  StatSet::const_iterator i_end = ((const Statistics*) &stats)->d_stats.end();
+  for(StatSet::const_iterator i = i_begin; i != i_end; ++i) {
+    SExprStat* p = new SExprStat((*i)->getName(), (*i)->getValue());
+    d_stats.insert(p);
+  }
+}
+
+void Statistics::clear() {
+  for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
+    delete *i;
+  }
+  d_stats.clear();
+}
+
+Statistics::Statistics(const StatisticsBase& stats) :
+  StatisticsBase(stats) {
+  copyFrom(stats);
+}
+
+Statistics::Statistics(const Statistics& stats) :
+  StatisticsBase(stats) {
+  copyFrom(stats);
+}
+
+Statistics::~Statistics() {
+  clear();
+}
+
+Statistics& Statistics::operator=(const StatisticsBase& stats) {
+  clear();
+  this->StatisticsBase::operator=(stats);
+  copyFrom(stats);
+
+  return *this;
+}
+
+Statistics& Statistics::operator=(const Statistics& stats) {
+  return this->operator=((const StatisticsBase&)stats);
+}
+
+StatisticsBase::const_iterator StatisticsBase::begin() const {
+  return iterator(d_stats.begin());
+}
+
+StatisticsBase::const_iterator StatisticsBase::end() const {
+  return iterator(d_stats.end());
+}
+
+void StatisticsBase::flushInformation(std::ostream &out) const {
+#ifdef CVC4_STATISTICS_ON
+  for(StatSet::iterator i = d_stats.begin();
+      i != d_stats.end();
+      ++i) {
+    Stat* s = *i;
+    if(d_prefix != "") {
+      out << d_prefix << s_regDelim;
+    }
+    s->flushStat(out);
+    out << std::endl;
+  }
+#endif /* CVC4_STATISTICS_ON */
+}
+
+SExpr StatisticsBase::getStatistic(std::string name) const {
+  SExpr value;
+  IntStat s(name, 0);
+  StatSet::iterator i = d_stats.find(&s);
+  if(i != d_stats.end()) {
+    return (*i)->getValue();
+  } else {
+    return SExpr();
+  }
+}
+
+void StatisticsBase::setPrefix(const std::string& prefix) {
+  d_prefix = prefix;
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/statistics.h b/src/util/statistics.h
new file mode 100644
index 000000000..a0b6ed083
--- /dev/null
+++ b/src/util/statistics.h
@@ -0,0 +1,129 @@
+/*********************                                                        */
+/*! \file statistics.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** 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 "cvc4_public.h"
+
+#ifndef __CVC4__STATISTICS_H
+#define __CVC4__STATISTICS_H
+
+#include <iterator>
+#include <ostream>
+#include <set>
+#include <string>
+#include <utility>
+
+#include "util/sexpr.h"
+
+namespace CVC4 {
+
+class Stat;
+
+class CVC4_PUBLIC StatisticsBase {
+protected:
+
+  static std::string s_regDelim;
+
+  /** A helper class for comparing two statistics */
+  struct StatCmp {
+    bool operator()(const Stat* s1, const Stat* s2) const;
+  };/* struct StatisticsRegistry::StatCmp */
+
+  /** A type for a set of statistics */
+  typedef std::set< Stat*, StatCmp > StatSet;
+
+  std::string d_prefix;
+
+  /** The set of statistics in this object */
+  StatSet d_stats;
+
+  StatisticsBase();
+  StatisticsBase(const StatisticsBase& stats);
+  StatisticsBase& operator=(const StatisticsBase& stats);
+
+public:
+
+  virtual ~StatisticsBase() { }
+
+  class CVC4_PUBLIC iterator : public std::iterator< std::input_iterator_tag, std::pair<std::string, SExpr> > {
+    StatSet::iterator d_it;
+
+    iterator(StatSet::iterator it) : d_it(it) { }
+
+    friend class StatisticsBase;
+
+  public:
+    iterator() : d_it() { }
+    iterator(const iterator& it) : d_it(it.d_it) { }
+    value_type operator*() const;
+    iterator& operator++() { ++d_it; return *this; }
+    iterator operator++(int) { iterator old = *this; ++d_it; return old; }
+    bool operator==(const iterator& i) const { return d_it == i.d_it; }
+    bool operator!=(const iterator& i) const { return d_it != i.d_it; }
+  };/* class StatisticsBase::iterator */
+
+  /** An iterator type over a set of statistics. */
+  typedef iterator const_iterator;
+
+  /** Set the output prefix for this set of statistics. */
+  virtual void setPrefix(const std::string& prefix);
+
+  /** Flush all statistics to the given output stream. */
+  void flushInformation(std::ostream& out) const;
+
+  /** Get the value of a named statistic. */
+  SExpr getStatistic(std::string name) const;
+
+  /**
+   * Get an iterator to the beginning of the range of the set of
+   * statistics.
+   */
+  const_iterator begin() const;
+
+  /**
+   * Get an iterator to the end of the range of the set of statistics.
+   */
+  const_iterator end() const;
+
+};/* class StatisticsBase */
+
+class CVC4_PUBLIC Statistics : public StatisticsBase {
+  void clear();
+  void copyFrom(const StatisticsBase&);
+
+public:
+
+  /**
+   * Override the copy constructor to do a "deep" copy of statistics
+   * values.
+   */
+  Statistics(const StatisticsBase& stats);
+  Statistics(const Statistics& stats);
+
+  ~Statistics();
+
+  /**
+   * Override the assignment operator to do a "deep" copy of statistics
+   * values.
+   */
+  Statistics& operator=(const StatisticsBase& stats);
+  Statistics& operator=(const Statistics& stats);
+
+};/* class Statistics */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__STATISTICS_H */
diff --git a/src/util/statistics.i b/src/util/statistics.i
new file mode 100644
index 000000000..bd3a4eeb9
--- /dev/null
+++ b/src/util/statistics.i
@@ -0,0 +1,79 @@
+%{
+#include "util/statistics.h"
+
+#ifdef SWIGJAVA
+
+#include "bindings/java_iterator_adapter.h"
+#include "bindings/java_stream_adapters.h"
+
+#endif /* SWIGJAVA */
+%}
+
+%rename(assign) CVC4::Statistics::operator=(const StatisticsBase&);
+%rename(assign) CVC4::Statistics::operator=(const Statistics& stats);
+
+#ifdef SWIGJAVA
+
+// Instead of StatisticsBase::begin() and end(), create an
+// iterator() method on the Java side that returns a Java-style
+// Iterator.
+%ignore CVC4::StatisticsBase::begin();
+%ignore CVC4::StatisticsBase::end();
+%ignore CVC4::StatisticsBase::begin() const;
+%ignore CVC4::StatisticsBase::end() const;
+%extend CVC4::StatisticsBase {
+  CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> iterator() {
+    return CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>(*$self);
+  }
+}
+
+// StatisticsBase is "iterable" on the Java side
+%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable<Object[]>";
+
+// the JavaIteratorAdapter should not be public, and implements Iterator
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "java.util.Iterator<Object[]>";
+// add some functions to the Java side (do it here because there's no way to do these in C++)
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "
+  public void remove() {
+    throw new java.lang.UnsupportedOperationException();
+  }
+
+  public Object[] next() {
+    if(hasNext()) {
+      return getNext();
+    } else {
+      throw new java.util.NoSuchElementException();
+    }
+  }
+"
+// getNext() just allows C++ iterator access from Java-side next(), make it private
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>::getNext() "private";
+
+// map the types appropriately.  for statistics, the "payload" of the iterator is an Object[].
+// These Object arrays are always of two elements, the first is a String and the second an
+// SExpr.  (On the C++ side, it is a std::pair<std::string, SExpr>.)
+%typemap(jni) CVC4::StatisticsBase::const_iterator::value_type "jobjectArray";
+%typemap(jtype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]";
+%typemap(jstype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]";
+%typemap(javaout) CVC4::StatisticsBase::const_iterator::value_type { return $jnicall; }
+%typemap(out) CVC4::StatisticsBase::const_iterator::value_type {
+      $result = jenv->NewObjectArray(2, jenv->FindClass("java/lang/Object"), $null);
+      jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str()));
+      jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/SExpr");
+      jmethodID methodid = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
+      jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(new CVC4::SExpr($1.second)), true));
+    };
+
+#endif /* SWIGJAVA */
+
+%include "util/statistics.h"
+
+#ifdef SWIGJAVA
+
+%include "bindings/java_iterator_adapter.h"
+%include "bindings/java_stream_adapters.h"
+
+%template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>;
+
+#endif /* SWIGJAVA */
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
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
new file mode 100644
index 000000000..f4f00e444
--- /dev/null
+++ b/src/util/statistics_registry.h
@@ -0,0 +1,766 @@
+/*********************                                                        */
+/*! \file statistics_registry.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: Tim King
+ ** Minor contributors (to current version): Kshitij Bansal
+ ** 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 Statistics utility classes
+ **
+ ** Statistics utility classes, including classes for holding (and referring
+ ** to) statistics, the statistics registry, and some other associated
+ ** classes.
+ **
+ ** This file is somewhat unique in that it is a "cvc4_private_library.h"
+ ** header. Because of this, most classes need to be marked as CVC4_PUBLIC.
+ ** This is because CVC4_PUBLIC is connected to the visibility of the linkage
+ ** in the object files for the class. It does not dictate what headers are
+ ** installed.
+ ** Because the StatisticsRegistry and associated classes are built into
+ ** libutil, which is used by libcvc4, and then later used by the libmain
+ ** without referring to libutil as well. Thus the without marking these as
+ ** CVC4_PUBLIC the symbols would be external in libutil, internal in libcvc4,
+ ** and not be visible to libmain and linking would fail.
+ ** You can debug this using "nm" on the .so and .o files in the builds/
+ ** directory. See
+ ** http://eli.thegreenplace.net/2013/07/09/library-order-in-static-linking
+ ** for a longer discussion on symbol visibility.
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef __CVC4__STATISTICS_REGISTRY_H
+#define __CVC4__STATISTICS_REGISTRY_H
+
+#include <stdint.h>
+
+#include <cassert>
+#include <ctime>
+#include <iomanip>
+#include <map>
+#include <sstream>
+#include <vector>
+
+#include "base/exception.h"
+#include "lib/clock_gettime.h"
+#include "util/statistics.h"
+
+namespace CVC4 {
+
+/**
+ * Prints a timespec.
+ *
+ * This is used in the implementation of TimerStat. This needs to be available
+ * before Stat due to ordering constraints in clang for TimerStat.
+ */
+std::ostream& operator<<(std::ostream& os, const timespec& t) CVC4_PUBLIC;
+
+#ifdef CVC4_STATISTICS_ON
+#  define __CVC4_USE_STATISTICS true
+#else
+#  define __CVC4_USE_STATISTICS false
+#endif
+
+
+/**
+ * The base class for all statistics.
+ *
+ * This base class keeps the name of the statistic and declares the (pure)
+ * virtual function flushInformation().  Derived classes must implement
+ * this function and pass their name to the base class constructor.
+ *
+ * This class also (statically) maintains the delimiter used to separate
+ * the name and the value when statistics are output.
+ */
+class Stat {
+protected:
+  /** The name of this statistic */
+  std::string d_name;
+
+public:
+
+  /** Nullary constructor, does nothing */
+  Stat() { }
+
+  /**
+   * Construct a statistic with the given name.  Debug builds of CVC4
+   * will throw an assertion exception if the given name contains the
+   * statistic delimiter string.
+   */
+  Stat(const std::string& name) throw(CVC4::IllegalArgumentException) :
+    d_name(name) {
+    if(__CVC4_USE_STATISTICS) {
+      CheckArgument(d_name.find(", ") == std::string::npos, name,
+                    "Statistics names cannot include a comma (',')");
+    }
+  }
+
+  /** Destruct a statistic.  This base-class version does nothing. */
+  virtual ~Stat() {}
+
+  /**
+   * Flush the value of this statistic to an output stream.  Should
+   * finish the output with an end-of-line character.
+   */
+  virtual void flushInformation(std::ostream& out) const = 0;
+
+  /**
+   * Flush the name,value pair of this statistic to an output stream.
+   * Uses the statistic delimiter string between name and value.
+   *
+   * May be redefined by a child class
+   */
+  virtual void flushStat(std::ostream& out) const {
+    if(__CVC4_USE_STATISTICS) {
+      out << d_name << ", ";
+      flushInformation(out);
+    }
+  }
+
+  /** Get the name of this statistic. */
+  const std::string& getName() const {
+    return d_name;
+  }
+
+  /** Get the value of this statistic as a string. */
+  virtual SExpr getValue() const {
+    std::stringstream ss;
+    flushInformation(ss);
+    return SExpr(ss.str());
+  }
+
+};/* class Stat */
+
+// A generic way of making a SExpr from templated stats code.
+// for example, the uint64_t version ensures that we create
+// Integer-SExprs for ReadOnlyDataStats (like those inside
+// Minisat) without having to specialize the entire
+// ReadOnlyDataStat class template.
+template <class T>
+inline SExpr mkSExpr(const T& x) {
+  std::stringstream ss;
+  ss << x;
+  return SExpr(ss.str());
+}
+
+template <>
+inline SExpr mkSExpr(const uint64_t& x) {
+  return SExpr(Integer(x));
+}
+
+template <>
+inline SExpr mkSExpr(const int64_t& x) {
+  return SExpr(Integer(x));
+}
+
+template <>
+inline SExpr mkSExpr(const int& x) {
+  return SExpr(Integer(x));
+}
+
+template <>
+inline SExpr mkSExpr(const Integer& x) {
+  return SExpr(x);
+}
+
+template <>
+inline SExpr mkSExpr(const double& x) {
+  // roundabout way to get a Rational from a double
+  std::stringstream ss;
+  ss << std::fixed << std::setprecision(8) << x;
+  return SExpr(Rational::fromDecimal(ss.str()));
+}
+
+template <>
+inline SExpr mkSExpr(const Rational& x) {
+  return SExpr(x);
+}
+
+/**
+ * A class to represent a "read-only" data statistic of type T.  Adds to
+ * the Stat base class the pure virtual function getData(), which returns
+ * type T, and flushInformation(), which outputs the statistic value to an
+ * output stream (using the same existing stream insertion operator).
+ *
+ * Template class T must have stream insertion operation defined:
+ * std::ostream& operator<<(std::ostream&, const T&)
+ */
+template <class T>
+class ReadOnlyDataStat : public Stat {
+public:
+  /** The "payload" type of this data statistic (that is, T). */
+  typedef T payload_t;
+
+  /** Construct a read-only data statistic with the given name. */
+  ReadOnlyDataStat(const std::string& name) :
+    Stat(name) {
+  }
+
+  /** Get the value of the statistic. */
+  virtual T getData() const = 0;
+
+  /** Flush the value of the statistic to the given output stream. */
+  void flushInformation(std::ostream& out) const {
+    if(__CVC4_USE_STATISTICS) {
+      out << getData();
+    }
+  }
+
+  SExpr getValue() const {
+    return mkSExpr(getData());
+  }
+
+};/* class ReadOnlyDataStat<T> */
+
+
+/**
+ * A data statistic class.  This class extends a read-only data statistic
+ * with assignment (the statistic can be set as well as read).  This class
+ * adds to the read-only case a pure virtual function setData(), thus
+ * providing the basic interface for a data statistic: getData() to get the
+ * statistic value, and setData() to set it.
+ *
+ * As with the read-only data statistic class, template class T must have
+ * stream insertion operation defined:
+ * std::ostream& operator<<(std::ostream&, const T&)
+ */
+template <class T>
+class DataStat : public ReadOnlyDataStat<T> {
+public:
+
+  /** Construct a data statistic with the given name. */
+  DataStat(const std::string& name) :
+    ReadOnlyDataStat<T>(name) {
+  }
+
+  /** Set the data statistic. */
+  virtual void setData(const T&) = 0;
+
+};/* class DataStat<T> */
+
+
+/**
+ * A data statistic that references a data cell of type T,
+ * implementing getData() by referencing that memory cell, and
+ * setData() by reassigning the statistic to point to the new
+ * data cell.  The referenced data cell is kept as a const
+ * reference, meaning the referenced data is never actually
+ * modified by this class (it must be externally modified for
+ * a reference statistic to make sense).  A common use for
+ * this type of statistic is to output a statistic that is kept
+ * outside the statistics package (for example, one that's kept
+ * by a theory implementation for internal heuristic purposes,
+ * which is important to keep even if statistics are turned off).
+ *
+ * Template class T must have an assignment operator=().
+ */
+template <class T>
+class ReferenceStat : public DataStat<T> {
+private:
+  /** The referenced data cell */
+  const T* d_data;
+
+public:
+  /**
+   * Construct a reference stat with the given name and a reference
+   * to NULL.
+   */
+  ReferenceStat(const std::string& name) :
+    DataStat<T>(name),
+    d_data(NULL) {
+  }
+
+  /**
+   * Construct a reference stat with the given name and a reference to
+   * the given data.
+   */
+  ReferenceStat(const std::string& name, const T& data) :
+    DataStat<T>(name),
+    d_data(NULL) {
+    setData(data);
+  }
+
+  /** Set this reference statistic to refer to the given data cell. */
+  void setData(const T& t) {
+    if(__CVC4_USE_STATISTICS) {
+      d_data = &t;
+    }
+  }
+
+  /** Get the value of the referenced data cell. */
+  T getData() const {
+    return *d_data;
+  }
+
+};/* class ReferenceStat<T> */
+
+
+/**
+ * A data statistic that keeps a T and sets it with setData().
+ *
+ * Template class T must have an operator=() and a copy constructor.
+ */
+template <class T>
+class BackedStat : public DataStat<T> {
+protected:
+  /** The internally-kept statistic value */
+  T d_data;
+
+public:
+
+  /** Construct a backed statistic with the given name and initial value. */
+  BackedStat(const std::string& name, const T& init) :
+    DataStat<T>(name),
+    d_data(init) {
+  }
+
+  /** Set the underlying data value to the given value. */
+  void setData(const T& t) {
+    if(__CVC4_USE_STATISTICS) {
+      d_data = t;
+    }
+  }
+
+  /** Identical to setData(). */
+  BackedStat<T>& operator=(const T& t) {
+    if(__CVC4_USE_STATISTICS) {
+      d_data = t;
+    }
+    return *this;
+  }
+
+  /** Get the underlying data value. */
+  T getData() const {
+    return d_data;
+  }
+
+};/* class BackedStat<T> */
+
+
+/**
+ * A wrapper Stat for another Stat.
+ *
+ * This type of Stat is useful in cases where a module (like the
+ * CongruenceClosure module) might keep its own statistics, but might
+ * be instantiated in many contexts by many clients.  This makes such
+ * a statistic inappopriate to register with the StatisticsRegistry
+ * directly, as all would be output with the same name (and may be
+ * unregistered too quickly anyway).  A WrappedStat allows the calling
+ * client (say, TheoryUF) to wrap the Stat from the client module,
+ * giving it a globally unique name.
+ */
+template <class Stat>
+class WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> {
+  typedef typename Stat::payload_t T;
+
+  const ReadOnlyDataStat<T>& d_stat;
+
+  /** Private copy constructor undefined (no copy permitted). */
+  WrappedStat(const WrappedStat&) CVC4_UNDEFINED;
+  /** Private assignment operator undefined (no copy permitted). */
+  WrappedStat<T>& operator=(const WrappedStat&) CVC4_UNDEFINED;
+
+public:
+
+  /**
+   * Construct a wrapped statistic with the given name that wraps the
+   * given statistic.
+   */
+  WrappedStat(const std::string& name, const ReadOnlyDataStat<T>& stat) :
+    ReadOnlyDataStat<T>(name),
+    d_stat(stat) {
+  }
+
+  /** Get the data of the underlying (wrapped) statistic. */
+  T getData() const {
+    return d_stat.getData();
+  }
+
+  SExpr getValue() const {
+    return d_stat.getValue();
+  }
+
+};/* class WrappedStat<T> */
+
+/**
+ * A backed integer-valued (64-bit signed) statistic.
+ * This doesn't functionally differ from its base class BackedStat<int64_t>,
+ * except for adding convenience functions for dealing with integers.
+ */
+class IntStat : public BackedStat<int64_t> {
+public:
+
+  /**
+   * Construct an integer-valued statistic with the given name and
+   * initial value.
+   */
+  IntStat(const std::string& name, int64_t init) :
+    BackedStat<int64_t>(name, init) {
+  }
+
+  /** Increment the underlying integer statistic. */
+  IntStat& operator++() {
+    if(__CVC4_USE_STATISTICS) {
+      ++d_data;
+    }
+    return *this;
+  }
+
+  /** Increment the underlying integer statistic by the given amount. */
+  IntStat& operator+=(int64_t val) {
+    if(__CVC4_USE_STATISTICS) {
+      d_data += val;
+    }
+    return *this;
+  }
+
+  /** Keep the maximum of the current statistic value and the given one. */
+  void maxAssign(int64_t val) {
+    if(__CVC4_USE_STATISTICS) {
+      if(d_data < val) {
+        d_data = val;
+      }
+    }
+  }
+
+  /** Keep the minimum of the current statistic value and the given one. */
+  void minAssign(int64_t val) {
+    if(__CVC4_USE_STATISTICS) {
+      if(d_data > val) {
+        d_data = val;
+      }
+    }
+  }
+
+  SExpr getValue() const {
+    return SExpr(Integer(d_data));
+  }
+
+};/* class IntStat */
+
+template <class T>
+class SizeStat : public Stat {
+private:
+  const T& d_sized;
+public:
+  SizeStat(const std::string&name, const T& sized) :
+    Stat(name), d_sized(sized) {}
+  ~SizeStat() {}
+
+  void flushInformation(std::ostream& out) const {
+    out << d_sized.size();
+  }
+
+  SExpr getValue() const {
+    return SExpr(Integer(d_sized.size()));
+  }
+
+};/* class SizeStat */
+
+/**
+ * The value for an AverageStat is the running average of (e1, e_2, ..., e_n),
+ *   (e1 + e_2 + ... + e_n)/n,
+ * where e_i is an entry added by an addEntry(e_i) call.
+ * The value is initially always 0.
+ * (This is to avoid making parsers confused.)
+ *
+ * A call to setData() will change the running average but not reset the
+ * running count, so should generally be avoided.  Call addEntry() to add
+ * an entry to the average calculation.
+ */
+class AverageStat : public BackedStat<double> {
+private:
+  /**
+   * The number of accumulations of the running average that we
+   * have seen so far.
+   */
+  uint32_t d_count;
+  double d_sum;
+
+public:
+  /** Construct an average statistic with the given name. */
+  AverageStat(const std::string& name) :
+    BackedStat<double>(name, 0.0), d_count(0), d_sum(0.0) {
+  }
+
+  /** Add an entry to the running-average calculation. */
+  void addEntry(double e) {
+    if(__CVC4_USE_STATISTICS) {
+      ++d_count;
+      d_sum += e;
+      setData(d_sum / d_count);
+    }
+  }
+
+  SExpr getValue() const {
+    std::stringstream ss;
+    ss << std::fixed << std::setprecision(8) << d_data;
+    return SExpr(Rational::fromDecimal(ss.str()));
+  }
+
+};/* class AverageStat */
+
+/** A statistic that contains a SExpr. */
+class SExprStat : public Stat {
+private:
+  SExpr d_data;
+
+public:
+
+  /**
+   * Construct a SExpr-valued statistic with the given name and
+   * initial value.
+   */
+  SExprStat(const std::string& name, const SExpr& init) :
+    Stat(name), d_data(init){}
+
+  virtual void flushInformation(std::ostream& out) const {
+    out << d_data << std::endl;
+  }
+
+  SExpr getValue() const {
+    return d_data;
+  }
+
+};/* class SExprStat */
+
+template <class T>
+class ListStat : public Stat {
+private:
+  typedef std::vector<T> List;
+  List d_list;
+public:
+
+  /**
+   * Construct an integer-valued statistic with the given name and
+   * initial value.
+   */
+  ListStat(const std::string& name) : Stat(name) {}
+  ~ListStat() {}
+
+  void flushInformation(std::ostream& out) const{
+    if(__CVC4_USE_STATISTICS) {
+      typename List::const_iterator i = d_list.begin(), end =  d_list.end();
+      out << "[";
+      if(i != end){
+        out << *i;
+        ++i;
+        for(; i != end; ++i){
+          out << ", " << *i;
+        }
+      }
+      out << "]";
+    }
+  }
+
+  ListStat& operator<<(const T& val){
+    if(__CVC4_USE_STATISTICS) {
+      d_list.push_back(val);
+    }
+    return (*this);
+  }
+
+};/* class ListStat */
+
+template <class T>
+class HistogramStat : public Stat {
+private:
+  typedef std::map<T, unsigned int> Histogram;
+  Histogram d_hist;
+public:
+
+  /** Construct a histogram of a stream of entries. */
+  HistogramStat(const std::string& name) : Stat(name) {}
+  ~HistogramStat() {}
+
+  void flushInformation(std::ostream& out) const{
+    if(__CVC4_USE_STATISTICS) {
+      typename Histogram::const_iterator i = d_hist.begin();
+      typename Histogram::const_iterator end =  d_hist.end();
+      out << "[";
+      while(i != end){
+        const T& key = (*i).first;
+        unsigned int count = (*i).second;
+        out << "("<<key<<" : "<<count<< ")";
+        ++i;
+        if(i != end){
+          out << ", ";
+        }
+      }
+      out << "]";
+    }
+  }
+
+  HistogramStat& operator<<(const T& val){
+    if(__CVC4_USE_STATISTICS) {
+      if(d_hist.find(val) == d_hist.end()){
+        d_hist.insert(std::make_pair(val,0));
+      }
+      d_hist[val]++;
+    }
+    return (*this);
+  }
+
+};/* class HistogramStat */
+
+/****************************************************************************/
+/* Statistics Registry                                                      */
+/****************************************************************************/
+
+/**
+ * The main statistics registry.  This registry maintains the list of
+ * currently active statistics and is able to "flush" them all.
+ */
+class CVC4_PUBLIC StatisticsRegistry : public StatisticsBase, public Stat {
+private:
+
+  /** Private copy constructor undefined (no copy permitted). */
+  StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED;
+
+public:
+
+  /** Construct an nameless statistics registry */
+  StatisticsRegistry() {}
+
+  /** Construct a statistics registry */
+  StatisticsRegistry(const std::string& name)
+    throw(CVC4::IllegalArgumentException);
+
+  /**
+   * Set the name of this statistic registry, used as prefix during
+   * output.  (This version overrides StatisticsBase::setPrefix().)
+   */
+  void setPrefix(const std::string& name) {
+    d_prefix = d_name = name;
+  }
+
+  /** Overridden to avoid the name being printed */
+  void flushStat(std::ostream &out) const;
+
+  virtual void flushInformation(std::ostream& out) const;
+
+  SExpr getValue() const {
+    std::vector<SExpr> v;
+    for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
+      std::vector<SExpr> w;
+      w.push_back(SExpr((*i)->getName()));
+      w.push_back((*i)->getValue());
+      v.push_back(SExpr(w));
+    }
+    return SExpr(v);
+  }
+
+  /** Register a new statistic */
+  void registerStat(Stat* s) throw(CVC4::IllegalArgumentException);
+
+  /** Unregister a new statistic */
+  void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException);
+
+};/* class StatisticsRegistry */
+
+class CodeTimer;
+
+/**
+ * A timer statistic.  The timer can be started and stopped
+ * arbitrarily, like a stopwatch; the value of the statistic at the
+ * end is the accumulated time over all (start,stop) pairs.
+ */
+class CVC4_PUBLIC TimerStat : public BackedStat<timespec> {
+
+  // strange: timespec isn't placed in 'std' namespace ?!
+  /** The last start time of this timer */
+  timespec d_start;
+
+  /** Whether this timer is currently running */
+  bool d_running;
+
+public:
+
+  typedef CVC4::CodeTimer CodeTimer;
+
+  /**
+   * Construct a timer statistic with the given name.  Newly-constructed
+   * timers have a 0.0 value and are not running.
+   */
+  TimerStat(const std::string& name) :
+    BackedStat< timespec >(name, timespec()),
+    d_running(false) {
+    /* timespec is POD and so may not be initialized to zero;
+     * here, ensure it is */
+    d_data.tv_sec = d_data.tv_nsec = 0;
+  }
+
+  /** Start the timer. */
+  void start();
+
+  /**
+   * Stop the timer and update the statistic value with the
+   * accumulated time.
+   */
+  void stop();
+
+  /** If the timer is currently running */
+  bool running() const;
+
+  timespec getData() const;
+
+  SExpr getValue() const;
+
+};/* class TimerStat */
+
+/**
+ * Utility class to make it easier to call stop() at the end of a
+ * code block.  When constructed, it starts the timer.  When
+ * destructed, it stops the timer.
+ */
+class CodeTimer {
+  TimerStat& d_timer;
+  bool d_reentrant;
+
+  /** Private copy constructor undefined (no copy permitted). */
+  CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED;
+  /** Private assignment operator undefined (no copy permitted). */
+  CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED;
+
+public:
+  CodeTimer(TimerStat& timer, bool allow_reentrant = false) : d_timer(timer), d_reentrant(false) {
+    if(!allow_reentrant || !(d_reentrant = d_timer.running())) {
+      d_timer.start();
+    }
+  }
+  ~CodeTimer() {
+    if(!d_reentrant) {
+      d_timer.stop();
+    }
+  }
+};/* class CodeTimer */
+
+/**
+ * Resource-acquisition-is-initialization idiom for statistics
+ * registry.  Useful for stack-based statistics (like in the driver).
+ * Generally, for statistics kept in a member field of class, it's
+ * better to use the above KEEP_STATISTIC(), which does declaration of
+ * the member, construction of the statistic, and
+ * registration/unregistration.  This RAII class only does
+ * registration and unregistration.
+ */
+class CVC4_PUBLIC RegisterStatistic {
+public:
+  RegisterStatistic(StatisticsRegistry* reg, Stat* stat);
+  ~RegisterStatistic();
+
+private:
+  StatisticsRegistry* d_reg;
+  Stat* d_stat;
+
+};/* class RegisterStatistic */
+
+#undef __CVC4_USE_STATISTICS
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__STATISTICS_REGISTRY_H */