summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.h
diff options
context:
space:
mode:
authorChristopher L. Conway <christopherleeconway@gmail.com>2010-10-27 20:10:12 +0000
committerChristopher L. Conway <christopherleeconway@gmail.com>2010-10-27 20:10:12 +0000
commit8e0be63829441a042ff030b47fa9b9a04b48984d (patch)
tree1ac7df877c8c5c9687f8a715661c6c2ed1478106 /src/expr/node_manager.h
parent4ab6323f8e5c8806ad02fc0f8417cf13b38cf350 (diff)
Modifying getType to use a non-recursive algorithm (Fixes: #228)
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r--src/expr/node_manager.h3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6c7bf500b..c262a4847 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -242,6 +242,9 @@ class NodeManager {
// undefined private copy constructor (disallow copy)
NodeManager(const NodeManager&) CVC4_UNDEFINED;
+ TypeNode computeType(TNode n, bool check = false)
+ throw (TypeCheckingExceptionPrivate, AssertionException);
+
public:
explicit NodeManager(context::Context* ctxt, bool earlyTypeChecking = true);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback