Proof caching: use dependency graph to increase hit rate

key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java

@@ -3,6 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.logic;
 
+import java.util.Collection;
 import java.util.Iterator;
 
 import org.key_project.util.collection.ImmutableList;
@@ -27,11 +28,10 @@ private Semisequent() {
         seqList = ImmutableSLList.nil();
     }
 
-
     /**
-     * creates a new Semisequent with the Semisequent elements in seqList; the provided list must be
-     * redundancy free, i.e., the created sequent must be exactly the same as when creating the
-     * sequent by subsequently inserting all formulas
+     * Create a new Semisequent from an ordered collection of formulas.
+     * The provided list must be redundancy free, i.e., the created sequent must be exactly
+     * the same as when creating the sequent by subsequently inserting all formulas
      *
      * @param seqList list of sequent formulas
      */
@@ -40,6 +40,33 @@ public Semisequent(ImmutableList<SequentFormula> seqList) {
         this.seqList = seqList;
     }
 
+    /**
+     * Create a new Semisequent from an ordered collection of formulas.
+     * The provided collection must be redundancy free, i.e., the created sequent must be exactly
+     * the same as when creating the sequent by subsequently inserting all formulas
+     *
+     * @param seqList list of sequent formulas
+     */
+    public Semisequent(Collection<SequentFormula> seqList) {
+        assert !seqList.isEmpty();
+        this.seqList = ImmutableList.fromList(seqList);
+    }
+
+    /**
+     * Create a new Semisequent from an ordered collection of formulas (possibly empty).
+     * The provided collection must be redundancy free, i.e., the created sequent must be exactly
+     * the same as when creating the
+     * sequent by subsequently inserting all formulas.
+     *
+     * @param seqList list of sequent formulas
+     */
+    public static Semisequent create(Collection<SequentFormula> seqList) {
+        if (seqList.isEmpty()) {
+            return EMPTY_SEMISEQUENT;
+        }
+        return new Semisequent(seqList);
+    }
+
 
     /**
      * creates a new Semisequent with the Semisequent elements in seqList

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

@@ -465,7 +465,7 @@ public Collection<Node> children() {
     }
 
     /**
-     * @return an iterator for all nodes in the subtree.
+     * @return an iterator for all nodes in the subtree (including this node).
      */
     public Iterator<Node> subtreeIterator() {
         return new SubtreeIterator(this);

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

@@ -1466,7 +1466,7 @@ public void copyCachedGoals(Proof referencedFrom, Consumer<Integer> callbackTota
             ClosedBy c = g.node().lookup(ClosedBy.class);
             g.node().deregister(c, ClosedBy.class);
             try {
-                new CopyingProofReplayer(c.proof(), this).copy(c.node(), g);
+                new CopyingProofReplayer(c.proof(), this).copy(c.node(), g, c.nodesToSkip());
             } catch (IntermediateProofReplayer.BuiltInConstructionException e) {
                 throw new RuntimeException(e);
             }

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

@@ -4,6 +4,7 @@
 package de.uka.ilkd.key.proof;
 
 import java.util.Iterator;
+import java.util.NoSuchElementException;
 
 /**
  * Iterator over subtree. Current implementation iteratively traverses the tree depth-first.
@@ -58,6 +59,8 @@ public Node next() {
             Node s = nextSibling(n);
             if (s != null) {
                 n = s;
+            } else {
+                throw new NoSuchElementException();
             }
         } else {
             n = n.child(0);

key.core/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java

@@ -3,6 +3,8 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof.reference;
 
+import java.util.Set;
+
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 
@@ -11,7 +13,8 @@
  *
  * @param proof The proof referenced.
  * @param node  The node referenced.
+ * @param nodesToSkip If the referenced proof has dependency graph information: proof steps to skip.
  * @author Arne Keller
  */
-public record ClosedBy(Proof proof, Node node) {
+public record ClosedBy(Proof proof, Node node, Set<Node> nodesToSkip) {
 }

key.core/src/main/java/de/uka/ilkd/key/proof/replay/CopyingProofReplayer.java

@@ -5,6 +5,7 @@
 
 import java.util.ArrayDeque;
 import java.util.Deque;
+import java.util.Set;
 
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
@@ -35,24 +36,36 @@ public CopyingProofReplayer(Proof originalProof, Proof proof) {
      *
      * @param originalNode original proof
      * @param newNode open goal in new proof
+     * @param skippedNodes nodes to skip when copying
      * @throws IntermediateProofReplayer.BuiltInConstructionException on error
      */
-    public void copy(Node originalNode, Goal newNode)
+    public void copy(Node originalNode, Goal newNode, Set<Node> skippedNodes)
             throws IntermediateProofReplayer.BuiltInConstructionException {
         newNode.proof().reOpenGoal(newNode);
         newNode.proof().register(this, CopyingProofReplayer.class);
         newNode.proof().setMutedProofCloseEvents(true);
         OneStepSimplifier.refreshOSS(newNode.proof());
+
+        // nodeQueue: nodes in the ORIGINAL proof
         Deque<Node> nodeQueue = new ArrayDeque<>();
+        // queue: nodes in the NEW proof
         Deque<Goal> queue = new ArrayDeque<>();
+
         queue.add(newNode);
         nodeQueue.add(originalNode);
-        while (!nodeQueue.isEmpty()) {
+        while (!nodeQueue.isEmpty() && !queue.isEmpty()) {
             Node nextNode = nodeQueue.pop();
             Goal nextGoal = queue.pop();
             for (int i = nextNode.childrenCount() - 1; i >= 0; i--) {
                 nodeQueue.addFirst(nextNode.child(i));
             }
+            // skip explicitly requested nodes
+            if (skippedNodes.contains(nextNode)) {
+                if (!nextGoal.node().isClosed()) {
+                    queue.addFirst(nextGoal);
+                }
+                continue;
+            }
             // skip nextNode if it is a closed goal
             if (nextNode.getAppliedRuleApp() == null) {
                 continue;

key.core/src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java

@@ -3,6 +3,8 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.logic;
 
+import java.util.ArrayList;
+
 import de.uka.ilkd.key.logic.op.Function;
 import de.uka.ilkd.key.logic.sort.Sort;
 import de.uka.ilkd.key.logic.sort.SortImpl;
@@ -306,4 +308,11 @@ public void testListReplaceAddRedundantList() {
         assertEquals(expected, extract(sci), "Both semisequents should be equal.");
     }
 
+    @Test
+    void constructorTest() {
+        var a = Semisequent.EMPTY_SEMISEQUENT;
+        var b = Semisequent.create(new ArrayList<>());
+        assertSame(a, b);
+    }
+
 }

key.core/src/test/java/de/uka/ilkd/key/proof/replay/TestCopyingReplayer.java

@@ -4,6 +4,7 @@
 package de.uka.ilkd.key.proof.replay;
 
 import java.io.File;
+import java.util.HashSet;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
 import de.uka.ilkd.key.control.KeYEnvironment;
@@ -45,7 +46,7 @@ void testJavaProof() throws Exception {
         proof2.pruneProof(proof2.root());
         proof2.getServices().resetCounters();
         new CopyingProofReplayer(proof1, proof2).copy(proof1.root(),
-            proof2.getOpenGoal(proof2.root()));
+            proof2.getOpenGoal(proof2.root()), new HashSet<>());
 
         Assertions.assertTrue(proof2.closed());
         Assertions.assertEquals(proof1.countNodes(), proof2.countNodes());

key.ui/build.gradle

@@ -29,6 +29,7 @@ dependencies {
     api 'org.key-project:docking-frames-core:1.1.3p1'
 
     runtimeOnly project(":keyext.ui.testgen")
+    runtimeOnly project(":keyext.caching")
     runtimeOnly project(":keyext.exploration")
     runtimeOnly project(":keyext.slicing")
     runtimeOnly project(":keyext.proofmanagement")

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java

@@ -26,8 +26,6 @@
 import de.uka.ilkd.key.gui.configuration.Config;
 import de.uka.ilkd.key.gui.fonticons.IconFactory;
 import de.uka.ilkd.key.gui.notification.events.GeneralInformationEvent;
-import de.uka.ilkd.key.gui.plugins.caching.DefaultReferenceSearchDialogListener;
-import de.uka.ilkd.key.gui.plugins.caching.ReferenceSearchDialog;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.Statistics;
@@ -315,6 +313,8 @@ private void init(MainWindow mainWindow, String stats) {
             buttonPane2.add(saveButton);
             buttonPane2.add(saveBundleButton);
 
+            // spotless:off
+            /*
             if (proof.closedGoals().stream()
                     .anyMatch(g -> g.node().lookup(ClosedBy.class) != null)) {
                 JButton copyReferences = new JButton("Realize cached branches");
@@ -332,6 +332,8 @@ private void init(MainWindow mainWindow, String stats) {
                 });
                 buttonPane2.add(copyReferences);
             }
+             */
+            // spotless:on
 
             getRootPane().setDefaultButton(okButton);
             getRootPane().addKeyListener(new KeyAdapter() {

keyext.caching/build.gradle

@@ -0,0 +1,6 @@
+dependencies {
+    implementation project(":key.core")
+    implementation project(":key.ui")
+
+    implementation project(":keyext.slicing")
+}

key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java → keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java

@@ -363,7 +363,8 @@ public void actionPerformed(ActionEvent e) {
             Goal current = node.proof().getClosedGoal(node);
             try {
                 mediator.stopInterface(true);
-                new CopyingProofReplayer(c.proof(), node.proof()).copy(c.node(), current);
+                new CopyingProofReplayer(c.proof(), node.proof()).copy(c.node(), current,
+                    c.nodesToSkip());
                 mediator.startInterface(true);
             } catch (Exception ex) {
                 LOGGER.error("failed to copy proof ", ex);

key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java → keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java

@@ -20,6 +20,9 @@
 import de.uka.ilkd.key.rule.NoPosTacletApp;
 import de.uka.ilkd.key.rule.merge.CloseAfterMerge;
 
+import org.key_project.slicing.DependencyTracker;
+import org.key_project.slicing.analysis.AnalysisResults;
+
 /**
  * Utility class for proof caching.
  *
@@ -88,6 +91,8 @@ public static ClosedBy findPreviousProof(DefaultListModel<Proof> previousProofs,
                 }
                 return n;
             }).filter(Objects::nonNull).collect(Collectors.toCollection(ArrayDeque::new));
+            var depTracker = p.lookup(DependencyTracker.class);
+            AnalysisResults results = depTracker != null ? depTracker.analyze(true, false) : null;
             while (!nodesToCheck.isEmpty()) {
                 // for each node, check that the sequent in the reference is
                 // a subset of the new sequent
@@ -104,14 +109,27 @@ public static ClosedBy findPreviousProof(DefaultListModel<Proof> previousProofs,
                 if (n.parent() != null) {
                     nodesToCheck.add(n.parent());
                 }
-                Semisequent ante = n.sequent().antecedent();
-                Semisequent succ = n.sequent().succedent();
+                Sequent seq = n.sequent();
+                if (results != null) {
+                    seq = results.reduceSequent(n);
+                }
+                Semisequent ante = seq.antecedent();
+                Semisequent succ = seq.succedent();
                 Semisequent anteNew = newNode.sequent().antecedent();
                 Semisequent succNew = newNode.sequent().succedent();
                 if (!containedIn(anteNew, ante) || !containedIn(succNew, succ)) {
                     continue;
                 }
-                return new ClosedBy(p, n);
+                Set<Node> toSkip = new HashSet<>();
+                if (results != null) {
+                    // computed skipped nodes by iterating through all nodes
+                    n.subtreeIterator().forEachRemaining(x -> {
+                        if (!results.usefulSteps.contains(x)) {
+                            toSkip.add(x);
+                        }
+                    });
+                }
+                return new ClosedBy(p, n, toSkip);
             }
         }
         return null;

key.core/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java → keyext.caching/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java

@@ -13,6 +13,7 @@
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.settings.GeneralSettings;
 
+import org.key_project.slicing.DependencyTracker;
 import org.key_project.util.helper.FindResources;
 
 import org.junit.jupiter.api.Test;
@@ -33,11 +34,11 @@ void testFindsReferenceInSameProof() throws Exception {
 
         KeYEnvironment<DefaultUserInterfaceControl> env =
             KeYEnvironment.load(new File(testCaseDirectory,
-                "../../../../../key.ui/examples/heap/verifyThis15_1_RelaxedPrefix/relax.proof"));
+                "../key.ui/examples/heap/verifyThis15_1_RelaxedPrefix/relax.proof"));
         Proof p = env.getLoadedProof();
         KeYEnvironment<DefaultUserInterfaceControl> env2 =
             KeYEnvironment.load(new File(testCaseDirectory,
-                "../../../../../key.ui/examples/heap/verifyThis15_1_RelaxedPrefix/relax.proof"));
+                "../key.ui/examples/heap/verifyThis15_1_RelaxedPrefix/relax.proof"));
         Proof p2 = env2.getLoadedProof();
 
         DefaultListModel<Proof> previousProofs = new DefaultListModel<>();
@@ -77,6 +78,22 @@ void testFindsReferenceInSameProof() throws Exception {
         assertTrue(p.closed());
         foundReference.proof().copyCachedGoals(p2, null, null);
         assertTrue(p.closed());
+        assertNotEquals(55, foundReference.serialNr());
+        // test that copying with slicing information works
+        new DependencyTracker(p2);
+        Node n55 = p.findAny(x -> x.serialNr() == 55);
+        assertTrue(ReferenceSearcher.suitableForCloseByReference(n55));
+        ClosedBy n55Close = ReferenceSearcher.findPreviousProof(previousProofs, n55);
+        assertEquals(n55.serialNr(), n55Close.node().serialNr());
+        assertSame(p2, n55Close.proof());
+        int previousTotal = p.countNodes();
+        n55.register(n55Close, ClosedBy.class);
+        p.pruneProof(n55);
+        p.closeGoal(p.getOpenGoal(n55));
+        assertTrue(p.closed());
+        n55.proof().copyCachedGoals(p2, null, null);
+        assertTrue(p.closed());
+        assertEquals(previousTotal - 4, p.countNodes());
 
         GeneralSettings.noPruningClosed = true;
         p.dispose();

keyext.slicing/build.gradle

@@ -1,5 +1,3 @@
-description "Computiation of the proof core (the essential rule applications to close a proof)"
-
 dependencies {
     implementation project(":key.core")
     implementation project(":key.ui")

keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java

@@ -88,6 +88,10 @@ public DependencyTracker(Proof proof) {
         if (!SlicingSettingsProvider.getSlicingSettings().getAlwaysTrack()) {
             return;
         }
+        // exotic use case: registering a dependency tracker after the proof is loaded
+        if (proof.countNodes() > 1) {
+            graph.ensureProofIsTracked(proof);
+        }
         proof.addRuleAppListener(this);
     }
 
@@ -431,10 +435,12 @@ public void proofIsBeingPruned(ProofTreeEvent e) {
      * See {@link DotExporter}.
      *
      * @param abbreviateFormulas whether to shorten formula labels
+     * @param abbreviateChains whether to reduce long chains to one link
      * @return DOT string
      */
-    public String exportDot(boolean abbreviateFormulas) {
-        return DotExporter.exportDot(proof, graph, analysisResults, abbreviateFormulas);
+    public String exportDot(boolean abbreviateFormulas, boolean abbreviateChains) {
+        return DotExporter.exportDot(proof, abbreviateChains ? graph.removeChains() : graph,
+            analysisResults, abbreviateFormulas);
     }
 
     /**