diff options
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5cb19bc89..53abdb703 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -21,6 +21,7 @@ #include "expr/attribute.h" #include "expr/node.h" #include "expr/type_node.h" +#include "expr/expr.h" #ifndef __CVC4__NODE_MANAGER_H #define __CVC4__NODE_MANAGER_H @@ -507,7 +508,7 @@ public: /** * Get the type for the given node. */ - inline TypeNode getType(TNode n); + TypeNode getType(TNode n) throw (TypeCheckingExceptionPrivate); /** * Returns true if this node is atomic (has no more Boolean structure) @@ -673,13 +674,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); } -inline TypeNode NodeManager::getType(TNode n) { - TypeNode typeNode; - getAttribute(n, TypeAttr(), typeNode); - // TODO: Type computation - return typeNode; -} - inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { NodeValuePool::const_iterator find = d_nodeValuePool.find(nv); if(find == d_nodeValuePool.end()) { |