diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-01-25 21:10:01 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-01-25 21:10:01 +0000 |
| commit | 53b60534fd72480121fa399534517938a5361c57 (patch) | |
| tree | 2cee3190e6e54a73d87b9070bf816c51cb4d84e6 /src/expr/node_manager.h | |
| parent | 0d6bb280d364f5f649d04de5fedefa3c8336f7d4 (diff) | |
scoped node managers
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 827c6c1b7..60699eeaf 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -53,6 +53,19 @@ public: Node mkVar(); }; + +class NodeManagerScope { + NodeManager *d_oldNodeManager; + +public: + NodeManagerScope(const NodeManager* nm) : d_oldNodeManager(NodeManager::s_current) { + NodeManager::s_current = nm; + } + ~NodeManagerScope() { + NodeManager::s_current = d_oldNodeManager; + } +}; + }/* CVC4 namespace */ #endif /* __CVC4__EXPR_MANAGER_H */ |