ProofManagement extension: Iterative NodeIntermediateWalker to avoid stack overflows (#3793)

Author: WolframPfeifer

keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/NodeIntermediateWalker.java

@@ -3,6 +3,9 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.proofmanagement.check.dependency;
 
+import java.util.Deque;
+import java.util.LinkedList;
+
 import de.uka.ilkd.key.proof.io.intermediate.NodeIntermediate;
 
 /**
@@ -13,7 +16,7 @@
  */
 public abstract class NodeIntermediateWalker {
     /** the root where the walker starts */
-    private NodeIntermediate root;
+    private final NodeIntermediate root;
 
     /**
      * create a walker starting from the given root
@@ -24,21 +27,41 @@ protected NodeIntermediateWalker(NodeIntermediate root) {
         this.root = root;
     }
 
+
     /** starts the walker */
     public void start() {
-        walk(root);
+        walkIteratively();
     }
 
     /**
-     * walks the tree while performing specified action
+     * Walks the tree while performing specified action.
+     *
+     * @deprecated Might run into stack overflow for medium to long proofs, use
+     *             {@link #walkIteratively()} instead.
      *
      * @param node the current position of the walker in tree
      */
-    protected void walk(NodeIntermediate node) {
+    @Deprecated()
+    protected void walkRecursively(NodeIntermediate node) {
         doAction(node);
 
         for (NodeIntermediate child : node.getChildren()) {
-            walk(child);
+            walkRecursively(child);
+        }
+    }
+
+    /**
+     * Walks the tree while performing specified action. This iterative variant avoids stack
+     * overflows and is thus preferred. It performs a breadth-first search traversal.
+     */
+    protected void walkIteratively() {
+        Deque<NodeIntermediate> queue = new LinkedList<>();
+        queue.add(root);
+
+        while (!queue.isEmpty()) {
+            NodeIntermediate node = queue.pollFirst();
+            doAction(node);
+            queue.addAll(node.getChildren());
         }
     }