diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-04 03:42:56 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-04 03:42:56 +0000 |
commit | 1ce8e28d5976e1ab30099cb9e6943514497d2980 (patch) | |
tree | 1a9382fb62b38e3b5768da951b7c684f1b8688e7 /src/expr/node_manager.h | |
parent | 69c2d3e702f8ec0bd0eec4a481a07571131aabeb (diff) |
Type-checking classes and hooks (not tested yet).
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()) { |