diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-28 21:12:02 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-28 21:12:02 +0000 |
| commit | d2ff1974a7cd87d841e1bcaeb0d93665f70d9259 (patch) | |
| tree | 6f35a4d1f191739fe9f1c2c237f6ede3ed5c99ab /src/expr/node_manager.h | |
| parent | c39254b98c010397fa5b2da9513d7b3451d682d7 (diff) | |
Changing NodeBuilder::debugCheckType() to maybeCheckType()
Changing NodeManager/ExprManager constructors to take Options
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 9 |
1 files changed, 7 insertions, 2 deletions
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. */ |