diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-27 22:53:03 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-27 22:53:03 +0000 |
commit | 40d8482d24cad4d998240f79e9d6a6745cb845c1 (patch) | |
tree | 59edf15471bfabb42f94ed2f7b7e17c89f8e5a8e /src/expr/node_manager.cpp | |
parent | 3acadd4924eaef5fa31bf8982f52b3b893cf003a (diff) |
Slightly more efficient version of getType
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 21 |
1 files changed, 8 insertions, 13 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index c1456050d..b0592ba2f 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -31,7 +31,7 @@ #include "util/tls.h" #include <algorithm> -#include <list> +#include <stack> #include <ext/hash_set> using namespace std; @@ -427,15 +427,12 @@ TypeNode NodeManager::getType(TNode n, bool check) if(!hasType || needsCheck) { // TypeNode oldType = typeNode; - list<TNode> worklist; - worklist.push_back(n); + stack<TNode> worklist; + worklist.push(n); - /* Iterate and compute the children bottom up. This iteration is - very inefficient: it would be better to top-sort the Nodes so - that the leaves are always computed first. */ + /* Iterate and compute the children bottom up. */ while( !worklist.empty() ) { - TNode m = worklist.front(); - worklist.pop_front(); + TNode m = worklist.top(); bool readyToCompute = true; TNode::iterator it = m.begin(); @@ -445,17 +442,15 @@ TypeNode NodeManager::getType(TNode n, bool check) if( !hasAttribute(*it, TypeAttr()) || (check && !getAttribute(*it, TypeCheckedAttr())) ) { readyToCompute = false; - worklist.push_back(*it); + worklist.push(*it); } } if( readyToCompute ) { /* All the children have types, time to compute */ computeType(m,check); - } else { - /* Wait until the children have been computed. */ - worklist.push_back(m); - } + worklist.pop(); + } } /* Retrieve the type computed in the loop */ |