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.

9 files changed, 7 insertions, 1477 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 5c046c282..4648ed3af 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -3,23 +3,10 @@ AM_CPPFLAGS = \
 	-I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
-#noinst_LTLIBRARIES = libexpr.la libstatistics.la
 noinst_LTLIBRARIES = libexpr.la
 
-# libstatistics_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) -D__BUILDING_STATISTICS_FOR_EXPORT
-# libstatistics_la_SOURCES = \
-# 	statistics_registry.h \
-# 	statistics_registry.cpp
-
-# EXTRA_libstatistics_la_DEPENDENCIES = \
-# 	builts
-
 # For some reason statistics were in libutil. No idea why though.
 libexpr_la_SOURCES = \
-	statistics.cpp \
-	statistics.h \
-	statistics_registry.cpp \
-	statistics_registry.h \
 	array.h \
 	array_store_all.cpp \
 	array_store_all.h \
@@ -102,7 +89,6 @@ EXTRA_DIST = \
 	expr_stream.i \
 	expr_manager.i \
 	symbol_table.i \
-	statistics.i \
 	type.i \
 	kind.i \
 	expr.i \
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 59f423e3c..0b9557cc8 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -19,9 +19,9 @@
 #include <map>
 
 #include "expr/node_manager.h"
-#include "expr/statistics_registry.h"
 #include "expr/variable_type_map.h"
 #include "options/options.h"
+#include "util/statistics_registry.h"
 
 ${includes}
 
@@ -38,7 +38,7 @@ ${includes}
       stringstream statName; \
       statName << "expr::ExprManager::" << kind; \
       d_exprStatistics[kind] = new IntStat(statName.str(), 0); \
-      d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatistics[kind]); \
+      d_nodeManager->getStatisticsRegistry()->registerStat(d_exprStatistics[kind]); \
     } \
     ++ *(d_exprStatistics[kind]); \
   }
@@ -54,7 +54,7 @@ ${includes}
         statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" << type; \
       } \
       d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \
-      d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \
+      d_nodeManager->getStatisticsRegistry()->registerStat(d_exprStatisticsVars[type]); \
     } \
     ++ *(d_exprStatisticsVars[type]); \
   }
@@ -100,14 +100,14 @@ ExprManager::~ExprManager() throw() {
 #ifdef CVC4_STATISTICS_ON
     for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
       if (d_exprStatistics[i] != NULL) {
-        d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatistics[i]);
+        d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatistics[i]);
         delete d_exprStatistics[i];
         d_exprStatistics[i] = NULL;
       }
     }
     for (unsigned i = 0; i < LAST_TYPE; ++ i) {
       if (d_exprStatisticsVars[i] != NULL) {
-        d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatisticsVars[i]);
+        d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatisticsVars[i]);
         delete d_exprStatisticsVars[i];
         d_exprStatisticsVars[i] = NULL;
       }
@@ -123,10 +123,6 @@ ExprManager::~ExprManager() throw() {
   }
 }
 
-StatisticsRegistry* ExprManager::getStatisticsRegistry() throw() {
-  return d_nodeManager->getStatisticsRegistry();
-}
-
 const Options& ExprManager::getOptions() const {
   return d_nodeManager->getOptions();
 }
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 31983d5a9..e65cfc358 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -24,7 +24,7 @@
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
-#include "expr/statistics.h"
+#include "util/statistics.h"
 #include "util/subrange_bound.h"
 
 ${includes}
@@ -43,7 +43,6 @@ class NodeManager;
 class Options;
 class IntStat;
 struct ExprManagerMapCollection;
-class StatisticsRegistry;
 class ResourceManager;
 
 namespace expr {
@@ -52,10 +51,6 @@ namespace expr {
   }/* CVC4::expr::pickle namespace */
 }/* CVC4::expr namespace */
 
