From: Christopher L. Conway <christopherleeconway@gmail.com>
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<TNode> 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;
 }