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