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, 23 insertions, 11 deletions

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 3b9c41973..68655aed9 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -658,17 +658,12 @@ private:
   expr::NodeValue* constructNV();
   expr::NodeValue* constructNV() const;
 
-  inline void maybeCheckType(const TNode n) const {
-    /* force an immediate type check, if early type checking is
-       enabled and the current node isn't a variable or constant */
-    if( d_nm->d_earlyTypeChecking ) {
-      kind::MetaKind mk = n.getMetaKind();
-      if( mk != kind::metakind::VARIABLE 
-          && mk != kind::metakind::CONSTANT ) {
-        d_nm->getType(n, true);
-      }
-    }
-  }
+#ifdef CVC4_DEBUG
+  void maybeCheckType(const TNode n) const
+    throw(TypeCheckingExceptionPrivate, AssertionException);
+#else /* CVC4_DEBUG */
+  inline void maybeCheckType(const TNode n) const throw() { }
+#endif /* CVC4_DEBUG */
 
 public:
 
@@ -716,6 +711,7 @@ public:
 
 #include "expr/node.h"
 #include "expr/node_manager.h"
+#include "util/options.h"
 
 namespace CVC4 {
 
@@ -1240,6 +1236,22 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
   }
 }
 
+#ifdef CVC4_DEBUG
+template <unsigned nchild_thresh>
+inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
+    throw(TypeCheckingExceptionPrivate, AssertionException) {
+  /* force an immediate type check, if early type checking is
+     enabled and the current node isn't a variable or constant */
+  if( d_nm->getOptions()->earlyTypeChecking ) {
+    kind::MetaKind mk = n.getMetaKind();
+    if( mk != kind::metakind::VARIABLE 
+        && mk != kind::metakind::CONSTANT ) {
+      d_nm->getType(n, true);
+    }
+  }
+}
+#endif /* CVC4_DEBUG */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__NODE_BUILDER_H */