From: Christopher L. Conway Date: Thu, 28 Oct 2010 20:05:32 +0000 (+0000) Subject: Disabling bottom-up algorithm in NodeManager::getType() when type checking X-Git-Tag: cvc5-1.0.0~8765 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c39254b98c010397fa5b2da9513d7b3451d682d7;p=cvc5.git Disabling bottom-up algorithm in NodeManager::getType() when type checking is not requested or eager type checking is enabled --- diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 2f5ba6824..5fc704cbc 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -424,23 +424,20 @@ TypeNode NodeManager::getType(TNode n, bool check) bool needsCheck = check && !getAttribute(n, TypeCheckedAttr()); Debug("getType") << "getting type for " << n << std::endl; - if(!hasType || needsCheck) { - // TypeNode oldType = typeNode; + if(needsCheck && !d_earlyTypeChecking) { + /* Iterate and compute the children bottom up. This avoids stack + overflows in computeType() when the Node graph is really deep, + which should only affect us when we're type checking lazily. */ stack worklist; worklist.push(n); - /* Iterate and compute the children bottom up. This avoids stack - overflows in computeType() when the Node graph is really - deep. */ while( !worklist.empty() ) { TNode m = worklist.top(); bool readyToCompute = true; - for( TNode::iterator it = m.begin(), end = m.end() ; - it != end; - ++it ) { + for( TNode::iterator it = m.begin(), end = m.end() ; it != end; ++it ) { if( !hasAttribute(*it, TypeAttr()) || (check && !getAttribute(*it, TypeCheckedAttr())) ) { readyToCompute = false; @@ -450,22 +447,24 @@ TypeNode NodeManager::getType(TNode n, bool check) if( readyToCompute ) { /* All the children have types, time to compute */ - computeType(m,check); + typeNode = computeType(m,check); worklist.pop(); } - } - - /* Retrieve the type computed in the loop */ - hasType = getAttribute(n, TypeAttr(), typeNode); + } // end while + + /* Last type computed in loop should be the type of n */ + Assert( typeNode == getAttribute(n,TypeAttr()) ); + } else if( !hasType || needsCheck ) { + /* We can compute the type top-down, without worrying about + deep recursion. */ + typeNode = computeType(n,check); + } - /* Type should be there and the check should have happened if we - asked for it. */ - Assert( hasType ); - Assert( !check || hasAttribute(n, TypeCheckedAttr()) ); + /* The type should be have been computed and stored. */ + Assert( hasAttribute(n, TypeAttr()) ); + /* The check should have happened, if we asked for it. */ + Assert( !check || hasAttribute(n, TypeCheckedAttr()) ); - // DebugAssert( !hasType || oldType == typeNode, - // "Type re-computation yielded a different type" ); - } Debug("getType") << "type of " << n << " is " << typeNode << std::endl; return typeNode; }