diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 0860365bc..6453a84d5 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -118,6 +118,12 @@ class NodeManager { Node d_operators[kind::LAST_KIND]; /** + * Whether to do early type checking (only effective in debug + * builds; other builds never do early type checking. + */ + const bool d_earlyTypeChecking; + + /** * Look up a NodeValue in the pool associated to this NodeManager. * The NodeValue argument need not be a "completely-constructed" * NodeValue. In particular, "non-inlined" constants are permitted @@ -233,9 +239,12 @@ class NodeManager { // bool containsDecision(TNode); // is "atomic" // bool properlyContainsDecision(TNode); // all children are atomic + // undefined private copy constructor (disallow copy) + NodeManager(const NodeManager&); + public: - NodeManager(context::Context* ctxt); + explicit NodeManager(context::Context* ctxt, bool earlyTypeChecking = true); ~NodeManager(); /** The node manager in the current context. */ |