diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-15 22:11:11 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-15 22:11:11 +0000 |
commit | e45de2ba8a8c34d3212327ed6f021462c149825c (patch) | |
tree | eb82e6d1a3bc9b133d501ff89742384156a64b3b /src/expr/node.h | |
parent | 225f4e77f3afdebdfa046834ef7c006b9b8ec77c (diff) |
partial merge from portfolio branch, adding conversions (library-internal-only of course) between Exprs and Nodes, Types and TypeNodes, ExprManagers and NodeManagers.
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index d67bc2e2b..2509640e0 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -372,6 +372,22 @@ public: // bool properlyContainsDecision(); // maybe not atomic but all children are /** + * Convert this Node into an Expr using the currently-in-scope + * manager. Essentially this is like an "operator Expr()" but we + * don't want it to compete with implicit conversions between e.g. + * Node and TNode, and we want internal-to-external interface + * (Node -> Expr) points to be explicit. We could write an + * explicit Expr(Node) constructor---but that dirties the public + * interface. + */ + inline Expr toExpr(); + + /** + * Convert an Expr into a Node. + */ + static inline Node fromExpr(const Expr& e); + + /** * Returns true if this node represents a constant * @return true if const */ @@ -1176,6 +1192,18 @@ Node NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, } } +template <bool ref_count> +inline Expr NodeTemplate<ref_count>::toExpr() { + assertTNodeNotExpired(); + return NodeManager::currentNM()->toExpr(*this); +} + +// intentionally not defined for TNode +template <> +inline Node NodeTemplate<true>::fromExpr(const Expr& e) { + return NodeManager::fromExpr(e); +} + #ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used |