6 files changed, 50 insertions, 21 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5cf3373c2..b0951b954 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -19,6 +19,7 @@
 #include "expr/node_manager.h"
 #include "expr/expr_manager.h"
 #include "context/context.h"
+#include "util/options.h"
 
 ${includes}
 
@@ -34,9 +35,14 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
-ExprManager::ExprManager(bool earlyTypeChecking) :
+ExprManager::ExprManager() :
   d_ctxt(new Context),
-  d_nodeManager(new NodeManager(d_ctxt, earlyTypeChecking)) {
+  d_nodeManager(new NodeManager(d_ctxt)) {
+}
+
+ExprManager::ExprManager(const Options& options) :
+  d_ctxt(new Context),
+  d_nodeManager(new NodeManager(d_ctxt, options)) {
 }
 
 ExprManager::~ExprManager() {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 457713597..21526809e 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -40,6 +40,7 @@ namespace CVC4 {
 class Expr;
 class SmtEngine;
 class NodeManager;
+class Options;
 
 namespace context {
   class Context;
@@ -80,12 +81,17 @@ private:
 public:
 
   /**
+   * Creates an expression manager with default options.
+   */
+  ExprManager();
+
+  /**
    * Creates an expression manager.
-   * @param earlyTypeChecking whether to do type checking early (at Expr
-   * creation time); only used in debug builds---for other builds, type
-   * checking is never done early.
+   *
+   * @param options the earlyTypeChecking field is used to configure
+   * whether to do at Expr creation time.
    */
-  explicit ExprManager(bool earlyTypeChecking = true);
+  explicit ExprManager(const Options&);
 
   /**
    * Destroys the expression manager. No will be deallocated at this point, so
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 095e81868..ce0928209 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -661,9 +661,9 @@ private:
   expr::NodeValue* constructNV();
   expr::NodeValue* constructNV() const;
 
-  inline void debugCheckType(const TNode n) const {
-    // force an immediate type check, if we are in debug mode
-    // and the current node isn't a variable or constant
+  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 
@@ -842,28 +842,28 @@ TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() const {
 template <unsigned nchild_thresh>
 Node NodeBuilder<nchild_thresh>::constructNode() {
   Node n = Node(constructNV());
-  debugCheckType(n);
+  maybeCheckType(n);
   return n;
 }
 
 template <unsigned nchild_thresh>
 Node NodeBuilder<nchild_thresh>::constructNode() const {
   Node n = Node(constructNV());
-  debugCheckType(n);
+  maybeCheckType(n);
   return n;
 }
 
 template <unsigned nchild_thresh>
 Node* NodeBuilder<nchild_thresh>::constructNodePtr() {
   Node *np = new Node(constructNV());
-  debugCheckType(*np);
+  maybeCheckType(*np);
   return np;
 }
 
 template <unsigned nchild_thresh>
 Node* NodeBuilder<nchild_thresh>::constructNodePtr() const {
   Node *np = new Node(constructNV());
-  debugCheckType(*np);
+  maybeCheckType(*np);
   return np;
 }
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 5fc704cbc..28404005c 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -28,6 +28,7 @@
 #include "theory/bv/theory_bv_type_rules.h"
 
 #include "util/Assert.h"
+#include "util/options.h"
 #include "util/tls.h"
 
 #include <algorithm>
@@ -82,12 +83,23 @@ struct NVReclaim {
   }
 };
 
+NodeManager::NodeManager(context::Context* ctxt) :
+  d_attrManager(ctxt) {
+  Options options;
+  init(options);
+}
+
+
+NodeManager::NodeManager(context::Context* ctxt, 
+                         const Options& options) :
+  d_attrManager(ctxt) {
+  init(options);
+}
 
-NodeManager::NodeManager(context::Context* ctxt, bool earlyTypeChecking) :
-  d_attrManager(ctxt),
-  d_nodeUnderDeletion(NULL),
-  d_inReclaimZombies(false),
-  d_earlyTypeChecking(earlyTypeChecking) {
+inline void NodeManager::init(const Options& options) {
+  d_nodeUnderDeletion = NULL;
+  d_inReclaimZombies = false;
+  d_earlyTypeChecking = options.earlyTypeChecking;
   poolInsert( &expr::NodeValue::s_null );
 
   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index c262a4847..206cf35d5 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -42,6 +42,8 @@
 
 namespace CVC4 {
 
+class Options;
+
 namespace expr {
 
 // Definition of an attribute for the variable name.
@@ -121,7 +123,7 @@ class NodeManager {
    * Whether to do early type checking (only effective in debug
    * builds; other builds never do early type checking).
    */
-  const bool d_earlyTypeChecking;
+  bool d_earlyTypeChecking;
 
   /**
    * Look up a NodeValue in the pool associated to this NodeManager.
@@ -245,9 +247,12 @@ class NodeManager {
   TypeNode computeType(TNode n, bool check = false)
     throw (TypeCheckingExceptionPrivate, AssertionException);
 
+  void init(const Options& options);
+
 public:
 
-  explicit NodeManager(context::Context* ctxt, bool earlyTypeChecking = true);
+  explicit NodeManager(context::Context* ctxt);
+  explicit NodeManager(context::Context* ctxt, const Options& options);
   ~NodeManager();
 
   /** The node manager in the current context. */
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 7943da0e7..38c75f0d3 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -172,7 +172,7 @@ int runCvc4(int argc, char* argv[]) {
   }
 
   // Create the expression manager
-  ExprManager exprMgr(options.earlyTypeChecking);
+  ExprManager exprMgr(options);
 
   // Create the SmtEngine
   SmtEngine smt(&exprMgr, options);