diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/NodeIntermediateWalker.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/NodeIntermediateWalker.java index 9afa8bbd5c9..619ddff9e40 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/NodeIntermediateWalker.java +++ b/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 queue = new LinkedList<>(); + queue.add(root); + + while (!queue.isEmpty()) { + NodeIntermediate node = queue.pollFirst(); + doAction(node); + queue.addAll(node.getChildren()); } }