From d2ff1974a7cd87d841e1bcaeb0d93665f70d9259 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Thu, 28 Oct 2010 21:12:02 +0000 Subject: [PATCH] Changing NodeBuilder::debugCheckType() to maybeCheckType() Changing NodeManager/ExprManager constructors to take Options --- src/expr/expr_manager_template.cpp | 10 ++++++++-- src/expr/expr_manager_template.h | 14 ++++++++++---- src/expr/node_builder.h | 14 +++++++------- src/expr/node_manager.cpp | 22 +++++++++++++++++----- src/expr/node_manager.h | 9 +++++++-- src/main/main.cpp | 2 +- 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; @@ -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 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::constructTypeNode() const { template Node NodeBuilder::constructNode() { Node n = Node(constructNV()); - debugCheckType(n); + maybeCheckType(n); return n; } template Node NodeBuilder::constructNode() const { Node n = Node(constructNV()); - debugCheckType(n); + maybeCheckType(n); return n; } template Node* NodeBuilder::constructNodePtr() { Node *np = new Node(constructNV()); - debugCheckType(*np); + maybeCheckType(*np); return np; } template Node* NodeBuilder::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 @@ -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); -- 2.30.2