Changing NodeBuilder::debugCheckType() to maybeCheckType()

Changing NodeManager/ExprManager constructors to take Options

1 files changed, 17 insertions, 5 deletions

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) {