diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-22 21:28:25 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-22 21:28:25 +0000 |
commit | c5872ac197a68ea0686c90f3a8bd1e7cc993532d (patch) | |
tree | 3a2d28f2cfb07e303a7e8f0ae87722859e9abad0 /src/expr/node.cpp | |
parent | 3d8fd1dad54c4057384c99bf6857361f29c23d12 (diff) |
Switching to types-as-attributes in parser
Diffstat (limited to 'src/expr/node.cpp')
-rw-r--r-- | src/expr/node.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 90dd86712..080623e21 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -160,6 +160,13 @@ Node Node::xorExpr(const Node& right) const { return NodeManager::currentNM()->mkNode(XOR, *this, right); } +const Type* Node::getType() const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->getType(*this); +} + static void indent(ostream & o, int indent) { for(int i=0; i < indent; i++) { o << ' '; |