This commit is a merge from the "betterstats" branch, which:

* Makes Options an "omnipresent thread-local global" (like the notion
  of the "current NodeManager" was already).  Options::current() accesses
  this structure.
* Removes Options from constructors and data structures everywhere
  (this cleans up a lot of things).
* No longer uses StatisticsRegistry statically.  An instance of the
  registry is created and linked to a NodeManager.
* StatisticsRegistry::current() is similar to Options::current(), but
  the pointer is stowed in the NodeManager (rather than stored)
* The static functions of StatisticsRegistry have been left, for backward
  compatibility; they now use the "current" statistics registry.
* SmtEngine::getStatisticsRegistry() is a public accessor for the
  registry; this is needed by main() to reach in and get the registry,
  for flushing statistics at the end.

1 files changed, 46 insertions, 3 deletions

diff --git a/src/util/stats.cpp b/src/util/stats.cpp
index 5be9525a9..428f051e0 100644
--- a/src/util/stats.cpp
+++ b/src/util/stats.cpp
@@ -18,13 +18,33 @@
  **/
 
 #include "util/stats.h"
+#include "expr/node_manager.h"
+#include "expr/expr_manager_scope.h"
 
 using namespace CVC4;
 
-StatisticsRegistry::StatSet StatisticsRegistry::d_registeredStats;
-
 std::string Stat::s_delim(",");
 
+StatisticsRegistry* StatisticsRegistry::current() {
+  return NodeManager::currentNM()->getStatisticsRegistry();
+}
+
+void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
+#ifdef CVC4_STATISTICS_ON
+  StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats;
+  AlwaysAssert(registeredStats.find(s) == registeredStats.end());
+  registeredStats.insert(s);
+#endif /* CVC4_STATISTICS_ON */
+}/* StatisticsRegistry::registerStat() */
+
+void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
+#ifdef CVC4_STATISTICS_ON
+  StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats;
+  AlwaysAssert(registeredStats.find(s) != registeredStats.end());
+  registeredStats.erase(s);
+#endif /* CVC4_STATISTICS_ON */
+}/* StatisticsRegistry::unregisterStat() */
+
 void StatisticsRegistry::flushStatistics(std::ostream& out) {
 #ifdef CVC4_STATISTICS_ON
   for(StatSet::iterator i = d_registeredStats.begin();
@@ -34,5 +54,28 @@ void StatisticsRegistry::flushStatistics(std::ostream& out) {
     s->flushStat(out);
     out << std::endl;
   }
-#endif
+#endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::flushStatistics() */
+
+StatisticsRegistry::const_iterator StatisticsRegistry::begin() {
+  return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin();
+}/* StatisticsRegistry::begin() */
+
+StatisticsRegistry::const_iterator StatisticsRegistry::end() {
+  return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.end();
+}/* StatisticsRegistry::end() */
+
+RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
+    d_em(&em), d_stat(stat) {
+  ExprManagerScope ems(*d_em);
+  StatisticsRegistry::registerStat(d_stat);
+}/* RegisterStatistic::RegisterStatistic(ExprManager&, Stat*) */
+
+RegisterStatistic::~RegisterStatistic() {
+  if(d_em != NULL) {
+    ExprManagerScope ems(*d_em);
+    StatisticsRegistry::unregisterStat(d_stat);
+  } else {
+    StatisticsRegistry::unregisterStat(d_stat);
+  }
+}/* RegisterStatistic::~RegisterStatistic() */