-namespace stats {
-  StatisticsRegistry* getStatisticsRegistry(ExprManager*);
-}/* CVC4::stats namespace */
-
 class CVC4_PUBLIC ExprManager {
 private:
   /** The internal node manager */
@@ -88,12 +83,6 @@ private:
   /** NodeManager reaches in to get the NodeManager */
   friend class NodeManager;
 
-  /** Statistics reach in to get the StatisticsRegistry */
-  friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(ExprManager*);
-
-  /** Get the underlying statistics registry. */
-  StatisticsRegistry* getStatisticsRegistry() throw();
-
   // undefined, private copy constructor and assignment op (disallow copy)
   ExprManager(const ExprManager&) CVC4_UNDEFINED;
   ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED;
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index c9e6866d4..4cb75bfc7 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -30,7 +30,7 @@
 #include "options/options.h"
 #include "options/smt_options.h"
 #include "expr/resource_manager.h"
-#include "expr/statistics_registry.h"
+#include "util/statistics_registry.h"
 
 
 using namespace std;
diff --git a/src/expr/statistics.cpp b/src/expr/statistics.cpp
deleted file mode 100644
index e5d3f6e69..000000000
--- a/src/expr/statistics.cpp
+++ /dev/null
@@ -1,133 +0,0 @@
-/*********************                                                        */
-/*! \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 <typeinfo>
-
-#include "expr/statistics.h"
-#include "expr/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/expr/statistics.h b/src/expr/statistics.h
deleted file mode 100644
index a0b6ed083..000000000
--- a/src/expr/statistics.h
+++ /dev/null
@@ -1,129 +0,0 @@
-/*********************                                                        */
-/*! \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/expr/statistics.i b/src/expr/statistics.i
deleted file mode 100644
index 990f465f5..000000000
--- a/src/expr/statistics.i
+++ /dev/null
@@ -1,79 +0,0 @@
-%{
-#include "expr/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 "expr/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/expr/statistics_registry.cpp b/src/expr/statistics_registry.cpp
deleted file mode 100644
index 3f9124a2f..000000000
--- a/src/expr/statistics_registry.cpp
+++ /dev/null
@@ -1,176 +0,0 @@
-/*********************                                                        */
-/*! \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 "expr/statistics_registry.h"
-
-#include "base/cvc4_assert.h"
-#include "expr/expr_manager.h"
-#include "lib/clock_gettime.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-
-
-#ifdef CVC4_STATISTICS_ON
-#  define __CVC4_USE_STATISTICS true
-#else
-#  define __CVC4_USE_STATISTICS false
-#endif
-
-#warning "TODO: Make StatisticsRegistry non-public again."
-#warning "TODO: Make TimerStat non-public again."
-
-namespace CVC4 {
-
-/** 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());
-  }
-}
-
-namespace stats {
-
-// This is a friend of SmtEngine, just to reach in and get it.
-// this isn't a class function because then there's a cyclic
-// dependence.
-inline StatisticsRegistry* getStatisticsRegistry(SmtEngine* smt) {
-  return smt->d_statisticsRegistry;
-}
-
-inline StatisticsRegistry* getStatisticsRegistry(ExprManager* em) {
-  return em->getStatisticsRegistry();
-}
-
-}/* CVC4::stats namespace */
-
-StatisticsRegistry* StatisticsRegistry::current() {
-  return stats::getStatisticsRegistry(smt::currentSmtEngine());
-}
-
-void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) {
-#ifdef CVC4_STATISTICS_ON
-  StatSet& stats = current()->d_stats;
-  PrettyCheckArgument(stats.find(s) == stats.end(), s,
-                      "Statistic `%s' was already registered with this registry.",
-                      s->getName().c_str());
-  stats.insert(s);
-#endif /* CVC4_STATISTICS_ON */
-}/* StatisticsRegistry::registerStat() */
-
-void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) {
-#ifdef CVC4_STATISTICS_ON
-  StatSet& stats = current()->d_stats;
-  PrettyCheckArgument(stats.find(s) != stats.end(), s,
-                "Statistic `%s' was not registered with this registry.",
-                s->getName().c_str());
-  stats.erase(s);
-#endif /* CVC4_STATISTICS_ON */
-}/* StatisticsRegistry::unregisterStat() */
-
-void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
-#ifdef CVC4_STATISTICS_ON
-  PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s);
-  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);
-  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(ExprManager& em, Stat* stat) :
-  d_reg(stats::getStatisticsRegistry(&em)),
-  d_stat(stat) {
-  d_reg->registerStat_(d_stat);
-}
-
-RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) :
-  d_reg(stats::getStatisticsRegistry(&smt)),
-  d_stat(stat) {
-  d_reg->registerStat_(d_stat);
-}
-
-
-
-}/* CVC4 namespace */
-
-#undef __CVC4_USE_STATISTICS
diff --git a/src/expr/statistics_registry.h b/src/expr/statistics_registry.h
deleted file mode 100644
index 3225f6672..000000000
--- a/src/expr/statistics_registry.h
+++ /dev/null
@@ -1,924 +0,0 @@
-/*********************                                                        */
-/*! \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.
- **/
-
-#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 "expr/statistics.h"
-#include "lib/clock_gettime.h"
-
-namespace CVC4 {
-
-#ifdef CVC4_STATISTICS_ON
-#  define __CVC4_USE_STATISTICS true
-#else
-#  define __CVC4_USE_STATISTICS false
-#endif
-
-class ExprManager;
-class SmtEngine;
-
-/**
- * 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;
-  }
-
-#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
-  /** Get a pointer to the current statistics registry */
-  static StatisticsRegistry* current();
-#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */
-
-  /** 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);
-  }
-
-#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
-  /** Register a new statistic, making it active. */
-  static void registerStat(Stat* s) throw(CVC4::IllegalArgumentException);
-
-  /** Unregister an active statistic, making it inactive. */
-  static void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException);
-#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) */
-
-  /** Register a new statistic */
-  void registerStat_(Stat* s) throw(CVC4::IllegalArgumentException);
-
-  /** Unregister a new statistic */
-  void unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException);
-
-};/* class StatisticsRegistry */
-
-}/* CVC4 namespace */
-
-/****************************************************************************/
-/* Some utility functions for timespec                                    */
-/****************************************************************************/
-
-inline std::ostream& operator<<(std::ostream& os, const timespec& t);
-
-/** 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. */
-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. */
-inline 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;
-}
-
-namespace CVC4 {
-
-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 */
-
-/**
- * To use a statistic, you need to declare it, initialize it in your
- * constructor, register it in your constructor, and deregister it in
- * your destructor.  Instead, this macro does it all for you (and
- * therefore also keeps the statistic type, field name, and output
- * string all in the same place in your class's header.  Its use is
- * like in this example, which takes the place of the declaration of a
- * statistics field "d_checkTimer":
- *
- *   KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::checkTime");
- *
- * If any args need to be passed to the constructor, you can specify
- * them after the string.
- *
- * The macro works by creating a nested class type, derived from the
- * statistic type you give it, which declares a registry-aware
- * constructor/destructor pair.
- */
-#define KEEP_STATISTIC(_StatType, _StatField, _StatName, _CtorArgs...)  \
-  struct Statistic_##_StatField : public _StatType {                    \
-    Statistic_##_StatField() : _StatType(_StatName, ## _CtorArgs) {     \
-      StatisticsRegistry::registerStat(this);                           \
-    }                                                                   \
-    ~Statistic_##_StatField() {                                         \
-      StatisticsRegistry::unregisterStat(this);                         \
-    }                                                                   \
-  } _StatField
-
-/**
- * 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 RegisterStatistic {
-
-  StatisticsRegistry* d_reg;
-  Stat* d_stat;
-
-public:
-
-#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
-  RegisterStatistic(Stat* stat) :
-      d_reg(StatisticsRegistry::current()),
-      d_stat(stat) {
-    if(d_reg != NULL) {
-      throw CVC4::Exception("There is no current statistics registry!");
-    }
-    StatisticsRegistry::registerStat(d_stat);
-  }
-#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */
-
-  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(ExprManager& em, Stat* stat);
-
-  RegisterStatistic(SmtEngine& smt, Stat* stat);
-
-  ~RegisterStatistic() {
-    d_reg->unregisterStat_(d_stat);
-  }
-
-};/* class RegisterStatistic */
-
-#undef __CVC4_USE_STATISTICS
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__STATISTICS_REGISTRY_H */