Changing NodeBuilder::debugCheckType() to maybeCheckType()

Changing NodeManager/ExprManager constructors to take Options

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5cf3373c2f56905550fd4c768d64df1ca0cd5e19..b0951b95497e77eb1cec9eb2a7d2f27cd6d46cd9 100644 (file)
--- 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 4577135970056bca02a5b743a80a899ad0c66170..21526809e1ad88f6c6425f869ac6787fc5512511 100644 (file)
--- 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;
@@ -79,13 +80,18 @@ 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 095e81868fe4380834f189513a8d33944581a81e..ce0928209d432dbb79e24f50f5c7345cc8a33e4f 100644 (file)
--- 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 5fc704cbcb326161d08dcf2c6986548a4ad12e80..28404005cc23751e0043b2698622693107cb15d2 100644 (file)
--- 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 c262a4847b4347de9309efb21ad5b5c1487753dc..206cf35d5ae17a8e821d2d332a96849eedcbc9cc 100644 (file)
--- 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 7943da0e75bc89c30d15f9ff767687f4717596c4..38c75f0d3960913722e243d342458414a98e47ab 100644 (file)
--- 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);