diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 9d2b0947e..00fcf52c4 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -13,6 +13,8 @@ ** A manager for Nodes. **/ +#include "cvc4_private.h" + /* circular dependency; force node.h first */ #include "expr/attribute.h" #include "expr/node.h" @@ -25,6 +27,7 @@ #include <ext/hash_set> #include "expr/kind.h" +#include "expr/expr.h" namespace __gnu_cxx { template<> @@ -155,6 +158,19 @@ public: } }; +/** + * A wrapper (essentially) for NodeManagerScope. Without this, we'd + * need Expr to be a friend of ExprManager. + */ +class ExprManagerScope { + NodeManagerScope d_nms; +public: + inline ExprManagerScope(const Expr& e) : + d_nms(e.getExprManager() == NULL ? + NodeManager::currentNM() : e.getExprManager()->getNodeManager()) { + } +}; + template <class AttrKind> inline typename AttrKind::value_type NodeManager::getAttribute(TNode n, const AttrKind&) const { |