diff 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. */ |