diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-15 22:11:11 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-15 22:11:11 +0000 |
commit | e45de2ba8a8c34d3212327ed6f021462c149825c (patch) | |
tree | eb82e6d1a3bc9b133d501ff89742384156a64b3b /src/expr/node_manager.cpp | |
parent | 225f4e77f3afdebdfa046834ef7c006b9b8ec77c (diff) |
partial merge from portfolio branch, adding conversions (library-internal-only of course) between Exprs and Nodes, Types and TypeNodes, ExprManagers and NodeManagers.
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 207f1f492..793b701f8 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -84,23 +84,27 @@ struct NVReclaim { } }; -NodeManager::NodeManager(context::Context* ctxt) : +NodeManager::NodeManager(context::Context* ctxt, + ExprManager* exprManager) : d_optionsAllocated(new Options()), d_options(d_optionsAllocated), d_statisticsRegistry(new StatisticsRegistry()), d_attrManager(ctxt), + d_exprManager(exprManager), d_nodeUnderDeletion(NULL), d_inReclaimZombies(false) { init(); } -NodeManager::NodeManager(context::Context* ctxt, +NodeManager::NodeManager(context::Context* ctxt, + ExprManager* exprManager, const Options& options) : d_optionsAllocated(NULL), d_options(&options), d_statisticsRegistry(new StatisticsRegistry()), d_attrManager(ctxt), + d_exprManager(exprManager), d_nodeUnderDeletion(NULL), d_inReclaimZombies(false) { init(); @@ -444,6 +448,15 @@ TypeNode NodeManager::computeType(TNode n, bool check) TypeNode NodeManager::getType(TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { + // Many theories' type checkers call Node::getType() directly. + // This is incorrect, since "this" might not be the caller's + // curent node manager. Rather than force the individual typecheckers + // not to do this (by policy, which would be imperfect and lead + // to hard-to-find bugs, which it has in the past), we just + // set this node manager to be current for the duration of this + // check. + NodeManagerScope nms(this); + TypeNode typeNode; bool hasType = getAttribute(n, TypeAttr(), typeNode); bool needsCheck = check && !getAttribute(n, TypeCheckedAttr()); |