Allow pruning cached goals

KeYProject · Mar 21, 2024 · 545b836 · 545b836
1 parent eb3df15
commit 545b836
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 2 deletions.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java
@@ -253,8 +253,8 @@ public void applyInteractive(RuleApp app, Goal goal) {
     /**
      * Prunes a proof to the given node.
      *
-     * @param node
-     * @see {@link Proof#pruneProof(Node)}
+     * @param node the node to prune to
+     * @see Proof#pruneProof(Node)
      */
     public void pruneTo(Node node) {
         node.proof().pruneProof(node);

diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/ProofPruner.java b/key.core/src/main/java/de/uka/ilkd/key/proof/ProofPruner.java
@@ -7,6 +7,7 @@
 import javax.swing.*;
 
 import de.uka.ilkd.key.proof.init.InitConfig;
+import de.uka.ilkd.key.proof.reference.ClosedBy;
 import de.uka.ilkd.key.rule.NoPosTacletApp;
 import de.uka.ilkd.key.rule.merge.MergePartner;
 import de.uka.ilkd.key.rule.merge.MergeRuleBuiltInRuleApp;
@@ -37,6 +38,15 @@ class ProofPruner {
      */
     public ImmutableList<Node> prune(final Node cuttingPoint) {
 
+        // very special case: prune of cached branch
+        // (simply reopen the cached branch)
+        var closedBy = cuttingPoint.lookup(ClosedBy.class);
+        if (closedBy != null) {
+            cuttingPoint.deregister(closedBy, ClosedBy.class);
+            cuttingPoint.proof().reOpenGoal(cuttingPoint.proof().getClosedGoal(cuttingPoint));
+            return ImmutableList.of(cuttingPoint);
+        }
+
         // there is only one leaf containing an open goal that is interesting for pruning the
         // subtree of <code>node</code>, namely the first leave that is found by a breadth
         // first search.

diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java
@@ -32,6 +32,7 @@
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.delayedcut.DelayedCutListener;
 import de.uka.ilkd.key.proof.delayedcut.DelayedCutProcessor;
+import de.uka.ilkd.key.proof.reference.ClosedBy;
 import de.uka.ilkd.key.prover.TaskStartedInfo;
 import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo;
 import de.uka.ilkd.key.rule.OneStepSimplifierRuleApp;
@@ -400,6 +401,9 @@ public Prune(ProofTreeContext context) {
                                         .getClosedSubtreeGoals(context.invokedNode).size() > 0))) {
                     setEnabled(true);
                 }
+                if (context.invokedNode.lookup(ClosedBy.class) != null) {
+                    setEnabled(true);
+                }
             }
         }