summaryrefslogtreecommitdiff
path: root/src/expr/node.cpp
diff options
context:
space:
mode:
authorChristopher L. Conway <christopherleeconway@gmail.com>2010-02-22 21:28:25 +0000
committerChristopher L. Conway <christopherleeconway@gmail.com>2010-02-22 21:28:25 +0000
commitc5872ac197a68ea0686c90f3a8bd1e7cc993532d (patch)
tree3a2d28f2cfb07e303a7e8f0ae87722859e9abad0 /src/expr/node.cpp
parent3d8fd1dad54c4057384c99bf6857361f29c23d12 (diff)
Switching to types-as-attributes in parser
Diffstat (limited to 'src/expr/node.cpp')
-rw-r--r--src/expr/node.cpp7
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 << ' ';
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback