select last node

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java

@@ -122,10 +122,20 @@ public static class File extends KeyAst<KeYParser.FileContext> {
                 } else {
                     return new KeyAst.ProofScript(pctx.proofScript());
                 }
+        /**
+         * Returns the raw settings within a {@link de.uka.ilkd.key.proof.io.KeYFile}.
+         */
+        public Configuration findSettings() {
+            final var cfg = new ConfigurationBuilder();
+            if (ctx.preferences() == null || ctx.preferences().cvalue() == null) {
+                return new Configuration();
             }
-            return null;
+
+            var c = ctx.preferences().cvalue();
+            return (Configuration) c.accept(cfg);
         }
 
+
         /// Returns the includes (possible empty but not null) computed from the underlying parse
         /// tree.
         public Includes getIncludes(URL base) {

key.core/src/main/java/de/uka/ilkd/key/proof/Node.java

@@ -3,16 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof;
 
-import java.util.ArrayList;
-import java.util.Collection;
-import java.util.Collections;
-import java.util.HashSet;
-import java.util.Iterator;
-import java.util.LinkedHashSet;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.ListIterator;
-
 import de.uka.ilkd.key.logic.RenamingTable;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
 import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit;
@@ -24,15 +14,17 @@
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentChangeInfo;
+import de.uka.ilkd.key.util.Pair;
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.Nullable;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.collection.Pair;
 import org.key_project.util.lookup.Lookup;
 
-import org.jspecify.annotations.NonNull;
-import org.jspecify.annotations.Nullable;
+import java.util.*;
 
 public class Node implements Iterable<Node> {
     private static final String RULE_WITHOUT_NAME = "rule without name";
@@ -50,10 +42,14 @@ public class Node implements Iterable<Node> {
 
     private static final String NODES = "nodes";
 
-    /** the proof the node belongs to */
+    /**
+     * the proof the node belongs to
+     */
     private final Proof proof;
 
-    /** The parent node. **/
+    /**
+     * The parent node.
+     **/
     private @Nullable Node parent = null;
     /**
      * The branch location of this proof node.
@@ -82,7 +78,9 @@ public class Node implements Iterable<Node> {
 
     private boolean closed = false;
 
-    /** contains non-logical content, used for user feedback */
+    /**
+     * contains non-logical content, used for user feedback
+     */
     private NodeInfo nodeInfo;
 
     /**
@@ -118,7 +116,7 @@ public class Node implements Iterable<Node> {
      * taclet with an addrule section on this node, then these taclets are stored in this list
      */
     private ImmutableSet<NoPosTacletApp> localIntroducedRules =
-        DefaultImmutableSet.nil();
+            DefaultImmutableSet.nil();
 
     /**
      * Holds the undo methods for the information added by rules to the {@code Goal.strategyInfos}.
@@ -161,7 +159,9 @@ public void setSequent(Sequent seq) {
         this.seq = seq;
     }
 
-    /** returns the sequent of this node */
+    /**
+     * returns the sequent of this node
+     */
     public Sequent sequent() {
         return seq;
     }
@@ -175,7 +175,9 @@ public NodeInfo getNodeInfo() {
         return nodeInfo;
     }
 
-    /** returns the proof the Node belongs to */
+    /**
+     * returns the proof the Node belongs to
+     */
     public Proof proof() {
         return proof;
     }
@@ -225,7 +227,9 @@ public RuleApp getAppliedRuleApp() {
         return appliedRuleApp;
     }
 
-    /** Returns the set of NoPosTacletApps at this node */
+    /**
+     * Returns the set of NoPosTacletApps at this node
+     */
     public Iterable<NoPosTacletApp> getLocalIntroducedRules() {
         return localIntroducedRules;
     }
@@ -249,7 +253,7 @@ public void addLocalProgVars(Iterable<? extends IProgramVariable> elements) {
 
     /**
      * Returns the set of freshly created function symbols known to this node.
-     *
+     * <p>
      * In the resulting list, the newest additions come first.
      *
      * @return a non-null immutable list of function symbols.
@@ -444,7 +448,7 @@ List<Node> getLeaves() {
 
     /**
      * @return an iterator for the leaves of the subtree below this node. The computation is called
-     *         at every call!
+     * at every call!
      */
     public Iterator<Node> leavesIterator() {
         return new NodeIterator(getLeaves().iterator());
@@ -471,13 +475,14 @@ public Iterator<Node> subtreeIterator() {
         return new SubtreeIterator(this);
     }
 
-    /** @return number of children */
+    /**
+     * @return number of children
+     */
     public int childrenCount() {
         return children.size();
     }
 
     /**
-     *
      * @param i an index (starting at 0).
      * @return the i-th child of this node.
      */
@@ -488,7 +493,7 @@ public Node child(int i) {
     /**
      * @param child a child of this node.
      * @return the number of the node <code>child</code>, if it is a child of this node (starting
-     *         with <code>0</code>), <code>-1</code> otherwise
+     * with <code>0</code>), <code>-1</code> otherwise
      */
     public int getChildNr(Node child) {
         int res = 0;
@@ -528,16 +533,16 @@ public StringBuffer getUniqueTacletId() {
      * Helper for {@link #toString()}
      *
      * @param prefix needed to keep track if a line has to be printed
-     * @param tree the tree representation we want to add this subtree " @param preEnumeration the
-     *        enumeration of the parent without the last number
+     * @param tree   the tree representation we want to add this subtree " @param preEnumeration the
+     *               enumeration of the parent without the last number
      * @param postNr the last number of the parents enumeration
-     * @param maxNr the number of nodes at this level
-     * @param ownNr the place of this node at this level
+     * @param maxNr  the number of nodes at this level
+     * @param ownNr  the place of this node at this level
      * @return the string representation of this node.
      */
 
     private StringBuffer toString(String prefix, StringBuffer tree, String preEnumeration,
-            int postNr, int maxNr, int ownNr) {
+                                  int postNr, int maxNr, int ownNr) {
         Iterator<Node> childrenIt = childrenIterator();
         // Some constants
         String frontIndent = (maxNr > 1 ? " " : "");
@@ -588,7 +593,7 @@ private StringBuffer toString(String prefix, StringBuffer tree, String preEnumer
         while (childrenIt.hasNext()) {
             childId++;
             childrenIt.next().toString(prefix, tree, newEnumeration, newPostNr, children.size(),
-                childId);
+                    childId);
         }
 
         return tree;
@@ -645,7 +650,7 @@ public String name() {
      * this node.
      *
      * @return true iff the parent of this node has this node as child and this condition holds also
-     *         for the own children.
+     * for the own children.
      */
     public boolean sanityCheckDoubleLinks() {
         if (!root()) {
@@ -667,7 +672,9 @@ public boolean sanityCheckDoubleLinks() {
         return true;
     }
 
-    /** marks a node as closed */
+    /**
+     * marks a node as closed
+     */
     Node close() {
         closed = true;
         Node tmp = parent;
@@ -684,7 +691,7 @@ Node close() {
     /**
      * Opens a previously closed node and all its closed parents.
      * <p>
-     *
+     * <p>
      * This is, for instance, needed for the {@link MergeRule}: In a situation where a merge node
      * and its associated partners have been closed and the merge node is then pruned away, the
      * partners have to be reopened again. Otherwise, we have a soundness issue.
@@ -699,7 +706,9 @@ void reopen() {
         clearNameCache();
     }
 
-    /** @return true iff this inner node is closeable */
+    /**
+     * @return true iff this inner node is closeable
+     */
     private boolean isCloseable() {
         assert childrenCount() > 0;
         for (Node child : children) {
@@ -768,7 +777,7 @@ public void addStrategyInfoUndoMethod(StrategyInfoUndoMethod undoMethod) {
     /**
      * Register a user-defined data in this node info.
      *
-     * @param obj an object to be registered
+     * @param obj     an object to be registered
      * @param service the key under it should be registered
      * @param <T> the type of the object to be registered
      */
@@ -779,9 +788,9 @@ public <T> void register(T obj, Class<T> service) {
     /**
      * Remove a previous registered user-defined data.
      *
-     * @param obj registered object
+     * @param obj     registered object
      * @param service the key under which the data was registered
-     * @param <T> arbitray object
+     * @param <T>     arbitray object
      */
     public <T> void deregister(T obj, Class<T> service) {
         if (userData != null) {
@@ -838,4 +847,36 @@ public int getStepIndex() {
     void setStepIndex(int stepIndex) {
         this.stepIndex = stepIndex;
     }
+
+    /**
+     * Calculates an array is the path from root node to this node. Each entry defines the child to be selected.
+     *
+     * @see #traversePath(Iterator)
+     */
+    public int[] getPosInProof() {
+        // collect the path from the current to node to the root of the proof.
+        // each entry is the children position
+        var path = new LinkedList<Integer>();
+        var current = this;
+        while (current.parent != null) {
+            path.add(0, current.parent.getChildNr(current));
+            current = current.parent;
+        }
+        return path.stream().mapToInt(it -> it).toArray();
+    }
+
+
+    /**
+     * Traverses a given iterator (child selection).
+     *
+     * @param traverse non-null
+     */
+    public Node traversePath(Iterator<Integer> traverse) {
+        var current = this;
+        while (traverse.hasNext()) {
+            int child = traverse.next();
+            current = current.child(child);
+        }
+        return current;
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java

@@ -9,6 +9,7 @@
 
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.nparser.*;
+import de.uka.ilkd.key.nparser.builder.ProblemFinder;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.ProofAggregate;
 import de.uka.ilkd.key.proof.io.IProofFileParser;
@@ -34,8 +35,12 @@
  * obligation.
  */
 public final class KeYUserProblemFile extends KeYFile implements ProofOblInput {
+    @Nullable
     private Sequent problem = null;
 
+    @Nullable
+    private Configuration settings;
+
     // -------------------------------------------------------------------------
     // constructors
     // -------------------------------------------------------------------------
@@ -119,6 +124,13 @@ public ImmutableSet<PositionedString> read() throws ProofInputException {
         return warnings;
     }
 
+    public Configuration  readSettings() {
+        if(settings==null){
+            settings = getParseContext().findSettings();
+        }
+        return settings;
+    }
+
     @Override
     public void readProblem() throws ProofInputException {
         if (initConfig == null) {