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, 20 insertions, 10 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 9006bf4d9..207f1f492 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -29,6 +29,7 @@
 
 #include "util/Assert.h"
 #include "util/options.h"
+#include "util/stats.h"
 #include "util/tls.h"
 
 #include <algorithm>
@@ -84,22 +85,28 @@ struct NVReclaim {
 };
 
 NodeManager::NodeManager(context::Context* ctxt) :
-  d_attrManager(ctxt) {
-  Options options;
-  init(options);
+  d_optionsAllocated(new Options()),
+  d_options(d_optionsAllocated),
+  d_statisticsRegistry(new StatisticsRegistry()),
+  d_attrManager(ctxt),
+  d_nodeUnderDeletion(NULL),
+  d_inReclaimZombies(false) {
+  init();
 }
 
 
 NodeManager::NodeManager(context::Context* ctxt, 
                          const Options& options) :
-  d_attrManager(ctxt) {
-  init(options);
+  d_optionsAllocated(NULL),
+  d_options(&options),
+  d_statisticsRegistry(new StatisticsRegistry()),
+  d_attrManager(ctxt),
+  d_nodeUnderDeletion(NULL),
+  d_inReclaimZombies(false) {
+  init();
 }
 
-inline void NodeManager::init(const Options& options) {
-  d_nodeUnderDeletion = NULL;
-  d_inReclaimZombies = false;
-  d_earlyTypeChecking = options.earlyTypeChecking;
+inline void NodeManager::init() {
   poolInsert( &expr::NodeValue::s_null );
 
   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
@@ -145,6 +152,9 @@ NodeManager::~NodeManager() {
     }
     Debug("gc:leaks") << ":end:" << std::endl;
   }
+
+  delete d_statisticsRegistry;
+  delete d_optionsAllocated;
 }
 
 void NodeManager::reclaimZombies() {
@@ -440,7 +450,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
 
   Debug("getType") << "getting type for " << n << std::endl;
 
-  if(needsCheck && !d_earlyTypeChecking) {
+  if(needsCheck && !d_options->earlyTypeChecking) {
     /* Iterate and compute the children bottom up. This avoids stack
        overflows in computeType() when the Node graph is really deep,
        which should only affect us when we're type checking lazily. */