From c8476ae902201cad837b9b2510c2eef2e0de9e43 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 15 May 2023 10:34:36 +0200 Subject: [PATCH 01/26] Proof reordering WIP --- .../main/java/de/uka/ilkd/key/proof/Node.java | 4 + .../org/key_project/slicing/ProofReorder.java | 78 +++++++++++++++++++ .../key_project/slicing/SlicingExtension.java | 15 ++++ 3 files changed, 97 insertions(+) create mode 100644 keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java index 4a2e1035d7d..bcc662f4dbe 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java @@ -395,6 +395,10 @@ void remove() { } } + public void removeChildren() { + children.clear(); + } + /** * Removes child/parent relationship between the given node and this node; if the given node is * not child of this node, nothing happens and then and only then false is returned. diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java new file mode 100644 index 00000000000..600bb586e9a --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -0,0 +1,78 @@ +package org.key_project.slicing; + +import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.logic.PosInTerm; +import de.uka.ilkd.key.logic.SequentFormula; +import de.uka.ilkd.key.proof.BranchLocation; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import org.key_project.slicing.graph.DependencyGraph; +import org.key_project.slicing.graph.GraphNode; + +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Collections; +import java.util.Comparator; +import java.util.Deque; +import java.util.HashSet; +import java.util.List; +import java.util.Set; +import java.util.stream.Collectors; + +public final class ProofReorder { + public static void reorderProof(Proof proof, DependencyGraph depGraph) { + Deque q = new ArrayDeque<>(); + var root = proof.root(); + for (int i = 1; i <= root.sequent().size(); i++) { + var node = depGraph.getGraphNode(proof, BranchLocation.ROOT, PosInOccurrence.findInSequent(root.sequent(), i, PosInTerm.getTopLevel())); + q.addLast(node); + } + List newOrder = new ArrayList<>(); + Set newOrderSorted = new HashSet<>(); + while (!q.isEmpty()) { + var nextNode = q.pop(); + System.out.println("trying " + nextNode.toString(false, false)); + depGraph.outgoingEdgesOf(nextNode).forEach(node -> { + // TODO: do this per branch + if (node.getBranchLocation() != BranchLocation.ROOT) { + return; + } + + if (newOrderSorted.contains(node)) { + return; + } + // check that all inputs are available + if (!depGraph.inputsOf(node).allMatch(otherNode -> depGraph.edgesProducing(otherNode).allMatch(edge -> newOrderSorted.contains(edge.getProofStep())))) { + q.addLast(nextNode); + return; + } + newOrder.add(node); + newOrderSorted.add(node); + + var outputs = depGraph.outputsOf(node).collect(Collectors.toList()); + Collections.reverse(outputs); + outputs.forEach(q::addFirst); + }); + } + // final children + var finalChildren = newOrder.stream().max(Comparator.comparing(n -> n.serialNr())).get().childrenIterator(); + var finalChildrenList = new ArrayList<>(); + while (finalChildren.hasNext()) { + finalChildrenList.add(finalChildren.next()); + } + for (int i = 0; i < newOrder.size(); i++) { + newOrder.get(i).removeChildren(); + } + // done, reorder proof steps now + Node last = null; + for (Node next : newOrder) { + if (last != null) { + last.removeChildren(); + last.add(next); + } + last = next; + } + last.addAll(finalChildrenList.toArray(new Node[0])); + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index 0d2807359cd..033b581bcfd 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -47,6 +47,7 @@ public class SlicingExtension implements KeYGuiExtension, KeYGuiExtension.Startup, KeYGuiExtension.LeftPanel, KeYGuiExtension.Settings, +KeYGuiExtension.Toolbar, KeYSelectionListener, ProofDisposedListener { /** @@ -175,4 +176,18 @@ public SettingsProvider getSettings() { public void enableSafeModeForNextProof() { this.enableSafeModeForNextProof = true; } + + @Nonnull + @Override + public JToolBar getToolbar(MainWindow mainWindow) { + JToolBar bar = new JToolBar(); + JButton b = new JButton(); + b.setText("Reorder"); + b.addActionListener(e -> { + KeYMediator m = MainWindow.getInstance().getMediator(); + ProofReorder.reorderProof(m.getSelectedProof(), trackers.get(m.getSelectedProof()).getDependencyGraph()); + }); + bar.add(b); + return bar; + } } From b56e32f435b6c026d8d5186c8afbeaa59f4d4bfd Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 20 May 2023 15:47:22 +0200 Subject: [PATCH 02/26] Add a 'shortened' dependency graph view --- .../de/uka/ilkd/key/java/Recoder2KeY.java | 1 + .../rule/tacletbuilder/TacletGenerator.java | 1 - .../de/uka/ilkd/key/util/LinkedHashMap.java | 1 + .../key/gui/actions/UnicodeToggleAction.java | 1 - .../main/java/de/uka/ilkd/key/util/Pair.java | 0 .../java/de/uka/ilkd/key/util/Quadruple.java | 0 .../java/de/uka/ilkd/key/util/Triple.java | 0 .../util/collection/DefaultEdge.java | 14 +++--- .../util/collection/DirectedGraph.java | 19 ++++++- .../util/collection/GraphEdge.java | 10 ++-- .../util/collection/GraphUtil.java | 40 +++++++++++++++ .../slicing/DependencyTracker.java | 12 +---- .../org/key_project/slicing/ProofReorder.java | 29 ++++++----- .../key_project/slicing/SlicingExtension.java | 5 +- .../slicing/graph/AnnotatedEdge.java | 2 +- .../slicing/graph/DependencyGraph.java | 10 ++++ .../slicing/graph/DotExporter.java | 50 ++++++++++++++++++- .../slicing/ui/SlicingLeftPanel.java | 23 +++++++++ 18 files changed, 175 insertions(+), 43 deletions(-) rename {key.core => key.util}/src/main/java/de/uka/ilkd/key/util/Pair.java (100%) rename {key.core => key.util}/src/main/java/de/uka/ilkd/key/util/Quadruple.java (100%) rename {key.core => key.util}/src/main/java/de/uka/ilkd/key/util/Triple.java (100%) create mode 100644 key.util/src/main/java/org/key_project/util/collection/GraphUtil.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java index 4409770292f..d08d9e70f45 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java @@ -20,6 +20,7 @@ import de.uka.ilkd.key.proof.io.consistency.FileRepo; import de.uka.ilkd.key.util.*; import de.uka.ilkd.key.util.LinkedHashMap; +import de.uka.ilkd.key.util.Pair; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java index 75274721f04..6ac13ffdf2a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java @@ -19,7 +19,6 @@ import de.uka.ilkd.key.speclang.HeapContext; import de.uka.ilkd.key.util.Pair; -import org.key_project.util.collection.*; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMap.java b/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMap.java index 65a890b04cc..8cc5bc96a71 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMap.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMap.java @@ -1,5 +1,6 @@ package de.uka.ilkd.key.util; + import java.util.Iterator; import java.util.Map; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/UnicodeToggleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/UnicodeToggleAction.java index 205389a2996..0cd28cb39e7 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/UnicodeToggleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/UnicodeToggleAction.java @@ -3,7 +3,6 @@ import java.awt.event.ActionEvent; import java.beans.PropertyChangeListener; import java.util.EventObject; -import javax.swing.*; import javax.swing.JCheckBoxMenuItem; import de.uka.ilkd.key.gui.MainWindow; diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/Pair.java b/key.util/src/main/java/de/uka/ilkd/key/util/Pair.java similarity index 100% rename from key.core/src/main/java/de/uka/ilkd/key/util/Pair.java rename to key.util/src/main/java/de/uka/ilkd/key/util/Pair.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/Quadruple.java b/key.util/src/main/java/de/uka/ilkd/key/util/Quadruple.java similarity index 100% rename from key.core/src/main/java/de/uka/ilkd/key/util/Quadruple.java rename to key.util/src/main/java/de/uka/ilkd/key/util/Quadruple.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/Triple.java b/key.util/src/main/java/de/uka/ilkd/key/util/Triple.java similarity index 100% rename from key.core/src/main/java/de/uka/ilkd/key/util/Triple.java rename to key.util/src/main/java/de/uka/ilkd/key/util/Triple.java diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java b/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java index a2b422b1ca6..efc3180e308 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java +++ b/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java @@ -6,33 +6,33 @@ * * @author Arne Keller */ -public class DefaultEdge implements GraphEdge { +public class DefaultEdge implements GraphEdge { /** * Source node of this edge. */ - private Object source; + private V source; /** * Target node of this edge. */ - private Object target; + private V target; @Override - public Object getSource() { + public V getSource() { return source; } @Override - public void setSource(Object source) { + public void setSource(V source) { this.source = source; } @Override - public Object getTarget() { + public V getTarget() { return target; } @Override - public void setTarget(Object target) { + public void setTarget(V target) { this.target = target; } } diff --git a/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java b/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java index dfc67953ff1..62d926b91eb 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java +++ b/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java @@ -14,7 +14,7 @@ * @param edge type * @author Arne Keller */ -public class DirectedGraph implements Graph { +public class DirectedGraph> implements Graph { /** * Set of vertices in this graph. */ @@ -127,4 +127,21 @@ public void removeEdge(E e) { incomingEdges.get(e.getTarget()).remove(e); edges.remove(e); } + + /** + * Create a copy of this graph. A new set of vertices and edges is created, + * but the vertex and edge objects are shared. + * + * @return copy of this graph + */ + public DirectedGraph copy() { + DirectedGraph graph = new DirectedGraph<>(); + for (V v : vertices) { + graph.addVertex(v); + } + for (E e : edges) { + graph.addEdge((V) e.getSource(), (V) e.getTarget(), e); + } + return graph; + } } diff --git a/key.util/src/main/java/org/key_project/util/collection/GraphEdge.java b/key.util/src/main/java/org/key_project/util/collection/GraphEdge.java index b0d8ae99e16..3c7711df99f 100644 --- a/key.util/src/main/java/org/key_project/util/collection/GraphEdge.java +++ b/key.util/src/main/java/org/key_project/util/collection/GraphEdge.java @@ -5,28 +5,28 @@ * * @author Arne Keller */ -public interface GraphEdge { +public interface GraphEdge { /** * @return where this edge starts */ - Object getSource(); + V getSource(); /** * @return where this edge goes to */ - Object getTarget(); + V getTarget(); /** * Specify the source of this edge. * * @param source source node */ - void setSource(Object source); + void setSource(V source); /** * Specify the target of this edge. * * @param target target node */ - void setTarget(Object target); + void setTarget(V target); } diff --git a/key.util/src/main/java/org/key_project/util/collection/GraphUtil.java b/key.util/src/main/java/org/key_project/util/collection/GraphUtil.java new file mode 100644 index 00000000000..aea5a9760ca --- /dev/null +++ b/key.util/src/main/java/org/key_project/util/collection/GraphUtil.java @@ -0,0 +1,40 @@ +package org.key_project.util.collection; + +import java.util.ArrayDeque; +import java.util.Deque; +import java.util.function.Function; + +import de.uka.ilkd.key.util.Quadruple; + +/** + * Utility functions for manipulating graphs. + * + * @author Arne Keller + */ +public final class GraphUtil { + private GraphUtil() { + + } + + public static > void collapseChains(DirectedGraph graph, + Function, E> edgeFactory) { + Deque todo = new ArrayDeque<>(graph.vertexSet()); + while (!todo.isEmpty()) { + V v = todo.pop(); + var incoming = graph.incomingEdgesOf(v); + var outgoing = graph.outgoingEdgesOf(v); + if (incoming.size() == 1 && outgoing.size() == 1) { + var in = incoming.iterator().next(); + var out = outgoing.iterator().next(); + var newEdge = + edgeFactory.apply(new Quadruple<>(in.getSource(), out.getTarget(), in, out)); + var src = in.getSource(); + var dst = out.getTarget(); + graph.removeVertex(v); + graph.addEdge(src, dst, newEdge); + todo.add(src); + todo.add(dst); + } + } + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java index 71f87068f38..6f9c6217f75 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java @@ -47,9 +47,6 @@ import org.key_project.slicing.graph.TrackedFormula; import org.key_project.util.collection.ImmutableList; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - /** * Tracks proof steps as they are applied on the proof. * Each proof step is recorded in the dependency graph ({@link DependencyGraph}). @@ -57,11 +54,6 @@ * @author Arne Keller */ public class DependencyTracker implements RuleAppListener, ProofTreeListener { - /** - * Logger. - */ - private static final Logger LOGGER = LoggerFactory.getLogger(DependencyTracker.class); - /** * The proof this tracker monitors. */ @@ -81,7 +73,6 @@ public class DependencyTracker implements RuleAppListener, ProofTreeListener { * @see DependencyAnalyzer */ private AnalysisResults analysisResults = null; - private boolean proofUsedStateMerging = false; /** * Construct a new tracker for a proof. @@ -354,7 +345,8 @@ public void proofIsBeingPruned(ProofTreeEvent e) { * @return DOT string */ public String exportDot(boolean abbreviateFormulas) { - return DotExporter.exportDot(proof, graph, analysisResults, abbreviateFormulas); + return DotExporter.exportDot(proof, graph.getInternalGraph(), analysisResults, + abbreviateFormulas); } /** diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index 600bb586e9a..b20ea600990 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -1,17 +1,7 @@ package org.key_project.slicing; -import de.uka.ilkd.key.logic.PosInOccurrence; -import de.uka.ilkd.key.logic.PosInTerm; -import de.uka.ilkd.key.logic.SequentFormula; -import de.uka.ilkd.key.proof.BranchLocation; -import de.uka.ilkd.key.proof.Node; -import de.uka.ilkd.key.proof.Proof; -import org.key_project.slicing.graph.DependencyGraph; -import org.key_project.slicing.graph.GraphNode; - import java.util.ArrayDeque; import java.util.ArrayList; -import java.util.Collection; import java.util.Collections; import java.util.Comparator; import java.util.Deque; @@ -20,12 +10,22 @@ import java.util.Set; import java.util.stream.Collectors; +import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.logic.PosInTerm; +import de.uka.ilkd.key.proof.BranchLocation; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; + +import org.key_project.slicing.graph.DependencyGraph; +import org.key_project.slicing.graph.GraphNode; + public final class ProofReorder { public static void reorderProof(Proof proof, DependencyGraph depGraph) { Deque q = new ArrayDeque<>(); var root = proof.root(); for (int i = 1; i <= root.sequent().size(); i++) { - var node = depGraph.getGraphNode(proof, BranchLocation.ROOT, PosInOccurrence.findInSequent(root.sequent(), i, PosInTerm.getTopLevel())); + var node = depGraph.getGraphNode(proof, BranchLocation.ROOT, + PosInOccurrence.findInSequent(root.sequent(), i, PosInTerm.getTopLevel())); q.addLast(node); } List newOrder = new ArrayList<>(); @@ -43,7 +43,9 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) { return; } // check that all inputs are available - if (!depGraph.inputsOf(node).allMatch(otherNode -> depGraph.edgesProducing(otherNode).allMatch(edge -> newOrderSorted.contains(edge.getProofStep())))) { + if (!depGraph.inputsOf(node) + .allMatch(otherNode -> depGraph.edgesProducing(otherNode) + .allMatch(edge -> newOrderSorted.contains(edge.getProofStep())))) { q.addLast(nextNode); return; } @@ -56,7 +58,8 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) { }); } // final children - var finalChildren = newOrder.stream().max(Comparator.comparing(n -> n.serialNr())).get().childrenIterator(); + var finalChildren = + newOrder.stream().max(Comparator.comparing(n -> n.serialNr())).get().childrenIterator(); var finalChildrenList = new ArrayList<>(); while (finalChildren.hasNext()) { finalChildrenList.add(finalChildren.next()); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index 033b581bcfd..e841ec56f7f 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -47,7 +47,7 @@ public class SlicingExtension implements KeYGuiExtension, KeYGuiExtension.Startup, KeYGuiExtension.LeftPanel, KeYGuiExtension.Settings, -KeYGuiExtension.Toolbar, + KeYGuiExtension.Toolbar, KeYSelectionListener, ProofDisposedListener { /** @@ -185,7 +185,8 @@ public JToolBar getToolbar(MainWindow mainWindow) { b.setText("Reorder"); b.addActionListener(e -> { KeYMediator m = MainWindow.getInstance().getMediator(); - ProofReorder.reorderProof(m.getSelectedProof(), trackers.get(m.getSelectedProof()).getDependencyGraph()); + ProofReorder.reorderProof(m.getSelectedProof(), + trackers.get(m.getSelectedProof()).getDependencyGraph()); }); bar.add(b); return bar; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedEdge.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedEdge.java index 1220e48c692..fb7cc4e2a78 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedEdge.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedEdge.java @@ -9,7 +9,7 @@ * * @author Arne Keller */ -public class AnnotatedEdge extends DefaultEdge { +public class AnnotatedEdge extends DefaultEdge { /** * The node that added this edge to the dependency graph. */ diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java index b08c9bedc0d..0aa8278bb8a 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java @@ -12,6 +12,7 @@ import org.key_project.slicing.DependencyNodeData; import org.key_project.util.EqualsModProofIrrelevancy; +import org.key_project.util.collection.DirectedGraph; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -332,4 +333,13 @@ public GraphNode getGraphNode(Proof proof, BranchLocation locationGuess, PosInOc } return null; } + + /** + * Get a copy of the internal graph. + * + * @return internal graph data + */ + public DirectedGraph getInternalGraph() { + return graph.copy(); + } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DotExporter.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DotExporter.java index 5bbe534dcc9..458f344d62f 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DotExporter.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DotExporter.java @@ -14,6 +14,7 @@ import org.key_project.slicing.DependencyNodeData; import org.key_project.slicing.analysis.AnalysisResults; +import org.key_project.util.collection.DirectedGraph; /** * Exports a {@link DependencyGraph} in DOT format. @@ -32,6 +33,51 @@ public final class DotExporter { private DotExporter() { } + /** + * Convert the given dependency graph into a text representation (DOT format). + * If analysis results are given, useless nodes and edges are marked in red. + * If abbreviateFormulas is true, node labels are shortened. + * + * @param graph dependency graph to show + * @return string representing the dependency graph + */ + public static String exportDot2(DirectedGraph graph) { + StringBuilder buf = new StringBuilder(); + buf.append("digraph {\n"); + // expected direction in output rendering is reverse internal order + buf.append("edge [dir=\"back\"];\n"); + + for (AnnotatedEdge in : graph.edgeSet()) { + var src = in.getSource(); + var dst = in.getTarget(); + String inString = src.toString(false, false); + String outString = dst.toString(false, false); + var label = in.getProofStep().lookup(DependencyNodeData.class).label; + buf + .append('"') + .append(inString) + .append("\" -> \"") + .append(outString) + .append("\" [label=\"") + .append(label) + .append("\"]\n"); + // make sure the formulas are drawn with the correct shape + String shape = SHAPES.get(src.getClass()); + if (shape != null) { + buf.append('"').append(inString).append("\" [shape=\"").append(shape) + .append("\"]\n"); + } + shape = SHAPES.get(dst.getClass()); + if (shape != null) { + buf.append('"').append(outString).append("\" [shape=\"").append(shape) + .append("\"]\n"); + } + } + + buf.append('}'); + return buf.toString(); + } + /** * Convert the given dependency graph into a text representation (DOT format). * If analysis results are given, useless nodes and edges are marked in red. @@ -45,7 +91,7 @@ private DotExporter() { */ public static String exportDot( Proof proof, - DependencyGraph graph, + DirectedGraph graph, AnalysisResults analysisResults, boolean abbreviateFormulas) { StringBuilder buf = new StringBuilder(); @@ -69,7 +115,7 @@ public static String exportDot( } // colorize useless nodes if (analysisResults != null) { - for (GraphNode formula : graph.nodes()) { + for (GraphNode formula : graph.vertexSet()) { if (!analysisResults.usefulNodes.contains(formula)) { buf.append('"').append(formula.toString(abbreviateFormulas, false)).append('"') .append(" [color=\"red\"]\n"); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java index c93d6d7fa34..b4e43293fb5 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java @@ -37,8 +37,11 @@ import org.key_project.slicing.SlicingProofReplayer; import org.key_project.slicing.SlicingSettingsProvider; import org.key_project.slicing.analysis.AnalysisResults; +import org.key_project.slicing.graph.AnnotatedEdge; +import org.key_project.slicing.graph.DotExporter; import org.key_project.slicing.util.GenericWorker; import org.key_project.slicing.util.GraphvizDotExecutor; +import org.key_project.util.collection.GraphUtil; import bibliothek.gui.dock.common.action.CAction; import org.slf4j.Logger; @@ -90,6 +93,10 @@ public class SlicingLeftPanel extends JPanel implements TabPanel, KeYSelectionLi * "Show rendering of graph" button. */ private JButton showGraphRendering = null; + /** + * "Show rendering of graph (shortened)" button. + */ + private JButton showGraphRenderingShort = null; /** * If {@link #ENABLE_DEBUGGING_UI} is true: a button that will call the garbage collector */ @@ -322,11 +329,16 @@ private JPanel getDependencyGraphPanel() { dotExport.addActionListener(this::exportDot); showGraphRendering = new JButton("Show rendering of graph"); showGraphRendering.addActionListener(this::previewGraph); + showGraphRenderingShort = new JButton("Show rendering of graph (shortened)"); + showGraphRenderingShort.addActionListener(this::previewGraphShort); if (!GraphvizDotExecutor.isDotInstalled()) { showGraphRendering.setEnabled(false); + showGraphRenderingShort.setEnabled(false); showGraphRendering.setToolTipText( "Install graphviz (dot) to enable graph rendering functionality."); + showGraphRenderingShort.setToolTipText( + "Install graphviz (dot) to enable graph rendering functionality."); } graphNodes = new JLabel(); @@ -342,6 +354,7 @@ private JPanel getDependencyGraphPanel() { panel1.add(abbreviateFormulas); panel1.add(dotExport); panel1.add(showGraphRendering); + panel1.add(showGraphRenderingShort); return panel1; } @@ -409,6 +422,16 @@ private void previewGraph(ActionEvent e) { new PreviewDialog(MainWindow.getInstance(), text); } + private void previewGraphShort(ActionEvent e) { + if (currentProof == null) { + return; + } + var g = extension.trackers.get(currentProof).getDependencyGraph().getInternalGraph(); + GraphUtil.collapseChains(g, q -> new AnnotatedEdge(q.fourth.getProofStep(), false)); + String text = DotExporter.exportDot2(g); + new PreviewDialog(MainWindow.getInstance(), text); + } + private AnalysisResults analyzeProof() { if (currentProof == null) { return null; From 3f514d6dd01fcceedde469373bc754c6d53f2921 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 20 May 2023 16:35:40 +0200 Subject: [PATCH 03/26] Reorder steps in all branches --- .../main/java/de/uka/ilkd/key/proof/Node.java | 15 ++ .../org/key_project/slicing/ProofReorder.java | 140 ++++++++++++------ 2 files changed, 106 insertions(+), 49 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java index bcc662f4dbe..8eaf83a2ba1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java @@ -399,6 +399,12 @@ public void removeChildren() { children.clear(); } + public void replaceChild(int i, Node newChild) { + children.set(i, newChild); + newChild.parent = this; + newChild.siblingNr = i; + } + /** * Removes child/parent relationship between the given node and this node; if the given node is * not child of this node, nothing happens and then and only then false is returned. @@ -826,4 +832,13 @@ public int getStepIndex() { void setStepIndex(int stepIndex) { this.stepIndex = stepIndex; } + + public Node getFirstInBranch() { + Node candidate = this; + while (candidate.parent != null + && candidate.parent.getBranchLocation().equals(candidate.getBranchLocation())) { + candidate = candidate.parent; + } + return candidate; + } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index b20ea600990..89c04df2186 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -10,72 +10,114 @@ import java.util.Set; import java.util.stream.Collectors; +import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.PosInTerm; import de.uka.ilkd.key.proof.BranchLocation; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.util.Pair; import org.key_project.slicing.graph.DependencyGraph; import org.key_project.slicing.graph.GraphNode; public final class ProofReorder { + private ProofReorder() { + + } + public static void reorderProof(Proof proof, DependencyGraph depGraph) { - Deque q = new ArrayDeque<>(); - var root = proof.root(); - for (int i = 1; i <= root.sequent().size(); i++) { - var node = depGraph.getGraphNode(proof, BranchLocation.ROOT, - PosInOccurrence.findInSequent(root.sequent(), i, PosInTerm.getTopLevel())); - q.addLast(node); - } - List newOrder = new ArrayList<>(); - Set newOrderSorted = new HashSet<>(); - while (!q.isEmpty()) { - var nextNode = q.pop(); - System.out.println("trying " + nextNode.toString(false, false)); - depGraph.outgoingEdgesOf(nextNode).forEach(node -> { - // TODO: do this per branch - if (node.getBranchLocation() != BranchLocation.ROOT) { - return; - } + MainWindow.getInstance().getMediator().stopInterface(true); + + Set done = new HashSet<>(); + + Deque> todo = new ArrayDeque<>(); + todo.add(new Pair<>(BranchLocation.ROOT, proof.root())); + while (!todo.isEmpty()) { + var t = todo.pop(); + var root = t.second; + var loc = t.first; + System.out.println("copying " + loc); + if (done.contains(loc)) { + continue; + } + done.add(loc); + + Deque q = new ArrayDeque<>(); + for (int i = 1; i <= root.sequent().size(); i++) { + var node = depGraph.getGraphNode(proof, loc, + PosInOccurrence.findInSequent(root.sequent(), i, PosInTerm.getTopLevel())); + q.addLast(node); + } + List newOrder = new ArrayList<>(); + Set newOrderSorted = new HashSet<>(); + while (!q.isEmpty()) { + var nextNode = q.pop(); + depGraph.outgoingEdgesOf(nextNode).forEach(node -> { + if (!node.getBranchLocation().equals(loc)) { + todo.add(new Pair<>(node.getBranchLocation(), node.getFirstInBranch())); + return; + } - if (newOrderSorted.contains(node)) { - return; + if (newOrderSorted.contains(node)) { + return; + } + // check that all inputs are available + if (!depGraph.inputsOf(node) + .allMatch(otherNode -> depGraph.edgesProducing(otherNode) + .allMatch(edge -> newOrderSorted.contains(edge.getProofStep()) + || !edge.getProofStep().getBranchLocation() + .equals(loc)))) { + q.addLast(nextNode); + return; + } + newOrder.add(node); + newOrderSorted.add(node); + + var outputs = depGraph.outputsOf(node).collect(Collectors.toList()); + Collections.reverse(outputs); + outputs.forEach(q::addFirst); + }); + } + var firstNode = newOrder.stream().min(Comparator.comparing(Node::serialNr)).get(); + var lastNode = newOrder.stream().max(Comparator.comparing(Node::serialNr)).get(); + newOrder.remove(lastNode); + Node closingNode = null; + for (int i = 0; i < newOrder.size(); i++) { + if (newOrder.get(i).childrenCount() == 0) { + closingNode = newOrder.get(i); } - // check that all inputs are available - if (!depGraph.inputsOf(node) - .allMatch(otherNode -> depGraph.edgesProducing(otherNode) - .allMatch(edge -> newOrderSorted.contains(edge.getProofStep())))) { - q.addLast(nextNode); - return; + newOrder.get(i).removeChildren(); + } + // done, reorder proof steps now + Node last = firstNode.parent(); + for (Node next : newOrder) { + if (last != null) { + if (last.childrenCount() > 1) { + for (int i = 0; i < last.childrenCount(); i++) { + if (last.child(i).getBranchLocation() == loc) { + last.replaceChild(i, next); + break; + } + } + } else { + last.removeChildren(); + if (last == closingNode) { + last = null; + break; + } + last.add(next); + } } - newOrder.add(node); - newOrderSorted.add(node); - - var outputs = depGraph.outputsOf(node).collect(Collectors.toList()); - Collections.reverse(outputs); - outputs.forEach(q::addFirst); - }); - } - // final children - var finalChildren = - newOrder.stream().max(Comparator.comparing(n -> n.serialNr())).get().childrenIterator(); - var finalChildrenList = new ArrayList<>(); - while (finalChildren.hasNext()) { - finalChildrenList.add(finalChildren.next()); - } - for (int i = 0; i < newOrder.size(); i++) { - newOrder.get(i).removeChildren(); - } - // done, reorder proof steps now - Node last = null; - for (Node next : newOrder) { + last = next; + } if (last != null) { last.removeChildren(); - last.add(next); + last.add(lastNode); } - last = next; } - last.addAll(finalChildrenList.toArray(new Node[0])); + + System.out.println("done!"); + MainWindow.getInstance().getMediator().startInterface(true); } } From 4a1c9c28a4856be82d3a2111d34c36fe5ddc486b Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 22 May 2023 09:31:02 +0200 Subject: [PATCH 04/26] Disable other button --- .../main/java/org/key_project/slicing/ui/SlicingLeftPanel.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java index b4e43293fb5..fea94785fe4 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java @@ -620,6 +620,8 @@ private void updateUIState() { dotExport.setToolTipText(noProof); showGraphRendering.setEnabled(false); showGraphRendering.setToolTipText(noProof); + showGraphRenderingShort.setEnabled(false); + showGraphRenderingShort.setToolTipText(noProof); runAnalysis.setEnabled(false); runAnalysis.setToolTipText(noProof); showRuleStatistics.setEnabled(false); From 5059d725a8c7bb8d305232ec6ef3a033e765c6c6 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 5 Jun 2023 08:12:14 +0200 Subject: [PATCH 05/26] . --- .../key/gui/prooftree/GUIProofTreeModel.java | 41 ++-- .../gui/prooftree/ProofTreePopupFactory.java | 22 ++ .../ilkd/key/gui/prooftree/ProofTreeView.java | 16 +- .../reference/CloseReferenceExtension.java | 221 ++++++++++++++++++ .../ilkd/key/proof/reference/ClosedBy.java | 25 ++ .../proof/reference/ProgramMethodFinder.java | 36 +++ .../proof/reference/ReferenceSearcher.java | 95 ++++++++ 7 files changed, 428 insertions(+), 28 deletions(-) create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/proof/reference/CloseReferenceExtension.java create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java index 80137f701b6..a4b37ef6eeb 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java @@ -67,14 +67,16 @@ public GUIProofTreeModel(Proof p) { GoalListener goalListener = new GoalListener() { @Override - public void sequentChanged(Goal source, SequentChangeInfo sci) {} + public void sequentChanged(Goal source, SequentChangeInfo sci) { + } @Override - public void goalReplaced(Goal source, Node parent, ImmutableList newGoals) {} + public void goalReplaced(Goal source, Node parent, ImmutableList newGoals) { + } @Override public void automaticStateChanged(Goal source, boolean oldAutomatic, - boolean newAutomatic) { + boolean newAutomatic) { if (!batchGoalStateChange && ProofTreeViewFilter.HIDE_INTERACTIVE_GOALS.isActive()) { updateTree((TreeNode) null); @@ -200,8 +202,8 @@ public boolean isAttentive() { * Adds a listener for the TreeModelEvent posted after the tree changes. Such events are * generated whenever the underlying Proof changes. * - * @see #removeTreeModelListener * @param l the listener to add + * @see #removeTreeModelListener */ @Override public void addTreeModelListener(TreeModelListener l) { @@ -211,8 +213,8 @@ public void addTreeModelListener(TreeModelListener l) { /** * Removes a listener previously added with addTreeModelListener(). * - * @see #addTreeModelListener * @param l the listener to remove + * @see #addTreeModelListener */ @Override public void removeTreeModelListener(TreeModelListener l) { @@ -220,7 +222,6 @@ public void removeTreeModelListener(TreeModelListener l) { } /** - * * @return whether or not {@link ProofTreeViewFilter#HIDE_CLOSED_SUBTREES} is active. */ public boolean hideClosedSubtrees() { @@ -229,7 +230,6 @@ public boolean hideClosedSubtrees() { /** - * * @return whether or not {@link ProofTreeViewFilter#HIDE_INTERACTIVE_GOALS} is active. */ public boolean hideInteractiveGoals() { @@ -237,7 +237,6 @@ public boolean hideInteractiveGoals() { } /** - * * @return whether or nor one of {@link ProofTreeViewFilter#ALL_GLOBAL_FILTERS} is active. */ public boolean globalFilterActive() { @@ -245,18 +244,6 @@ public boolean globalFilterActive() { .anyMatch(ProofTreeViewFilter::isActive); } - /** - * Set filters active or inactive and update tree if necessary. - * - * @param filter - * @param active - */ - public void setFilter(ProofTreeViewFilter filter, boolean active) { - if (active != filter.isActive()) { - setFilterImmediately(filter, active); - } - } - /** * Set filters active or inactive and update tree if necessary. * Always updates the filter and the tree. @@ -264,15 +251,16 @@ public void setFilter(ProofTreeViewFilter filter, boolean active) { * @param filter the filter * @param active whether to activate the filter */ - public void setFilterImmediately(ProofTreeViewFilter filter, boolean active) { + public void setFilter(ProofTreeViewFilter filter, boolean active) { if (filter == null) { activeNodeFilter = null; updateTree((TreeNode) null); return; } if (!filter.global()) { - if (activeNodeFilter != null) + if (activeNodeFilter != null) { activeNodeFilter.setActive(false); + } activeNodeFilter = active ? (NodeFilter) filter : null; } filter.setActive(active); @@ -323,7 +311,6 @@ public int getChildCount(Object parent) { * @param parent a node in the tree, obtained from this data source * @param child a child of parent, obtained from this data source * @return The index of child in parent - * */ @Override public int getIndexOfChild(Object parent, Object child) { @@ -390,7 +377,7 @@ private void updateTree(TreeNode trn) { if (trn == null || trn == getRoot()) { // bigger change, redraw whole tree proofTreeNodes = new WeakHashMap<>(); branchNodes = new WeakHashMap<>(); - fireTreeStructureChanged(new Object[] { getRoot() }); + fireTreeStructureChanged(new Object[]{getRoot()}); return; } // otherwise redraw only a certain subtree @@ -474,7 +461,7 @@ protected void fireTreeStructureChanged(Object[] path) { // generated to represent the nodes resp. subtrees of the Proof. private WeakHashMap proofTreeNodes = - new WeakHashMap<>(); + new WeakHashMap<>(); private WeakHashMap branchNodes = new WeakHashMap<>(); /** @@ -519,7 +506,9 @@ public GUIBranchNode getBranchNode(Node n, Object label) { } - /** stores exactly the paths that are expanded in the proof tree */ + /** + * stores exactly the paths that are expanded in the proof tree + */ private @Nonnull Collection expansionState = Collections.emptySet(); public void setExpansionState(@Nonnull Collection c) { 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 index d70d2302d8d..899280bd6c1 100644 --- 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 @@ -22,6 +22,8 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.rule.OneStepSimplifierRuleApp; +import de.uka.ilkd.key.proof.reference.ClosedBy; +import de.uka.ilkd.key.proof.reference.ReferenceSearcher; import de.uka.ilkd.key.settings.GeneralSettings; import de.uka.ilkd.key.util.Pair; @@ -409,6 +411,26 @@ public void actionPerformed(ActionEvent e) { } } + static class CloseByReference extends ProofTreeAction { + public CloseByReference(ProofTreeContext context) { + super(context); + setName("Close by reference to other proof"); + setEnabled(context.invokedNode.leaf() && !context.invokedNode.isClosed()); + } + + @Override + public void actionPerformed(ActionEvent e) { + // search other proofs for matching nodes + ClosedBy c = ReferenceSearcher.findPreviousProof(context.mediator, context.invokedNode); + if (c != null) { + Node toClose = context.invokedNode; + Proof newProof = context.proof; + newProof.closeGoal(newProof.getGoal(toClose)); + toClose.register(c, ClosedBy.class); + } + } + } + static class DelayedCut extends ProofTreeAction { private static final long serialVersionUID = 2264044175802298829L; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java index bdef859bd08..54b4834dd25 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java @@ -32,6 +32,7 @@ import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.pp.PrettyPrinter; import de.uka.ilkd.key.proof.*; +import de.uka.ilkd.key.proof.reference.ClosedBy; import de.uka.ilkd.key.rule.RuleApp; import org.key_project.util.collection.ImmutableList; @@ -430,12 +431,15 @@ private void setProof(Proof p) { // Redraw the tree in case the ProofTreeViewFilters have changed // since the last time the proof was loaded. - delegateModel.setFilterImmediately(filter, filter != null && filter.isActive()); + delegateModel.setFilter(filter, filter != null && filter.isActive()); // Expand previously visible rows. for (int i : rowsToExpand) { delegateView.expandRow(i); } + if (filter != null) { + delegateModel.setFilter(filter, true); + } if (delegateModel.getSelection() != null) { delegateView.setSelectionPath(delegateModel.getSelection()); @@ -1008,9 +1012,17 @@ private void renderLeaf(Style style, GUIAbstractTreeNode node) { String toolTipText; if (goal == null || leaf.isClosed()) { + ClosedBy c = leaf.lookup(ClosedBy.class); + if (c != null) { + style.icon = IconFactory.BACKREFERENCE.get(iconHeight); + } else { + style.icon = IconFactory.keyHoleClosed(iconHeight); + } style.foreground = DARK_GREEN_COLOR.get(); - style.icon = IconFactory.keyHoleClosed(iconHeight); toolTipText = "A closed goal"; + if (c != null) { + toolTipText += " (by reference to other proof)"; + } } else if (goal.isLinked()) { style.foreground = PINK_COLOR.get(); style.icon = IconFactory.keyHoleLinked(20, 20); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/CloseReferenceExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/CloseReferenceExtension.java new file mode 100644 index 00000000000..3c85220aee0 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/CloseReferenceExtension.java @@ -0,0 +1,221 @@ +package de.uka.ilkd.key.proof.reference; + +import java.awt.event.ActionEvent; +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; +import java.util.Set; +import javax.annotation.Nonnull; +import javax.swing.*; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.core.KeYSelectionEvent; +import de.uka.ilkd.key.core.KeYSelectionListener; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.actions.KeyAction; +import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.ProofEvent; +import de.uka.ilkd.key.proof.RuleAppListener; +import de.uka.ilkd.key.proof.event.ProofDisposedEvent; +import de.uka.ilkd.key.proof.event.ProofDisposedListener; +import de.uka.ilkd.key.proof.io.IntermediateProofReplayer; +import de.uka.ilkd.key.settings.ProofIndependentSettings; + +import org.key_project.util.collection.ImmutableList; + +@KeYGuiExtension.Info(name = "Proof Caching", optional = true, + description = "Functionality related to reusing previous proof results in similar proofs", + experimental = false) +public class CloseReferenceExtension + implements KeYGuiExtension, KeYGuiExtension.Startup, KeYGuiExtension.ContextMenu, + KeYGuiExtension.Toolbar, + KeYSelectionListener, RuleAppListener, + ProofDisposedListener { + + private KeYMediator mediator; + + private final Set trackedProofs = new HashSet<>(); + + private static boolean ignoreRuleApplications = false; + + public static void setIgnoreRuleApplications(boolean ignoreRuleApplications) { + CloseReferenceExtension.ignoreRuleApplications = ignoreRuleApplications; + } + + @Override + public void selectedNodeChanged(KeYSelectionEvent e) { + } + + @Override + public void selectedProofChanged(KeYSelectionEvent e) { + Proof p = e.getSource().getSelectedProof(); + if (p == null || trackedProofs.contains(p)) { + return; + } + trackedProofs.add(p); + p.addRuleAppListener(this); + p.addProofDisposedListener(this); + } + + @Override + public void ruleApplied(ProofEvent e) { + if (e.getSource().lookup(CopyingProofReplayer.class) != null) { + return; // copy in progress! + } + if (!ProofIndependentSettings.DEFAULT_INSTANCE.getProofCachingSettings().getEnabled()) { + return; + } + Proof p = e.getSource(); + if (e.getRuleAppInfo().getOriginalNode().getNodeInfo().getInteractiveRuleApplication()) { + return; // only applies for automatic proof search + } + ImmutableList newGoals = e.getNewGoals(); + if (newGoals.size() <= 1) { + return; + } + for (Goal goal : newGoals) { + ClosedBy c = ReferenceSearcher.findPreviousProof(mediator.getCurrentlyOpenedProofs(), + goal.node()); + if (c != null) { + // p.closeGoal(goal); + goal.setEnabled(false); + + goal.node().register(c, ClosedBy.class); + c.getProof() + .addProofDisposedListener(new CopyBeforeDispose(mediator, c.getProof(), p)); + } + } + } + + @Override + public void init(MainWindow window, KeYMediator mediator) { + this.mediator = mediator; + mediator.addKeYSelectionListener(this); + } + + @Override + public void proofDisposing(ProofDisposedEvent e) { + trackedProofs.remove(e.getSource()); + } + + @Override + public void proofDisposed(ProofDisposedEvent e) { + + } + + @Nonnull + @Override + public List getContextActions(@Nonnull KeYMediator mediator, + @Nonnull ContextMenuKind kind, @Nonnull Object underlyingObject) { + if (kind.getType() == Node.class) { + return List.of(new CloseByReference(mediator, (Node) underlyingObject), + new CopyReferencedProof(mediator, (Node) underlyingObject)); + } + return new ArrayList<>(); + } + + @Nonnull + @Override + public JToolBar getToolbar(MainWindow mainWindow) { + JToolBar bar = new JToolBar(); + bar.add(new CopyStepsAction(mainWindow)); + return bar; + } + + /** + * Listener that ensures steps are copied before the referenced proof is disposed. + */ + private static class CopyBeforeDispose implements ProofDisposedListener { + + private final KeYMediator mediator; + private final Proof referencedProof; + private final Proof newProof; + + /** + * Construct new listener. + * + * @param referencedProof referenced proof + * @param newProof new proof + */ + CopyBeforeDispose(KeYMediator mediator, Proof referencedProof, Proof newProof) { + this.mediator = mediator; + this.referencedProof = referencedProof; + this.newProof = newProof; + } + + @Override + public void proofDisposing(ProofDisposedEvent e) { + if (!newProof.isDisposed()) { + mediator.stopInterface(true); + newProof.copyCachedGoals(referencedProof); + mediator.startInterface(true); + } + } + + @Override + public void proofDisposed(ProofDisposedEvent e) { + + } + } + + static class CloseByReference extends KeyAction { + private final KeYMediator mediator; + private final Node node; + + public CloseByReference(KeYMediator mediator, Node node) { + this.mediator = mediator; + this.node = node; + setName("Close by reference to other proof"); + setEnabled(node.leaf() && !node.isClosed()); + setMenuPath("Proof Caching"); + } + + @Override + public void actionPerformed(ActionEvent e) { + // search other proofs for matching nodes + ClosedBy c = ReferenceSearcher.findPreviousProof(mediator, node); + if (c != null) { + Node toClose = node; + Proof newProof = node.proof(); + // newProof.closeGoal(newProof.getGoal(toClose)); + toClose.register(c, ClosedBy.class); + } else { + JOptionPane.showMessageDialog((JComponent) e.getSource(), + "No matching branch found", "Proof Caching error", JOptionPane.WARNING_MESSAGE); + } + } + } + + static class CopyReferencedProof extends KeyAction { + private final KeYMediator mediator; + private final Node node; + + public CopyReferencedProof(KeYMediator mediator, Node node) { + this.mediator = mediator; + this.node = node; + setName("Copy referenced proof steps here"); + setEnabled(node.leaf() && !node.isClosed() + && node.lookup(ClosedBy.class) != null); + setMenuPath("Proof Caching"); + } + + @Override + public void actionPerformed(ActionEvent e) { + ClosedBy c = node.lookup(ClosedBy.class); + Goal current = node.proof().getGoal(node); + // node.proof().add(current); + // node.proof().reOpenGoal(current); + try { + // mediator.stopInterface(true); + new CopyingProofReplayer(c.getProof(), node.proof()).copy(c.getNode(), current); + // mediator.startInterface(true); + } catch (IntermediateProofReplayer.BuiltInConstructionException ex) { + throw new RuntimeException(ex); + } + } + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java new file mode 100644 index 00000000000..5f37e22068d --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java @@ -0,0 +1,25 @@ +package de.uka.ilkd.key.proof.reference; + +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; + +/** + * Indicates that a branch has been closed by "reference" to another closed proof. + * + * @author Arne Keller + */ +public class ClosedBy { + /** + * The proof referenced. + */ + private Proof proof; + /** + * The node referenced. + */ + private Node node; + + public ClosedBy(Proof proof, Node node) { + this.proof = proof; + this.node = node; + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java new file mode 100644 index 00000000000..ae69104c587 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java @@ -0,0 +1,36 @@ +package de.uka.ilkd.key.proof.reference; + +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.Visitor; +import de.uka.ilkd.key.logic.op.ProgramMethod; + +public class ProgramMethodFinder implements Visitor { + + private boolean foundProgramMethod = false; + + @Override + public boolean visitSubtree(Term visited) { + return false; + } + + @Override + public void visit(Term visited) { + if (visited.op() instanceof ProgramMethod) { + foundProgramMethod = true; + } + } + + @Override + public void subtreeEntered(Term subtreeRoot) { + + } + + @Override + public void subtreeLeft(Term subtreeRoot) { + + } + + public boolean getFoundProgramMethod() { + return foundProgramMethod; + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java new file mode 100644 index 00000000000..e7b95cb22a0 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java @@ -0,0 +1,95 @@ +package de.uka.ilkd.key.proof.reference; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.logic.Semisequent; +import de.uka.ilkd.key.logic.Sequent; +import de.uka.ilkd.key.logic.SequentFormula; +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.op.ProgramMethod; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; + +import java.util.Optional; + +public class ReferenceSearcher { + private ReferenceSearcher() { + + } + + public static ClosedBy findPreviousProof(KeYMediator mediator, Node newNode) { + // TODO: + // - disallow closing by reference to merged branch + // - once the other proof is closed, copy the steps into the new proof + // - when saving the new proof, copy the steps + // - compare sequents using the new equality infrastructure in the slicing branch + + // first verify that the new node does not contain any terms that depend on external + // influences + ProgramMethodFinder f = new ProgramMethodFinder(); + Sequent seq = newNode.sequent(); + for (int i = 1; i <= seq.size(); i++) { + Term term = seq.getFormulabyNr(i).formula(); + if (term.containsJavaBlockRecursive()) { + return null; + } + term.execPreOrder(f); + if (f.getFoundProgramMethod()) { + return null; + } + } + var proofs = mediator.getCurrentlyOpenedProofs(); + for (int i = 0; i < proofs.size(); i++) { + Proof p = proofs.get(i); + // only search in compatible proofs + if (!p.getSettings().getChoiceSettings() + .equals(newNode.proof().getSettings().getChoiceSettings())) { + continue; + } + Optional match = p.closedGoals().stream().map(goal -> { + // first, find the initial node in this branch + Node n = goal.node(); + while (n.parent() != null && n.parent().childrenCount() == 1) { + n = n.parent(); + } + return n; + }).filter(node -> { + // check that all formulas are also present in the new proof + Semisequent ante = node.sequent().antecedent(); + Semisequent succ = node.sequent().succedent(); + Semisequent anteNew = newNode.sequent().antecedent(); + Semisequent succNew = newNode.sequent().succedent(); + if (!containedIn(anteNew, ante) || !containedIn(succNew, succ)) { + return false; + } + return true; + }).findAny(); + if (match.isPresent()) { + return new ClosedBy(p, match.get()); + } + } + return null; + } + + /** + * Check whether all formulas in {@code subset} are conatined in {@code superset}. + * @param superset Semisequent supposed to contain {@code subset} + * @param subset Semisequent supposed to be in {@code superset} + * @return whether all formulas are present + */ + private static boolean containedIn(Semisequent superset, Semisequent subset) { + for (SequentFormula sf : subset) { + String sfString = sf.toString(); + boolean found = false; + for (SequentFormula sf2 : superset) { + if (sf2.toString().equals(sfString)) { + found = true; + break; + } + } + if (!found) { + return false; + } + } + return true; + } +} \ No newline at end of file From c2434ab4aecc7f75cf35a80d58b93288b10f9c40 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 5 Jun 2023 08:41:09 +0200 Subject: [PATCH 06/26] WIP reordering change --- .../de/uka/ilkd/key/proof/BranchLocation.java | 13 +++- .../main/java/de/uka/ilkd/key/proof/Node.java | 7 ++- .../proof/replay/AbstractProofReplayer.java | 2 +- .../main/java/de/uka/ilkd/key/util/Pair.java | 16 ++++- .../util/collection/ImmutableList.java | 34 +++++++++- .../org/key_project/slicing/ProofReorder.java | 62 +++++++++++++++---- .../slicing/ReorderingReplayer.java | 60 ++++++++++++++++++ .../key_project/slicing/SlicingExtension.java | 8 ++- 8 files changed, 184 insertions(+), 18 deletions(-) create mode 100644 keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/BranchLocation.java b/key.core/src/main/java/de/uka/ilkd/key/proof/BranchLocation.java index c1690ee9ca0..4ec960c9ab0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/BranchLocation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/BranchLocation.java @@ -14,7 +14,7 @@ * * @author Arne Keller */ -public class BranchLocation { +public class BranchLocation implements Comparable { /** * Branch location of the initial proof branch. */ @@ -168,4 +168,15 @@ public boolean equals(Object o) { public int hashCode() { return Objects.hash(location); } + + @Override + public int compareTo(BranchLocation other) { + if (this == BranchLocation.ROOT) { + return -1; + } else if (other == BranchLocation.ROOT) { + return 1; + } else { + return location.compareTo(other.location); + } + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java index dd9786b8a78..dceffc00ca5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java @@ -29,7 +29,7 @@ import org.key_project.util.collection.ImmutableSet; import org.key_project.util.lookup.Lookup; -public class Node implements Iterable { +public class Node implements Iterable, Comparable { private static final String RULE_WITHOUT_NAME = "rule without name"; private static final String RULE_APPLICATION_WITHOUT_RULE = "rule application without rule"; @@ -845,4 +845,9 @@ public Node getFirstInBranch() { } return candidate; } + + @Override + public int compareTo(Node node) { + return Integer.compare(this.serialNr, node.serialNr); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java index 16316f69658..53d26729875 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java @@ -64,7 +64,7 @@ public abstract class AbstractProofReplayer { /** * The new proof. */ - private final Proof proof; + protected final Proof proof; /** * Instantiate a new replayer. diff --git a/key.util/src/main/java/de/uka/ilkd/key/util/Pair.java b/key.util/src/main/java/de/uka/ilkd/key/util/Pair.java index 3f2b35c8bb6..f5c636780c3 100644 --- a/key.util/src/main/java/de/uka/ilkd/key/util/Pair.java +++ b/key.util/src/main/java/de/uka/ilkd/key/util/Pair.java @@ -11,7 +11,7 @@ * @param type of first element * @param type of second element */ -public class Pair { +public class Pair implements Comparable> { /** * First element. */ @@ -95,4 +95,18 @@ public static Set getSecondSet(Collection> pairs) { } return res; } + + @Override + public int compareTo(Pair other) { + if (this == other) { + return 0; + } + var a = (Comparable) this.first; + var b = (Comparable) this.second; + var value = a.compareTo(other.first); + if (value != 0) { + return value; + } + return b.compareTo(other.second); + } } diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java index 0b9aaceabe4..bd603d6e58f 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java @@ -11,7 +11,7 @@ /** * List interface to be implemented by non-destructive lists */ -public interface ImmutableList extends Iterable, java.io.Serializable { +public interface ImmutableList extends Iterable, java.io.Serializable, Comparable> { /** * Returns a Collector that accumulates the input elements into a new ImmutableList. @@ -351,4 +351,36 @@ default T last() { return remainder.head(); } + @Override + default int compareTo(ImmutableList other) { + if (this.isEmpty() && other.isEmpty()) { + return 0; + } else if (this.isEmpty()) { + return -1; + } else if (other.isEmpty()) { + return 1; + } else if (this.head().getClass() != other.head().getClass()) { + throw new IllegalStateException("tried to compare lists with elements of different classes"); + } else if (!(this.head() instanceof Comparable)) { + throw new IllegalStateException("tried to compare list with incomparable elements"); + } else { + var l1 = this; + var l2 = other; + while (true) { + if (l1.isEmpty()) { + return -1; + } else if (l2.isEmpty()) { + return 1; + } + var a = (Comparable) this.head(); + var b = (T) other.head(); + var value = a.compareTo(b); + if (value != 0) { + return value; + } + l1 = l1.tail(); + l2 = l2.tail(); + } + } + } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index 89c04df2186..e92b2475810 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -1,21 +1,23 @@ package org.key_project.slicing; -import java.util.ArrayDeque; -import java.util.ArrayList; -import java.util.Collections; -import java.util.Comparator; -import java.util.Deque; -import java.util.HashSet; -import java.util.List; -import java.util.Set; +import java.io.File; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.*; import java.util.stream.Collectors; +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.PosInTerm; import de.uka.ilkd.key.proof.BranchLocation; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.ProofAggregate; +import de.uka.ilkd.key.proof.init.ProofInputException; +import de.uka.ilkd.key.proof.io.*; import de.uka.ilkd.key.util.Pair; import org.key_project.slicing.graph.DependencyGraph; @@ -26,9 +28,11 @@ private ProofReorder() { } - public static void reorderProof(Proof proof, DependencyGraph depGraph) { + public static void reorderProof(Proof proof, DependencyGraph depGraph) throws IOException, ProofInputException, ProblemLoaderException, IntermediateProofReplayer.BuiltInConstructionException { MainWindow.getInstance().getMediator().stopInterface(true); + SortedMap> steps = new TreeMap<>(); + Set done = new HashSet<>(); Deque> todo = new ArrayDeque<>(); @@ -53,6 +57,7 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) { Set newOrderSorted = new HashSet<>(); while (!q.isEmpty()) { var nextNode = q.pop(); + List finalNewOrder = newOrder; depGraph.outgoingEdgesOf(nextNode).forEach(node -> { if (!node.getBranchLocation().equals(loc)) { todo.add(new Pair<>(node.getBranchLocation(), node.getFirstInBranch())); @@ -71,7 +76,7 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) { q.addLast(nextNode); return; } - newOrder.add(node); + finalNewOrder.add(node); newOrderSorted.add(node); var outputs = depGraph.outputsOf(node).collect(Collectors.toList()); @@ -79,6 +84,14 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) { outputs.forEach(q::addFirst); }); } + for (int i = 0; i < newOrder.size(); i++) { + if (newOrder.get(i).childrenCount() == 0) { + newOrder = newOrder.subList(0, i + 1); + break; + } + } + steps.put(loc, newOrder); + /* var firstNode = newOrder.stream().min(Comparator.comparing(Node::serialNr)).get(); var lastNode = newOrder.stream().max(Comparator.comparing(Node::serialNr)).get(); newOrder.remove(lastNode); @@ -115,9 +128,36 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) { last.removeChildren(); last.add(lastNode); } + */ } System.out.println("done!"); - MainWindow.getInstance().getMediator().startInterface(true); + + ProblemLoaderControl control = new DefaultUserInterfaceControl(); + Path tmpFile = Files.createTempFile("proof", ".proof"); + proof.saveProofObligationToFile(tmpFile.toFile()); + + String bootClassPath = proof.getEnv().getJavaModel().getBootClassPath(); + AbstractProblemLoader problemLoader = new SingleThreadProblemLoader( + tmpFile.toFile(), + proof.getEnv().getJavaModel().getClassPathEntries(), + bootClassPath != null ? new File(bootClassPath) : null, + null, + proof.getEnv().getInitConfigForEnvironment().getProfile(), + false, + control, false, null); + problemLoader.load(); + //Files.delete(tmpFile); + Proof newProof = problemLoader.getProof(); + new ReorderingReplayer(proof, newProof, steps).copy(); + newProof.saveToFile(tmpFile.toFile()); + KeYMediator mediator = MainWindow.getInstance().getMediator(); + mediator.startInterface(true); + + ProblemLoader problemLoader2 = + mediator.getUI().getProblemLoader(tmpFile.toFile(), null, null, null, mediator); + // user already knows about any warnings + problemLoader2.setIgnoreWarnings(true); + problemLoader2.runAsynchronously(); } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java b/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java new file mode 100644 index 00000000000..caf6e8192b2 --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java @@ -0,0 +1,60 @@ +package org.key_project.slicing; + +import java.io.File; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.*; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.proof.BranchLocation; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.init.ProofInputException; +import de.uka.ilkd.key.proof.io.*; +import de.uka.ilkd.key.proof.replay.AbstractProofReplayer; +import de.uka.ilkd.key.rule.OneStepSimplifier; + +import org.key_project.util.collection.ImmutableList; + +public class ReorderingReplayer extends AbstractProofReplayer { + + private final SortedMap> steps; + + public ReorderingReplayer(Proof originalProof, Proof proof, SortedMap> steps) throws IOException, ProofInputException, ProblemLoaderException { + super(originalProof, proof); + this.steps = steps; + } + + public void copy() + throws IntermediateProofReplayer.BuiltInConstructionException { + OneStepSimplifier.refreshOSS(proof); + Deque nodeQueue = new ArrayDeque<>(); + Deque queue = new ArrayDeque<>(); + queue.add(proof.getGoal(proof.root())); + + for (Map.Entry> e : steps.entrySet()) { + nodeQueue.addAll(e.getValue()); + } + + while (!nodeQueue.isEmpty()) { + Node nextNode = nodeQueue.pop(); + Goal nextGoal = queue.pop(); + System.out.println("working on goal " + nextGoal.node().serialNr()); + // skip nextNode if it is a closed goal + if (nextNode.getAppliedRuleApp() == null) { + continue; + } + proof.getServices().getNameRecorder().setProposals( + nextNode.getNameRecorder().getProposals()); + ImmutableList newGoals = reApplyRuleApp(nextNode, nextGoal); + List sortedGoals = newGoals.toList(); + Collections.reverse(sortedGoals); + for (Goal g : newGoals) { + //System.out.println("adding goal " + g.node().serialNr() +" to queue"); + queue.addFirst(g); + } + } + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index e841ec56f7f..8ac1afd95d2 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -185,8 +185,12 @@ public JToolBar getToolbar(MainWindow mainWindow) { b.setText("Reorder"); b.addActionListener(e -> { KeYMediator m = MainWindow.getInstance().getMediator(); - ProofReorder.reorderProof(m.getSelectedProof(), - trackers.get(m.getSelectedProof()).getDependencyGraph()); + try { + ProofReorder.reorderProof(m.getSelectedProof(), + trackers.get(m.getSelectedProof()).getDependencyGraph()); + } catch (Exception exc) { + exc.printStackTrace(); + } }); bar.add(b); return bar; From dcf2ae50ab59e8c832c050a5765141d949c5b82c Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 5 Jun 2023 08:43:22 +0200 Subject: [PATCH 07/26] . --- .../key/gui/plugins/caching/CloseReferenceExtension.java | 6 ++---- .../key/gui/plugins/caching/ReferenceSearchButton.java | 3 +-- .../key/proof/reference/CloseReferenceExtension.java | 9 +++++---- .../java/de/uka/ilkd/key/proof/reference/ClosedBy.java | 8 ++++++++ 4 files changed, 16 insertions(+), 10 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CloseReferenceExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CloseReferenceExtension.java index ee0456b9a6c..7b3bb189139 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CloseReferenceExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CloseReferenceExtension.java @@ -89,8 +89,7 @@ public void ruleApplied(ProofEvent e) { return; } for (Goal goal : newGoals) { - ClosedBy c = ReferenceSearcher.findPreviousProof(mediator.getCurrentlyOpenedProofs(), - goal.node()); + ClosedBy c = ReferenceSearcher.findPreviousProof(mediator, goal.node()); if (c != null) { // p.closeGoal(goal); goal.setEnabled(false); @@ -228,8 +227,7 @@ public CloseByReference(KeYMediator mediator, Node node) { @Override public void actionPerformed(ActionEvent e) { // search other proofs for matching nodes - ClosedBy c = ReferenceSearcher.findPreviousProof( - mediator.getCurrentlyOpenedProofs(), node); + ClosedBy c = ReferenceSearcher.findPreviousProof(mediator, node); if (c != null) { node.register(c, ClosedBy.class); } else { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java index dd588191733..9a2450c4992 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java @@ -55,8 +55,7 @@ public ReferenceSearchButton(KeYMediator mediator) { public void actionPerformed(ActionEvent e) { Proof p = mediator.getSelectedProof(); for (Goal goal : p.openEnabledGoals()) { - ClosedBy c = ReferenceSearcher.findPreviousProof(mediator.getCurrentlyOpenedProofs(), - goal.node()); + ClosedBy c = ReferenceSearcher.findPreviousProof(mediator, goal.node()); if (c != null) { // p.closeGoal(goal); goal.setEnabled(false); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/CloseReferenceExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/CloseReferenceExtension.java index 3c85220aee0..687e0014028 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/CloseReferenceExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/CloseReferenceExtension.java @@ -15,6 +15,7 @@ import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.gui.plugins.caching.CachingSettingsProvider; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; @@ -23,6 +24,7 @@ import de.uka.ilkd.key.proof.event.ProofDisposedEvent; import de.uka.ilkd.key.proof.event.ProofDisposedListener; import de.uka.ilkd.key.proof.io.IntermediateProofReplayer; +import de.uka.ilkd.key.proof.replay.CopyingProofReplayer; import de.uka.ilkd.key.settings.ProofIndependentSettings; import org.key_project.util.collection.ImmutableList; @@ -66,7 +68,7 @@ public void ruleApplied(ProofEvent e) { if (e.getSource().lookup(CopyingProofReplayer.class) != null) { return; // copy in progress! } - if (!ProofIndependentSettings.DEFAULT_INSTANCE.getProofCachingSettings().getEnabled()) { + if (!CachingSettingsProvider.getCachingSettings().getEnabled()) { return; } Proof p = e.getSource(); @@ -78,8 +80,7 @@ public void ruleApplied(ProofEvent e) { return; } for (Goal goal : newGoals) { - ClosedBy c = ReferenceSearcher.findPreviousProof(mediator.getCurrentlyOpenedProofs(), - goal.node()); + ClosedBy c = ReferenceSearcher.findPreviousProof(mediator, goal.node()); if (c != null) { // p.closeGoal(goal); goal.setEnabled(false); @@ -151,7 +152,7 @@ private static class CopyBeforeDispose implements ProofDisposedListener { public void proofDisposing(ProofDisposedEvent e) { if (!newProof.isDisposed()) { mediator.stopInterface(true); - newProof.copyCachedGoals(referencedProof); + newProof.copyCachedGoals(referencedProof, null, null); mediator.startInterface(true); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java index 5f37e22068d..9faa6fa490c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java @@ -22,4 +22,12 @@ public ClosedBy(Proof proof, Node node) { this.proof = proof; this.node = node; } + + public Proof getProof() { + return proof; + } + + public Node getNode() { + return node; + } } From 5ff832058e9bc79a197232c8e0c1716bf4c4fdf3 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sun, 11 Jun 2023 11:04:23 +0200 Subject: [PATCH 08/26] Fix proof reordering bugs --- .../de/uka/ilkd/key/logic/op/Function.java | 10 + .../key/nparser/builder/DefaultBuilder.java | 9 - .../ilkd/key/parser/DefaultTermParser.java | 2 +- .../main/java/de/uka/ilkd/key/proof/Goal.java | 3 + .../proof/replay/AbstractProofReplayer.java | 4 + .../caching/CloseReferenceExtension.java | 6 +- .../caching/ReferenceSearchButton.java | 3 +- .../key/gui/prooftree/GUIProofTreeModel.java | 6 +- .../gui/prooftree/ProofTreePopupFactory.java | 22 -- .../reference/CloseReferenceExtension.java | 222 ------------------ .../proof/reference/ReferenceSearcher.java | 95 -------- .../util/collection/ImmutableList.java | 6 +- .../slicing/DependencyTracker.java | 27 +++ .../org/key_project/slicing/ProofReorder.java | 70 ++---- .../slicing/ReorderingReplayer.java | 16 +- .../key_project/slicing/SlicingExtension.java | 2 +- 16 files changed, 81 insertions(+), 422 deletions(-) delete mode 100644 key.ui/src/main/java/de/uka/ilkd/key/proof/reference/CloseReferenceExtension.java delete mode 100644 key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java index 8626c1d4acf..6dcf4eaf67c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java @@ -3,6 +3,7 @@ import de.uka.ilkd.key.logic.Name; import de.uka.ilkd.key.logic.sort.NullSort; import de.uka.ilkd.key.logic.sort.Sort; +import de.uka.ilkd.key.proof.Node; import org.key_project.util.collection.ImmutableArray; @@ -15,6 +16,7 @@ public class Function extends AbstractSortedOperator { private final boolean unique; private final boolean skolemConstant; + private Node introducedBy = null; // ------------------------------------------------------------------------- @@ -130,4 +132,12 @@ public final String proofToString() { public Function rename(Name newName) { return new Function(newName, sort(), argSorts(), whereToBind(), unique, skolemConstant); } + + public void setIntroducedBy(Node introducedBy) { + this.introducedBy = introducedBy; + } + + public Node getIntroducedBy() { + return introducedBy; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java index 9194686da2b..66a93e24ff1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java @@ -3,7 +3,6 @@ import java.util.ArrayList; import java.util.Collection; import java.util.List; -import java.util.ResourceBundle; import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.Services; @@ -35,9 +34,6 @@ public class DefaultBuilder extends AbstractBuilder { public static final String LIMIT_SUFFIX = "$lmtd"; - private static final ResourceBundle bundle = - ResourceBundle.getBundle("de.uka.ilkd.key.nparser.builder.resources"); - protected final Services services; protected final NamespaceSet nss; @@ -120,11 +116,6 @@ public Sort visitArg_sorts_or_formula_helper(KeYParser.Arg_sorts_or_formula_help } } - /* - * @Override public Sort visitAny_sortId(KeYParser.Any_sortIdContext ctx) { Pair p = - * accept(ctx.any_sortId_help()); return toArraySort(p, ctx.EMPTYBRACKETS().size()); } - */ - /** * looks up a function, (program) variable or static query of the given name varfunc_id and the * argument terms args in the namespaces and java info. diff --git a/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java b/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java index 49912041478..1961d1baece 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java @@ -26,7 +26,7 @@ * @author weigl * @deprecated Use the facade new KeyIO(services).parseTerm directly */ -@Deprecated // java11:(forRemoval = true, since = "2.8.0") +@Deprecated(forRemoval = true, since = "2.8.0") public final class DefaultTermParser { /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java index c56a09a6108..dc40e35c9c9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java @@ -665,6 +665,9 @@ private void adaptNamespacesNewGoals(final ImmutableList goalList) { boolean first = true; for (Goal goal : goalList) { goal.node().addLocalProgVars(newProgVars); + for (Function f : newFunctions) { + f.setIntroducedBy(goal.node().parent()); + } goal.node().addLocalFunctions(newFunctions); if (first) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java index 53d26729875..b8cdc9d0aef 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java @@ -89,6 +89,9 @@ protected ImmutableList reApplyRuleApp(Node node, Goal openGoal) throws IntermediateProofReplayer.BuiltInConstructionException { RuleApp ruleApp = node.getAppliedRuleApp(); ImmutableList nextGoals; + System.out.println( + "reapplying " + node.serialNr() + " " + node.getAppliedRuleApp().rule().displayName() + + " on node " + openGoal.node().serialNr()); if (ruleApp.rule() instanceof BuiltInRule) { IBuiltInRuleApp builtInRuleApp = constructBuiltinApp(node, openGoal); if (!builtInRuleApp.complete()) { @@ -312,6 +315,7 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) { } if (!ourApp.complete()) { + System.out.println("incomplete!"); ourApp = ourApp.tryToInstantiate(proof.getServices()); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CloseReferenceExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CloseReferenceExtension.java index 7b3bb189139..04243785ca0 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CloseReferenceExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CloseReferenceExtension.java @@ -89,7 +89,8 @@ public void ruleApplied(ProofEvent e) { return; } for (Goal goal : newGoals) { - ClosedBy c = ReferenceSearcher.findPreviousProof(mediator, goal.node()); + ClosedBy c = ReferenceSearcher.findPreviousProof(mediator.getCurrentlyOpenedProofs(), + goal.node()); if (c != null) { // p.closeGoal(goal); goal.setEnabled(false); @@ -227,7 +228,8 @@ public CloseByReference(KeYMediator mediator, Node node) { @Override public void actionPerformed(ActionEvent e) { // search other proofs for matching nodes - ClosedBy c = ReferenceSearcher.findPreviousProof(mediator, node); + ClosedBy c = + ReferenceSearcher.findPreviousProof(mediator.getCurrentlyOpenedProofs(), node); if (c != null) { node.register(c, ClosedBy.class); } else { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java index 9a2450c4992..dd588191733 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java @@ -55,7 +55,8 @@ public ReferenceSearchButton(KeYMediator mediator) { public void actionPerformed(ActionEvent e) { Proof p = mediator.getSelectedProof(); for (Goal goal : p.openEnabledGoals()) { - ClosedBy c = ReferenceSearcher.findPreviousProof(mediator, goal.node()); + ClosedBy c = ReferenceSearcher.findPreviousProof(mediator.getCurrentlyOpenedProofs(), + goal.node()); if (c != null) { // p.closeGoal(goal); goal.setEnabled(false); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java index a4b37ef6eeb..a25a2227f97 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java @@ -76,7 +76,7 @@ public void goalReplaced(Goal source, Node parent, ImmutableList newGoals) @Override public void automaticStateChanged(Goal source, boolean oldAutomatic, - boolean newAutomatic) { + boolean newAutomatic) { if (!batchGoalStateChange && ProofTreeViewFilter.HIDE_INTERACTIVE_GOALS.isActive()) { updateTree((TreeNode) null); @@ -377,7 +377,7 @@ private void updateTree(TreeNode trn) { if (trn == null || trn == getRoot()) { // bigger change, redraw whole tree proofTreeNodes = new WeakHashMap<>(); branchNodes = new WeakHashMap<>(); - fireTreeStructureChanged(new Object[]{getRoot()}); + fireTreeStructureChanged(new Object[] { getRoot() }); return; } // otherwise redraw only a certain subtree @@ -461,7 +461,7 @@ protected void fireTreeStructureChanged(Object[] path) { // generated to represent the nodes resp. subtrees of the Proof. private WeakHashMap proofTreeNodes = - new WeakHashMap<>(); + new WeakHashMap<>(); private WeakHashMap branchNodes = new WeakHashMap<>(); /** 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 index 0f6f4264b97..7e4f6b4b70b 100644 --- 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 @@ -22,8 +22,6 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.rule.OneStepSimplifierRuleApp; -import de.uka.ilkd.key.proof.reference.ClosedBy; -import de.uka.ilkd.key.proof.reference.ReferenceSearcher; import de.uka.ilkd.key.settings.GeneralSettings; import de.uka.ilkd.key.util.Pair; @@ -412,26 +410,6 @@ public void actionPerformed(ActionEvent e) { } } - static class CloseByReference extends ProofTreeAction { - public CloseByReference(ProofTreeContext context) { - super(context); - setName("Close by reference to other proof"); - setEnabled(context.invokedNode.leaf() && !context.invokedNode.isClosed()); - } - - @Override - public void actionPerformed(ActionEvent e) { - // search other proofs for matching nodes - ClosedBy c = ReferenceSearcher.findPreviousProof(context.mediator, context.invokedNode); - if (c != null) { - Node toClose = context.invokedNode; - Proof newProof = context.proof; - newProof.closeGoal(newProof.getGoal(toClose)); - toClose.register(c, ClosedBy.class); - } - } - } - static class DelayedCut extends ProofTreeAction { private static final long serialVersionUID = 2264044175802298829L; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/CloseReferenceExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/CloseReferenceExtension.java deleted file mode 100644 index 687e0014028..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/CloseReferenceExtension.java +++ /dev/null @@ -1,222 +0,0 @@ -package de.uka.ilkd.key.proof.reference; - -import java.awt.event.ActionEvent; -import java.util.ArrayList; -import java.util.HashSet; -import java.util.List; -import java.util.Set; -import javax.annotation.Nonnull; -import javax.swing.*; - -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; -import de.uka.ilkd.key.gui.MainWindow; -import de.uka.ilkd.key.gui.actions.KeyAction; -import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; -import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; -import de.uka.ilkd.key.gui.plugins.caching.CachingSettingsProvider; -import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.proof.Node; -import de.uka.ilkd.key.proof.Proof; -import de.uka.ilkd.key.proof.ProofEvent; -import de.uka.ilkd.key.proof.RuleAppListener; -import de.uka.ilkd.key.proof.event.ProofDisposedEvent; -import de.uka.ilkd.key.proof.event.ProofDisposedListener; -import de.uka.ilkd.key.proof.io.IntermediateProofReplayer; -import de.uka.ilkd.key.proof.replay.CopyingProofReplayer; -import de.uka.ilkd.key.settings.ProofIndependentSettings; - -import org.key_project.util.collection.ImmutableList; - -@KeYGuiExtension.Info(name = "Proof Caching", optional = true, - description = "Functionality related to reusing previous proof results in similar proofs", - experimental = false) -public class CloseReferenceExtension - implements KeYGuiExtension, KeYGuiExtension.Startup, KeYGuiExtension.ContextMenu, - KeYGuiExtension.Toolbar, - KeYSelectionListener, RuleAppListener, - ProofDisposedListener { - - private KeYMediator mediator; - - private final Set trackedProofs = new HashSet<>(); - - private static boolean ignoreRuleApplications = false; - - public static void setIgnoreRuleApplications(boolean ignoreRuleApplications) { - CloseReferenceExtension.ignoreRuleApplications = ignoreRuleApplications; - } - - @Override - public void selectedNodeChanged(KeYSelectionEvent e) { - } - - @Override - public void selectedProofChanged(KeYSelectionEvent e) { - Proof p = e.getSource().getSelectedProof(); - if (p == null || trackedProofs.contains(p)) { - return; - } - trackedProofs.add(p); - p.addRuleAppListener(this); - p.addProofDisposedListener(this); - } - - @Override - public void ruleApplied(ProofEvent e) { - if (e.getSource().lookup(CopyingProofReplayer.class) != null) { - return; // copy in progress! - } - if (!CachingSettingsProvider.getCachingSettings().getEnabled()) { - return; - } - Proof p = e.getSource(); - if (e.getRuleAppInfo().getOriginalNode().getNodeInfo().getInteractiveRuleApplication()) { - return; // only applies for automatic proof search - } - ImmutableList newGoals = e.getNewGoals(); - if (newGoals.size() <= 1) { - return; - } - for (Goal goal : newGoals) { - ClosedBy c = ReferenceSearcher.findPreviousProof(mediator, goal.node()); - if (c != null) { - // p.closeGoal(goal); - goal.setEnabled(false); - - goal.node().register(c, ClosedBy.class); - c.getProof() - .addProofDisposedListener(new CopyBeforeDispose(mediator, c.getProof(), p)); - } - } - } - - @Override - public void init(MainWindow window, KeYMediator mediator) { - this.mediator = mediator; - mediator.addKeYSelectionListener(this); - } - - @Override - public void proofDisposing(ProofDisposedEvent e) { - trackedProofs.remove(e.getSource()); - } - - @Override - public void proofDisposed(ProofDisposedEvent e) { - - } - - @Nonnull - @Override - public List getContextActions(@Nonnull KeYMediator mediator, - @Nonnull ContextMenuKind kind, @Nonnull Object underlyingObject) { - if (kind.getType() == Node.class) { - return List.of(new CloseByReference(mediator, (Node) underlyingObject), - new CopyReferencedProof(mediator, (Node) underlyingObject)); - } - return new ArrayList<>(); - } - - @Nonnull - @Override - public JToolBar getToolbar(MainWindow mainWindow) { - JToolBar bar = new JToolBar(); - bar.add(new CopyStepsAction(mainWindow)); - return bar; - } - - /** - * Listener that ensures steps are copied before the referenced proof is disposed. - */ - private static class CopyBeforeDispose implements ProofDisposedListener { - - private final KeYMediator mediator; - private final Proof referencedProof; - private final Proof newProof; - - /** - * Construct new listener. - * - * @param referencedProof referenced proof - * @param newProof new proof - */ - CopyBeforeDispose(KeYMediator mediator, Proof referencedProof, Proof newProof) { - this.mediator = mediator; - this.referencedProof = referencedProof; - this.newProof = newProof; - } - - @Override - public void proofDisposing(ProofDisposedEvent e) { - if (!newProof.isDisposed()) { - mediator.stopInterface(true); - newProof.copyCachedGoals(referencedProof, null, null); - mediator.startInterface(true); - } - } - - @Override - public void proofDisposed(ProofDisposedEvent e) { - - } - } - - static class CloseByReference extends KeyAction { - private final KeYMediator mediator; - private final Node node; - - public CloseByReference(KeYMediator mediator, Node node) { - this.mediator = mediator; - this.node = node; - setName("Close by reference to other proof"); - setEnabled(node.leaf() && !node.isClosed()); - setMenuPath("Proof Caching"); - } - - @Override - public void actionPerformed(ActionEvent e) { - // search other proofs for matching nodes - ClosedBy c = ReferenceSearcher.findPreviousProof(mediator, node); - if (c != null) { - Node toClose = node; - Proof newProof = node.proof(); - // newProof.closeGoal(newProof.getGoal(toClose)); - toClose.register(c, ClosedBy.class); - } else { - JOptionPane.showMessageDialog((JComponent) e.getSource(), - "No matching branch found", "Proof Caching error", JOptionPane.WARNING_MESSAGE); - } - } - } - - static class CopyReferencedProof extends KeyAction { - private final KeYMediator mediator; - private final Node node; - - public CopyReferencedProof(KeYMediator mediator, Node node) { - this.mediator = mediator; - this.node = node; - setName("Copy referenced proof steps here"); - setEnabled(node.leaf() && !node.isClosed() - && node.lookup(ClosedBy.class) != null); - setMenuPath("Proof Caching"); - } - - @Override - public void actionPerformed(ActionEvent e) { - ClosedBy c = node.lookup(ClosedBy.class); - Goal current = node.proof().getGoal(node); - // node.proof().add(current); - // node.proof().reOpenGoal(current); - try { - // mediator.stopInterface(true); - new CopyingProofReplayer(c.getProof(), node.proof()).copy(c.getNode(), current); - // mediator.startInterface(true); - } catch (IntermediateProofReplayer.BuiltInConstructionException ex) { - throw new RuntimeException(ex); - } - } - } -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java deleted file mode 100644 index e7b95cb22a0..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java +++ /dev/null @@ -1,95 +0,0 @@ -package de.uka.ilkd.key.proof.reference; - -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.logic.Semisequent; -import de.uka.ilkd.key.logic.Sequent; -import de.uka.ilkd.key.logic.SequentFormula; -import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.op.ProgramMethod; -import de.uka.ilkd.key.proof.Node; -import de.uka.ilkd.key.proof.Proof; - -import java.util.Optional; - -public class ReferenceSearcher { - private ReferenceSearcher() { - - } - - public static ClosedBy findPreviousProof(KeYMediator mediator, Node newNode) { - // TODO: - // - disallow closing by reference to merged branch - // - once the other proof is closed, copy the steps into the new proof - // - when saving the new proof, copy the steps - // - compare sequents using the new equality infrastructure in the slicing branch - - // first verify that the new node does not contain any terms that depend on external - // influences - ProgramMethodFinder f = new ProgramMethodFinder(); - Sequent seq = newNode.sequent(); - for (int i = 1; i <= seq.size(); i++) { - Term term = seq.getFormulabyNr(i).formula(); - if (term.containsJavaBlockRecursive()) { - return null; - } - term.execPreOrder(f); - if (f.getFoundProgramMethod()) { - return null; - } - } - var proofs = mediator.getCurrentlyOpenedProofs(); - for (int i = 0; i < proofs.size(); i++) { - Proof p = proofs.get(i); - // only search in compatible proofs - if (!p.getSettings().getChoiceSettings() - .equals(newNode.proof().getSettings().getChoiceSettings())) { - continue; - } - Optional match = p.closedGoals().stream().map(goal -> { - // first, find the initial node in this branch - Node n = goal.node(); - while (n.parent() != null && n.parent().childrenCount() == 1) { - n = n.parent(); - } - return n; - }).filter(node -> { - // check that all formulas are also present in the new proof - Semisequent ante = node.sequent().antecedent(); - Semisequent succ = node.sequent().succedent(); - Semisequent anteNew = newNode.sequent().antecedent(); - Semisequent succNew = newNode.sequent().succedent(); - if (!containedIn(anteNew, ante) || !containedIn(succNew, succ)) { - return false; - } - return true; - }).findAny(); - if (match.isPresent()) { - return new ClosedBy(p, match.get()); - } - } - return null; - } - - /** - * Check whether all formulas in {@code subset} are conatined in {@code superset}. - * @param superset Semisequent supposed to contain {@code subset} - * @param subset Semisequent supposed to be in {@code superset} - * @return whether all formulas are present - */ - private static boolean containedIn(Semisequent superset, Semisequent subset) { - for (SequentFormula sf : subset) { - String sfString = sf.toString(); - boolean found = false; - for (SequentFormula sf2 : superset) { - if (sf2.toString().equals(sfString)) { - found = true; - break; - } - } - if (!found) { - return false; - } - } - return true; - } -} \ No newline at end of file diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java index bd603d6e58f..731fb8486ca 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java @@ -11,7 +11,8 @@ /** * List interface to be implemented by non-destructive lists */ -public interface ImmutableList extends Iterable, java.io.Serializable, Comparable> { +public interface ImmutableList + extends Iterable, java.io.Serializable, Comparable> { /** * Returns a Collector that accumulates the input elements into a new ImmutableList. @@ -360,7 +361,8 @@ default int compareTo(ImmutableList other) { } else if (other.isEmpty()) { return 1; } else if (this.head().getClass() != other.head().getClass()) { - throw new IllegalStateException("tried to compare lists with elements of different classes"); + throw new IllegalStateException( + "tried to compare lists with elements of different classes"); } else if (!(this.head() instanceof Comparable)) { throw new IllegalStateException("tried to compare list with incomparable elements"); } else { diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java index f837e8eba6e..3938601f0de 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java @@ -9,6 +9,8 @@ import java.util.stream.Stream; import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.op.Function; import de.uka.ilkd.key.proof.BranchLocation; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; @@ -155,6 +157,31 @@ private List> inputsOfNode(Node n, Set } } + // determine for each instantiated schema variable which node first introduced that variable + if (ruleApp instanceof TacletApp) { + TacletApp t = (TacletApp) ruleApp; + var it = t.instantiations().pairIterator(); + while (it.hasNext()) { + var x = it.next(); + var y = x.value(); + var z = y.getInstantiation(); + if (z instanceof Term) { + z = ((Term) z).op(); + } + if (z instanceof Function) { + var a = ((Function) z).getIntroducedBy(); + if (a != null && a != n) { + graph.outputsOf(a).forEach(i -> { + input.add(new Pair<>(i, false)); + // TODO: not strictly necessary if the Function is used in one of the + // previous inputs + // e.g. applyEq + }); + } + } + } + } + return input; } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index e92b2475810..d538b04bc98 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -15,7 +15,6 @@ import de.uka.ilkd.key.proof.BranchLocation; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; -import de.uka.ilkd.key.proof.ProofAggregate; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.proof.io.*; import de.uka.ilkd.key.util.Pair; @@ -28,7 +27,9 @@ private ProofReorder() { } - public static void reorderProof(Proof proof, DependencyGraph depGraph) throws IOException, ProofInputException, ProblemLoaderException, IntermediateProofReplayer.BuiltInConstructionException { + public static void reorderProof(Proof proof, DependencyGraph depGraph) + throws IOException, ProofInputException, ProblemLoaderException, + IntermediateProofReplayer.BuiltInConstructionException { MainWindow.getInstance().getMediator().stopInterface(true); SortedMap> steps = new TreeMap<>(); @@ -41,7 +42,6 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) throws IO var t = todo.pop(); var root = t.second; var loc = t.first; - System.out.println("copying " + loc); if (done.contains(loc)) { continue; } @@ -85,69 +85,31 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) throws IO }); } for (int i = 0; i < newOrder.size(); i++) { - if (newOrder.get(i).childrenCount() == 0) { - newOrder = newOrder.subList(0, i + 1); + if (newOrder.get(i).childrenCount() != 1 + || newOrder.get(i).child(0).childrenCount() == 0) { + var last = newOrder.remove(i); + newOrder.add(last); break; } } steps.put(loc, newOrder); - /* - var firstNode = newOrder.stream().min(Comparator.comparing(Node::serialNr)).get(); - var lastNode = newOrder.stream().max(Comparator.comparing(Node::serialNr)).get(); - newOrder.remove(lastNode); - Node closingNode = null; - for (int i = 0; i < newOrder.size(); i++) { - if (newOrder.get(i).childrenCount() == 0) { - closingNode = newOrder.get(i); - } - newOrder.get(i).removeChildren(); - } - // done, reorder proof steps now - Node last = firstNode.parent(); - for (Node next : newOrder) { - if (last != null) { - if (last.childrenCount() > 1) { - for (int i = 0; i < last.childrenCount(); i++) { - if (last.child(i).getBranchLocation() == loc) { - last.replaceChild(i, next); - break; - } - } - } else { - last.removeChildren(); - if (last == closingNode) { - last = null; - break; - } - last.add(next); - } - } - last = next; - } - if (last != null) { - last.removeChildren(); - last.add(lastNode); - } - */ } - System.out.println("done!"); - ProblemLoaderControl control = new DefaultUserInterfaceControl(); Path tmpFile = Files.createTempFile("proof", ".proof"); proof.saveProofObligationToFile(tmpFile.toFile()); String bootClassPath = proof.getEnv().getJavaModel().getBootClassPath(); AbstractProblemLoader problemLoader = new SingleThreadProblemLoader( - tmpFile.toFile(), - proof.getEnv().getJavaModel().getClassPathEntries(), - bootClassPath != null ? new File(bootClassPath) : null, - null, - proof.getEnv().getInitConfigForEnvironment().getProfile(), - false, - control, false, null); + tmpFile.toFile(), + proof.getEnv().getJavaModel().getClassPathEntries(), + bootClassPath != null ? new File(bootClassPath) : null, + null, + proof.getEnv().getInitConfigForEnvironment().getProfile(), + false, + control, false, null); problemLoader.load(); - //Files.delete(tmpFile); + // Files.delete(tmpFile); Proof newProof = problemLoader.getProof(); new ReorderingReplayer(proof, newProof, steps).copy(); newProof.saveToFile(tmpFile.toFile()); @@ -155,7 +117,7 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) throws IO mediator.startInterface(true); ProblemLoader problemLoader2 = - mediator.getUI().getProblemLoader(tmpFile.toFile(), null, null, null, mediator); + mediator.getUI().getProblemLoader(tmpFile.toFile(), null, null, null, mediator); // user already knows about any warnings problemLoader2.setIgnoreWarnings(true); problemLoader2.runAsynchronously(); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java b/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java index caf6e8192b2..c9f05c9f215 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java @@ -1,17 +1,11 @@ package org.key_project.slicing; -import java.io.File; -import java.io.IOException; -import java.nio.file.Files; -import java.nio.file.Path; import java.util.*; -import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.proof.BranchLocation; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; -import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.proof.io.*; import de.uka.ilkd.key.proof.replay.AbstractProofReplayer; import de.uka.ilkd.key.rule.OneStepSimplifier; @@ -22,7 +16,8 @@ public class ReorderingReplayer extends AbstractProofReplayer { private final SortedMap> steps; - public ReorderingReplayer(Proof originalProof, Proof proof, SortedMap> steps) throws IOException, ProofInputException, ProblemLoaderException { + public ReorderingReplayer(Proof originalProof, Proof proof, + SortedMap> steps) { super(originalProof, proof); this.steps = steps; } @@ -41,18 +36,19 @@ public void copy() while (!nodeQueue.isEmpty()) { Node nextNode = nodeQueue.pop(); Goal nextGoal = queue.pop(); - System.out.println("working on goal " + nextGoal.node().serialNr()); // skip nextNode if it is a closed goal if (nextNode.getAppliedRuleApp() == null) { continue; } proof.getServices().getNameRecorder().setProposals( - nextNode.getNameRecorder().getProposals()); + nextNode.getNameRecorder().getProposals()); ImmutableList newGoals = reApplyRuleApp(nextNode, nextGoal); List sortedGoals = newGoals.toList(); Collections.reverse(sortedGoals); for (Goal g : newGoals) { - //System.out.println("adding goal " + g.node().serialNr() +" to queue"); + if (g.node().isClosed()) { + continue; + } queue.addFirst(g); } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index 8ac1afd95d2..81e35f505d7 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -187,7 +187,7 @@ public JToolBar getToolbar(MainWindow mainWindow) { KeYMediator m = MainWindow.getInstance().getMediator(); try { ProofReorder.reorderProof(m.getSelectedProof(), - trackers.get(m.getSelectedProof()).getDependencyGraph()); + trackers.get(m.getSelectedProof()).getDependencyGraph()); } catch (Exception exc) { exc.printStackTrace(); } From ff7df0739e9be116e1d88d85f974d9a6d10327b3 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sun, 11 Jun 2023 19:07:53 +0200 Subject: [PATCH 09/26] Regroup rules based on heuristics --- .../main/java/de/uka/ilkd/key/proof/Node.java | 19 ++++ .../ilkd/key/gui/prooftree/GUIBranchNode.java | 16 +++- .../key/gui/prooftree/GUIProofTreeModel.java | 2 +- .../key/gui/prooftree/GUIProofTreeNode.java | 25 ++++- .../org/key_project/slicing/ProofRegroup.java | 93 +++++++++++++++++++ .../key_project/slicing/SlicingExtension.java | 11 +++ 6 files changed, 160 insertions(+), 6 deletions(-) create mode 100644 keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java index dceffc00ca5..c5d491660c2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java @@ -109,6 +109,9 @@ public class Node implements Iterable, Comparable { @Nullable private Lookup userData = null; + private List group = null; + private boolean hideInProofTree = false; + /** * If the rule base has been extended e.g. by loading a new taclet as lemma or by applying a @@ -846,6 +849,22 @@ public Node getFirstInBranch() { return candidate; } + public List getGroup() { + return group; + } + + public void setGroup(List group) { + this.group = group; + } + + public boolean isHideInProofTree() { + return hideInProofTree; + } + + public void setHideInProofTree(boolean hideInProofTree) { + this.hideInProofTree = hideInProofTree; + } + @Override public int compareTo(Node node) { return Integer.compare(this.serialNr, node.serialNr); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIBranchNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIBranchNode.java index 33b65aa6989..78fd8d0c254 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIBranchNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIBranchNode.java @@ -54,7 +54,10 @@ private void fillChildrenCache() { while (true) { childrenCache[count] = getProofTreeModel().getProofTreeNode(n); count++; - final Node nextN = findChild(n); + Node nextN = findChild(n); + while (nextN != null && nextN.isHideInProofTree()) { + nextN = findChild(nextN); + } if (nextN == null) { break; } @@ -62,7 +65,8 @@ private void fillChildrenCache() { } for (int i = 0; i != n.childrenCount(); ++i) { - if (!ProofTreeViewFilter.hiddenByGlobalFilters(n.child(i))) { + if (!ProofTreeViewFilter.hiddenByGlobalFilters(n.child(i)) + && !n.child(i).isHideInProofTree()) { childrenCache[count] = findBranch(n.child(i)); count++; } @@ -97,7 +101,10 @@ private int getChildCountHelp() { while (true) { count++; - final Node nextN = findChild(n); + Node nextN = findChild(n); + while (nextN != null && nextN.isHideInProofTree()) { + nextN = findChild(nextN); + } if (nextN == null) { break; } @@ -105,7 +112,8 @@ private int getChildCountHelp() { } for (int i = 0; i != n.childrenCount(); ++i) { - if (!ProofTreeViewFilter.hiddenByGlobalFilters(n.child(i))) { + if (!ProofTreeViewFilter.hiddenByGlobalFilters(n.child(i)) + && !n.child(i).isHideInProofTree()) { count++; } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java index a25a2227f97..99d2603f966 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java @@ -478,7 +478,7 @@ public GUIAbstractTreeNode find(Node n) { public GUIAbstractTreeNode getProofTreeNode(Node n) { GUIAbstractTreeNode res = find(n); if (res == null) { - res = new GUIProofTreeNode(this, n); + res = new GUIProofTreeNode(this, n, false); proofTreeNodes.put(n, res); } return res; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java index 476dfa9bd1d..878af3704d6 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java @@ -3,6 +3,7 @@ * this class implements a TreeModel that can be displayed using the JTree class framework */ +import java.util.List; import javax.annotation.Nonnull; import javax.swing.tree.TreeNode; @@ -13,9 +14,11 @@ class GUIProofTreeNode extends GUIAbstractTreeNode { private GUIAbstractTreeNode[] children; + private boolean leaf; - public GUIProofTreeNode(GUIProofTreeModel tree, Node node) { + public GUIProofTreeNode(GUIProofTreeModel tree, Node node, boolean leaf) { super(tree, node); + this.leaf = leaf; } public TreeNode getChildAt(int childIndex) { @@ -33,6 +36,13 @@ public TreeNode getParent() { if (n == null) { return null; } + if (n.isHideInProofTree()) { + // "parent" TreeNode is another proof node + while (n.parent() != null && n.getGroup() == null) { + n = n.parent(); + } + return findBranch(n); + } while (n.parent() != null && findChild(n.parent()) != null) { n = n.parent(); } @@ -62,6 +72,11 @@ public String toString() { */ private void ensureChildrenArray() { if (children == null) { + if (leaf) { + children = new GUIAbstractTreeNode[0]; + return; + } + Node node = getNode(); if (node != null && node.getAppliedRuleApp() instanceof OneStepSimplifierRuleApp) { Protocol protocol = @@ -74,6 +89,14 @@ private void ensureChildrenArray() { } return; } + } else if (node != null && node.getGroup() != null) { + System.out.println("setting up children array of grouped node"); + List group = node.getGroup(); + children = new GUIAbstractTreeNode[group.size()]; + for (int i = 0; i < group.size(); i++) { + children[i] = new GUIProofTreeNode(getProofTreeModel(), group.get(i), true); + } + return; } // otherwise diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java new file mode 100644 index 00000000000..329010a021a --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java @@ -0,0 +1,93 @@ +package org.key_project.slicing; + +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Deque; +import java.util.List; + +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.Rule; +import de.uka.ilkd.key.rule.RuleApp; +import de.uka.ilkd.key.rule.Taclet; + +public final class ProofRegroup { + private static final List> GROUPS = + List.of(List.of("alpha", "delta"), List.of("negationNormalForm", "conjNormalForm"), + List.of("polySimp_expand", "polySimp_normalise", "polySimp_newSym", + "polySimp_pullOutGcd", "polySimp_applyEq", "polySimp_applyEqRigid", + "simplify_literals")); + + public static void regroupProof(Proof proof) { + /* + * alpha, delta + * negationNormalForm, conjNormalForm + * polySimp_*, inEqSimp_*, simplify_literals + * + * simplify_enlarging, simplify, simplify_select + */ + Deque q = new ArrayDeque<>(); + q.add(proof.root()); + while (!q.isEmpty()) { + Node n = q.pop(); + if (n.childrenCount() == 0) { + continue; + } + RuleApp r = n.getAppliedRuleApp(); + if (r == null) { + continue; + } + Rule rule = r.rule(); + if (rule instanceof Taclet) { + var ruleSets = ((Taclet) rule).getRuleSets(); + int matchingGroup = -1; + for (var name : ruleSets) { + for (int i = 0; i < GROUPS.size(); i++) { + if (GROUPS.get(i).contains(name.toString())) { + matchingGroup = i; + break; + } + } + } + if (matchingGroup != -1) { + List group = new ArrayList<>(); + group.add(n); + while (true) { + if (n.childrenCount() != 1) { + break; + } + var n2 = n.child(0); + var rule2 = n2.getAppliedRuleApp().rule(); + if (rule2 instanceof Taclet) { + var ruleSets2 = ((Taclet) rule2).getRuleSets(); + var found = false; + for (var name : ruleSets2) { + if (GROUPS.get(matchingGroup).contains(name.toString())) { + found = true; + break; + } + } + if (!found) { + break; + } + group.add(n2); + n = n2; + } else { + break; + } + } + if (group.size() > 1) { + System.out.println("found group ending @ " + n.serialNr()); + group.get(0).setGroup(group); + for (int i = 1; i < group.size(); i++) { + group.get(i).setHideInProofTree(true); + } + } + } + } + for (int i = 0; i < n.childrenCount(); i++) { + q.add(n.child(i)); + } + } + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index 81e35f505d7..5781144c038 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -193,6 +193,17 @@ public JToolBar getToolbar(MainWindow mainWindow) { } }); bar.add(b); + JButton b2 = new JButton(); + b2.setText("Reorder"); + b2.addActionListener(e -> { + KeYMediator m = MainWindow.getInstance().getMediator(); + try { + ProofRegroup.regroupProof(m.getSelectedProof()); + } catch (Exception exc) { + exc.printStackTrace(); + } + }); + bar.add(b2); return bar; } } From 0f182dac5be6d55aa89a736991aa3d7bd9850660 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 12 Jun 2023 08:45:48 +0200 Subject: [PATCH 10/26] Only group rule apps on the same pos --- .../ilkd/key/rule/AbstractBuiltInRuleApp.java | 2 +- .../java/de/uka/ilkd/key/rule/PosRuleApp.java | 15 +++++++++++++++ .../de/uka/ilkd/key/rule/PosTacletApp.java | 14 +------------- .../key/gui/prooftree/GUIProofTreeNode.java | 1 - .../org/key_project/slicing/ProofRegroup.java | 18 +++++++++++++++--- .../key_project/slicing/SlicingExtension.java | 5 +++-- 6 files changed, 35 insertions(+), 20 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/PosRuleApp.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java index 586f99ba980..e5c399693e2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java @@ -13,7 +13,7 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; -public abstract class AbstractBuiltInRuleApp implements IBuiltInRuleApp { +public abstract class AbstractBuiltInRuleApp implements IBuiltInRuleApp, PosRuleApp { public static final AtomicLong PERF_EXECUTE = new AtomicLong(); public static final AtomicLong PERF_SET_SEQUENT = new AtomicLong(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/PosRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/PosRuleApp.java new file mode 100644 index 00000000000..493732009e6 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/PosRuleApp.java @@ -0,0 +1,15 @@ +package de.uka.ilkd.key.rule; + +import de.uka.ilkd.key.logic.PosInOccurrence; + +/** + * Interface for rule applications with associated position information. + * + * @author Arne Keller + */ +public interface PosRuleApp { + /** + * @return the position the rule was applied on + */ + PosInOccurrence posInOccurrence(); +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java index 7353e6a9e3c..32d258b19e3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java @@ -24,7 +24,7 @@ * ({@link de.uka.ilkd.key.rule.NoPosTacletApp}) is used to keep track of the (partial) * instantiation information. */ -public class PosTacletApp extends TacletApp { +public class PosTacletApp extends TacletApp implements PosRuleApp { /** * stores the information where the Taclet is to be applied. This means where the find section @@ -68,18 +68,6 @@ public static PosTacletApp createPosTacletApp(FindTaclet taclet, MatchConditions return createPosTacletApp(taclet, matchCond.getInstantiations(), null, pos, services); } - - /** - * creates a PosTacletApp for the given taclet and a position information - * - * @param taclet the FindTaclet - * @param pos the PosInOccurrence storing the position where to apply the Taclet - */ - private PosTacletApp(FindTaclet taclet, PosInOccurrence pos) { - super(taclet); - this.pos = pos; - } - /** * creates a PosTacletApp for the given taclet with some known instantiations and a position * information diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java index 878af3704d6..544c26a2733 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java @@ -90,7 +90,6 @@ private void ensureChildrenArray() { return; } } else if (node != null && node.getGroup() != null) { - System.out.println("setting up children array of grouped node"); List group = node.getGroup(); children = new GUIAbstractTreeNode[group.size()]; for (int i = 0; i < group.size(); i++) { diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java index 329010a021a..9e688f39ea1 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java @@ -7,10 +7,13 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.PosRuleApp; import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.RuleApp; import de.uka.ilkd.key.rule.Taclet; +import org.key_project.slicing.graph.DependencyGraph; + public final class ProofRegroup { private static final List> GROUPS = List.of(List.of("alpha", "delta"), List.of("negationNormalForm", "conjNormalForm"), @@ -18,7 +21,7 @@ public final class ProofRegroup { "polySimp_pullOutGcd", "polySimp_applyEq", "polySimp_applyEqRigid", "simplify_literals")); - public static void regroupProof(Proof proof) { + public static void regroupProof(Proof proof, DependencyGraph graph) { /* * alpha, delta * negationNormalForm, conjNormalForm @@ -57,8 +60,17 @@ public static void regroupProof(Proof proof) { break; } var n2 = n.child(0); - var rule2 = n2.getAppliedRuleApp().rule(); - if (rule2 instanceof Taclet) { + var r2 = n2.getAppliedRuleApp(); + var rule2 = r2.rule(); + if (r2 instanceof PosRuleApp && rule2 instanceof Taclet) { + var p2 = (PosRuleApp) r2; + var graphNode = graph.getGraphNode(proof, n2.getBranchLocation(), + p2.posInOccurrence()); + Node finalN = n; + if (graph.edgesProducing(graphNode) + .noneMatch(a -> a.getProofStep() == finalN)) { + break; + } var ruleSets2 = ((Taclet) rule2).getRuleSets(); var found = false; for (var name : ruleSets2) { diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index 5781144c038..b85ac648fa3 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -194,11 +194,12 @@ public JToolBar getToolbar(MainWindow mainWindow) { }); bar.add(b); JButton b2 = new JButton(); - b2.setText("Reorder"); + b2.setText("Regroup"); b2.addActionListener(e -> { KeYMediator m = MainWindow.getInstance().getMediator(); try { - ProofRegroup.regroupProof(m.getSelectedProof()); + ProofRegroup.regroupProof(m.getSelectedProof(), + trackers.get(m.getSelectedProof()).getDependencyGraph()); } catch (Exception exc) { exc.printStackTrace(); } From 0ac82bd79ffac0bb38240556a27dfd3eda0f68f9 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Tue, 13 Jun 2023 16:27:46 +0200 Subject: [PATCH 11/26] Track newly introduced functions correctly --- .../proof/replay/AbstractProofReplayer.java | 8 +++ .../slicing/DependencyNodeData.java | 2 +- .../slicing/DependencyTracker.java | 25 +++++++--- .../org/key_project/slicing/ProofReorder.java | 10 ++++ .../slicing/graph/DependencyGraph.java | 28 +++++++++++ .../slicing/graph/TrackedFunction.java | 49 +++++++++++++++++++ 6 files changed, 115 insertions(+), 7 deletions(-) create mode 100644 keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java index b8cdc9d0aef..7ae30e56033 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java @@ -1,5 +1,6 @@ package de.uka.ilkd.key.proof.replay; +import java.io.File; import java.util.ArrayList; import java.util.Collection; import java.util.List; @@ -92,6 +93,13 @@ protected ImmutableList reApplyRuleApp(Node node, Goal openGoal) System.out.println( "reapplying " + node.serialNr() + " " + node.getAppliedRuleApp().rule().displayName() + " on node " + openGoal.node().serialNr()); + + try { + openGoal.proof().saveToFile(new File("/tmp/p" + openGoal.node().serialNr() + ".proof")); + } catch (Exception e) { + // . + } + if (ruleApp.rule() instanceof BuiltInRule) { IBuiltInRuleApp builtInRuleApp = constructBuiltinApp(node, openGoal); if (!builtInRuleApp.complete()) { diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyNodeData.java b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyNodeData.java index a5a4d97c606..23b84d2fe1a 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyNodeData.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyNodeData.java @@ -38,7 +38,7 @@ public class DependencyNodeData { public DependencyNodeData(List> inputs, List outputs, String label) { this.inputs = Collections.unmodifiableList(inputs); - this.outputs = Collections.unmodifiableList(outputs); + this.outputs = outputs; this.label = label; } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java index 3938601f0de..601d8dbb92a 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java @@ -8,9 +8,11 @@ import java.util.Set; import java.util.stream.Stream; +import de.uka.ilkd.key.logic.OpCollector; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.Function; +import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.proof.BranchLocation; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; @@ -169,14 +171,25 @@ private List> inputsOfNode(Node n, Set z = ((Term) z).op(); } if (z instanceof Function) { + // skip if z is contained in any of the other inputs + Operator finalZ = (Function) z; + if (input.stream().anyMatch(form -> { + var graphNode = form.first; + if (graphNode instanceof TrackedFormula) { + TrackedFormula tf = (TrackedFormula) graphNode; + OpCollector op = new OpCollector(); + tf.formula.formula().execPreOrder(op); + return op.contains(finalZ); + } + return false; + })) { + continue; + } + var a = ((Function) z).getIntroducedBy(); if (a != null && a != n) { - graph.outputsOf(a).forEach(i -> { - input.add(new Pair<>(i, false)); - // TODO: not strictly necessary if the Function is used in one of the - // previous inputs - // e.g. applyEq - }); + input.add(new Pair<>( + graph.getFunctionNode((Function) z, a.getBranchLocation()), false)); } } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index d538b04bc98..9ad3e837983 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -19,6 +19,7 @@ import de.uka.ilkd.key.proof.io.*; import de.uka.ilkd.key.util.Pair; +import org.key_project.slicing.graph.AnnotatedEdge; import org.key_project.slicing.graph.DependencyGraph; import org.key_project.slicing.graph.GraphNode; @@ -76,6 +77,15 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) q.addLast(nextNode); return; } + // check that all consumed inputs were already used by all other steps + if (!depGraph.inputsConsumedBy(node) + .allMatch( + input -> depGraph.edgesUsing(input).map(AnnotatedEdge::getProofStep) + .allMatch(x -> node == x || newOrderSorted.contains(x) + || !x.getBranchLocation().equals(loc)))) { + q.addLast(nextNode); + return; + } finalNewOrder.add(node); newOrderSorted.add(node); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java index 0aa8278bb8a..2c7106690f3 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java @@ -4,6 +4,7 @@ import java.util.stream.Stream; import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.logic.op.Function; import de.uka.ilkd.key.proof.BranchLocation; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; @@ -334,6 +335,33 @@ public GraphNode getGraphNode(Proof proof, BranchLocation locationGuess, PosInOc return null; } + public TrackedFunction getFunctionNode(Function function, BranchLocation loc) { + TrackedFunction candidate = new TrackedFunction(function, loc); + if (graph.containsVertex(candidate)) { + return candidate; + } + graph.addVertex(candidate); + var edges = edgeDataReversed.get(function.getIntroducedBy()); + var sourcesDone = new HashSet<>(); + Collection newEdges = new ArrayList<>(); + for (var x : edges) { + GraphNode g = x.getSource(); + if (sourcesDone.contains(g)) { + continue; + } + sourcesDone.add(g); + AnnotatedEdge e = new AnnotatedEdge(function.getIntroducedBy(), false); + graph.addEdge(g, candidate, e); + newEdges.add(e); + } + edgeDataReversed.get(function.getIntroducedBy()).addAll(newEdges); + DependencyNodeData n = function.getIntroducedBy().lookup(DependencyNodeData.class); + if (n != null) { + n.outputs.add(candidate); + } + return candidate; + } + /** * Get a copy of the internal graph. * diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java new file mode 100644 index 00000000000..e51b50d920b --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java @@ -0,0 +1,49 @@ +package org.key_project.slicing.graph; + +import java.util.Objects; + +import de.uka.ilkd.key.logic.op.Function; +import de.uka.ilkd.key.proof.BranchLocation; + +public class TrackedFunction extends GraphNode { + private Function function; + + public TrackedFunction(Function f, BranchLocation loc) { + super(loc); + + this.function = f; + } + + @Override + public GraphNode popLastBranchID() { + return new TrackedFunction(function, getBranchLocation().removeLast()); + } + + @Override + public String toString(boolean abbreviated, boolean omitBranch) { + return "variable " + function.toString(); + } + + public Function getFunction() { + return function; + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + + TrackedFunction that = (TrackedFunction) o; + + return Objects.equals(function, that.function); + } + + @Override + public int hashCode() { + return function != null ? function.hashCode() : 0; + } +} From f2002ee73f264ea60b8fbc05d5fbcc8a9f7d3ee8 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Tue, 13 Jun 2023 17:05:01 +0200 Subject: [PATCH 12/26] Fix UI issues around regrouping --- .../ilkd/key/gui/MainWindowTabbedPane.java | 67 ------------------- .../key/gui/prooftree/GUIProofTreeNode.java | 18 +++-- .../org/key_project/slicing/ProofRegroup.java | 4 +- 3 files changed, 16 insertions(+), 73 deletions(-) delete mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java deleted file mode 100644 index 3d0731046b5..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java +++ /dev/null @@ -1,67 +0,0 @@ -package de.uka.ilkd.key.gui; - -import java.awt.*; -import java.awt.event.KeyEvent; -import java.util.stream.Stream; -import javax.swing.*; - -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.gui.actions.AutoModeAction; -import de.uka.ilkd.key.gui.extension.api.TabPanel; -import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade; -import de.uka.ilkd.key.gui.prooftree.ProofTreeView; - -/** - * {@link JTabbedPane} displayed in {@link MainWindow}, to the left of - * {@link de.uka.ilkd.key.gui.nodeviews.SequentView}. - * - * @author Kai Wallisch - */ -@Deprecated -public class MainWindowTabbedPane extends JTabbedPane { - private static final long serialVersionUID = 1L; - public static final float TAB_ICON_SIZE = 16f; - private final ProofTreeView proofTreeView; - - MainWindowTabbedPane(MainWindow mainWindow, KeYMediator mediator, - AutoModeAction autoModeAction) { - assert mediator != null; - assert mainWindow != null; - - proofTreeView = new ProofTreeView(mediator); - InfoView infoView = new InfoView(mainWindow, mediator); - StrategySelectionView strategySelectionView = - new StrategySelectionView(mainWindow, mediator); - GoalList openGoalsView = new GoalList(mediator); - - Stream panels = KeYGuiExtensionFacade.getAllPanels(mainWindow); - addPanel(infoView); - addPanel(strategySelectionView); - addPanel(openGoalsView); - addPanel(proofTreeView); - panels.forEach(this::addPanel); - - - // change some key mappings which collide with font settings. - getInputMap(JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT).getParent() - .remove(KeyStroke.getKeyStroke(KeyEvent.VK_UP, - Toolkit.getDefaultToolkit().getMenuShortcutKeyMask())); - getInputMap(JComponent.WHEN_FOCUSED).getParent().remove(KeyStroke.getKeyStroke( - KeyEvent.VK_DOWN, Toolkit.getDefaultToolkit().getMenuShortcutKeyMask())); - setName("leftTabbed"); - } - - protected void addPanel(TabPanel p) { - addTab(p.getTitle(), p.getIcon(), p.getComponent()); - } - - protected void setEnabledForAllTabs(boolean b) { - for (int i = 0; i < getTabCount(); i++) { - getComponentAt(i).setEnabled(b); - } - } - - public ProofTreeView getProofTreeView() { - return proofTreeView; - } -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java index 544c26a2733..5f28d17325a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java @@ -16,7 +16,15 @@ class GUIProofTreeNode extends GUIAbstractTreeNode { private GUIAbstractTreeNode[] children; private boolean leaf; - public GUIProofTreeNode(GUIProofTreeModel tree, Node node, boolean leaf) { + /** + * This constructor should only be called by the {@link GUIProofTreeModel}! + * Use {@link GUIProofTreeModel#getProofTreeNode(Node)} to get the nodes. + * + * @param tree the proof tree + * @param node the node + * @param leaf whether the node is a leaf + */ + GUIProofTreeNode(GUIProofTreeModel tree, Node node, boolean leaf) { super(tree, node); this.leaf = leaf; } @@ -41,7 +49,7 @@ public TreeNode getParent() { while (n.parent() != null && n.getGroup() == null) { n = n.parent(); } - return findBranch(n); + return getProofTreeModel().getProofTreeNode(n); } while (n.parent() != null && findChild(n.parent()) != null) { n = n.parent(); @@ -91,9 +99,9 @@ private void ensureChildrenArray() { } } else if (node != null && node.getGroup() != null) { List group = node.getGroup(); - children = new GUIAbstractTreeNode[group.size()]; - for (int i = 0; i < group.size(); i++) { - children[i] = new GUIProofTreeNode(getProofTreeModel(), group.get(i), true); + children = new GUIAbstractTreeNode[group.size() - 1]; + for (int i = 1; i < group.size(); i++) { + children[i - 1] = getProofTreeModel().getProofTreeNode(group.get(i)); } return; } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java index 9e688f39ea1..e8abafb9f19 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java @@ -5,6 +5,7 @@ import java.util.Deque; import java.util.List; +import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.rule.PosRuleApp; @@ -89,7 +90,6 @@ public static void regroupProof(Proof proof, DependencyGraph graph) { } } if (group.size() > 1) { - System.out.println("found group ending @ " + n.serialNr()); group.get(0).setGroup(group); for (int i = 1; i < group.size(); i++) { group.get(i).setHideInProofTree(true); @@ -101,5 +101,7 @@ public static void regroupProof(Proof proof, DependencyGraph graph) { q.add(n.child(i)); } } + // make sure the changed structure is visible + MainWindow.getInstance().getProofTreeView().getDelegateModel().updateTree(null); } } From 6522b2fcca9ce9755cf4690749a25e632c54cbdd Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 15 Jun 2023 14:58:57 +0200 Subject: [PATCH 13/26] Javadocs --- .../main/java/org/key_project/slicing/ProofRegroup.java | 9 +++++++++ .../org/key_project/slicing/graph/DependencyGraph.java | 9 +++++++++ .../org/key_project/slicing/graph/TrackedFunction.java | 7 ++++++- 3 files changed, 24 insertions(+), 1 deletion(-) diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java index e8abafb9f19..6eec3d3337c 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java @@ -15,7 +15,16 @@ import org.key_project.slicing.graph.DependencyGraph; +/** + * Proof step regrouping functionality. + * + * @author Arne Keller + */ public final class ProofRegroup { + private ProofRegroup() { + + } + private static final List> GROUPS = List.of(List.of("alpha", "delta"), List.of("negationNormalForm", "conjNormalForm"), List.of("polySimp_expand", "polySimp_normalise", "polySimp_newSym", diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java index 2c7106690f3..34844bc2065 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java @@ -335,6 +335,15 @@ public GraphNode getGraphNode(Proof proof, BranchLocation locationGuess, PosInOc return null; } + /** + * Get the graph node for a given function and branch location. + * If the function is not registered in the graph yet, a new graph node is created. + * The function has to be a skolem constant! + * + * @param function function + * @param loc branch location + * @return graph node representing the function + */ public TrackedFunction getFunctionNode(Function function, BranchLocation loc) { TrackedFunction candidate = new TrackedFunction(function, loc); if (graph.containsVertex(candidate)) { diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java index e51b50d920b..219b70ea336 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java @@ -5,8 +5,13 @@ import de.uka.ilkd.key.logic.op.Function; import de.uka.ilkd.key.proof.BranchLocation; +/** + * A skolem constant tracked in the dependency graph. + * + * @author Arne Keller + */ public class TrackedFunction extends GraphNode { - private Function function; + private final Function function; public TrackedFunction(Function f, BranchLocation loc) { super(loc); From 583724500386ddc679dfebbb8e70c7413e6d6ec3 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 16 Jun 2023 15:12:25 +0200 Subject: [PATCH 14/26] Add settings UI and tree node labels --- .../main/java/de/uka/ilkd/key/proof/Node.java | 19 ++--- .../rules/integerSimplificationRules.key | 2 +- .../de/uka/ilkd/key/nparser/taclets.old.txt | 2 +- .../key/gui/prooftree/GUIProofTreeNode.java | 3 + .../org/key_project/slicing/ProofRegroup.java | 14 ++-- .../slicing/ProofRegroupSettings.java | 67 +++++++++++++++ .../slicing/ProofRegroupSettingsProvider.java | 83 +++++++++++++++++++ .../key_project/slicing/RegroupExtension.java | 37 +++++++++ ...ilkd.key.gui.extension.api.KeYGuiExtension | 3 +- 9 files changed, 208 insertions(+), 22 deletions(-) create mode 100644 keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java create mode 100644 keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java create mode 100644 keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java index c5d491660c2..ecedf8dd0df 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java @@ -111,6 +111,7 @@ public class Node implements Iterable, Comparable { private List group = null; private boolean hideInProofTree = false; + private String extraNodeLabel = null; /** @@ -400,16 +401,6 @@ void remove() { } } - public void removeChildren() { - children.clear(); - } - - public void replaceChild(int i, Node newChild) { - children.set(i, newChild); - newChild.parent = this; - newChild.siblingNr = i; - } - /** * Removes child/parent relationship between the given node and this node; if the given node is * not child of this node, nothing happens and then and only then false is returned. @@ -857,6 +848,14 @@ public void setGroup(List group) { this.group = group; } + public String getExtraNodeLabel() { + return extraNodeLabel; + } + + public void setExtraNodeLabel(String extraNodeLabel) { + this.extraNodeLabel = extraNodeLabel; + } + public boolean isHideInProofTree() { return hideInProofTree; } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key index 27df6130f18..8a679f33ff3 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key @@ -1802,7 +1802,7 @@ \then(aePseudoRight * aePseudoTargetFactor = aePseudoTargetRight * aePseudoLeftCoeff) \else(aePseudoTargetLeft = aePseudoTargetRight)) - \heuristics(polySimp_leftNonUnit, polySimp_applyEqPseudo, notHumanReadable, notHumanReadable) + \heuristics(polySimp_leftNonUnit, polySimp_applyEqPseudo, notHumanReadable) }; apply_eq_pseudo_leq { diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt index 084552d436d..e5a642f2e75 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt @@ -1032,7 +1032,7 @@ apply_eq_pseudo_eq { \assumes ([equals(mul(aePseudoLeft,aePseudoLeftCoeff),aePseudoRight)]==>[]) \find(equals(aePseudoTargetLeft,aePseudoTargetRight)) \sameUpdateLevel\replacewith(if-then-else(and(equals(aePseudoTargetLeft,mul(aePseudoLeft,aePseudoTargetFactor)),not(equals(aePseudoLeftCoeff,Z(0(#))))),equals(mul(aePseudoRight,aePseudoTargetFactor),mul(aePseudoTargetRight,aePseudoLeftCoeff)),equals(aePseudoTargetLeft,aePseudoTargetRight))) -\heuristics(notHumanReadable, notHumanReadable, polySimp_applyEqPseudo, polySimp_leftNonUnit) +\heuristics(notHumanReadable, polySimp_applyEqPseudo, polySimp_leftNonUnit) Choices: true} ----------------------------------------------------- == apply_eq_pseudo_geq (apply_eq_pseudo_geq) ========================================= diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java index 5f28d17325a..ede2e08f162 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java @@ -66,6 +66,9 @@ public String toString() { // the proof tree in ProofTreeView.java Node n = getNode(); if (n != null) { + if (n.getExtraNodeLabel() != null) { + return n.serialNr() + ":" + n.getExtraNodeLabel(); + } return n.serialNr() + ":" + n.name(); } else { return "Invalid WeakReference"; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java index 6eec3d3337c..12dea9865b1 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java @@ -25,12 +25,6 @@ private ProofRegroup() { } - private static final List> GROUPS = - List.of(List.of("alpha", "delta"), List.of("negationNormalForm", "conjNormalForm"), - List.of("polySimp_expand", "polySimp_normalise", "polySimp_newSym", - "polySimp_pullOutGcd", "polySimp_applyEq", "polySimp_applyEqRigid", - "simplify_literals")); - public static void regroupProof(Proof proof, DependencyGraph graph) { /* * alpha, delta @@ -39,6 +33,7 @@ public static void regroupProof(Proof proof, DependencyGraph graph) { * * simplify_enlarging, simplify, simplify_select */ + var GROUPS = ProofRegroupSettingsProvider.getSettings().getGroups(); Deque q = new ArrayDeque<>(); q.add(proof.root()); while (!q.isEmpty()) { @@ -53,16 +48,16 @@ public static void regroupProof(Proof proof, DependencyGraph graph) { Rule rule = r.rule(); if (rule instanceof Taclet) { var ruleSets = ((Taclet) rule).getRuleSets(); - int matchingGroup = -1; + String matchingGroup = null; for (var name : ruleSets) { - for (int i = 0; i < GROUPS.size(); i++) { + for (String i : GROUPS.keySet()) { if (GROUPS.get(i).contains(name.toString())) { matchingGroup = i; break; } } } - if (matchingGroup != -1) { + if (matchingGroup != null) { List group = new ArrayList<>(); group.add(n); while (true) { @@ -100,6 +95,7 @@ public static void regroupProof(Proof proof, DependencyGraph graph) { } if (group.size() > 1) { group.get(0).setGroup(group); + group.get(0).setExtraNodeLabel(matchingGroup); for (int i = 1; i < group.size(); i++) { group.get(i).setHideInProofTree(true); } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java new file mode 100644 index 00000000000..525b6ed8ae7 --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java @@ -0,0 +1,67 @@ +package org.key_project.slicing; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Properties; + +import de.uka.ilkd.key.settings.AbstractPropertiesSettings; + +public class ProofRegroupSettings extends AbstractPropertiesSettings { + private static final String PREFIX = "[ProofRegrouping]Group"; + + private final List> groups = new ArrayList<>(); + + @Override + public void readSettings(Properties props) { + for (var key : props.keySet()) { + var k = (String) key; + var v = props.get(k); + if (k.startsWith(PREFIX)) { + var groupName = k.substring(PREFIX.length()); + var prop = createStringProperty(PREFIX + groupName, ""); + prop.set((String) v); + groups.add(prop); + } + } + if (groups.isEmpty()) { + addGroup("Propositional expansion", List.of("alpha", "delta")); + addGroup("Normal form", + List.of("negationNormalForm", "conjNormalForm")); + addGroup("Polynomials and inequations", + List.of("polySimp_expand", "polySimp_normalise", "polySimp_newSym", + "polySimp_pullOutGcd", "polySimp_applyEq", "polySimp_applyEqRigid", + "polySimp_directEquations", "polySimp_applyEqPseudo", + "inEqSimp_forNormalisation", "inEqSimp_directInEquations", + "inEqSimp_propagation", + "inEqSimp_nonLin", "inEqSimp_signCases", + "inEqSimp_expand", "inEqSimp_saturate", + "inEqSimp_pullOutGcd", "inEqSimp_special_nonLin", + "simplify_literals")); + addGroup("Simplification", + List.of("simplify", "simplify_select", "simplify_enlarging")); + } + } + + public void addGroup(String name, List ruleSets) { + groups.add(createStringProperty(PREFIX + name, String.join(",", ruleSets))); + } + + public void updateGroup(String name, List ruleSets) { + for (var prop : groups) { + if (prop.getKey().equals(PREFIX + name)) { + prop.set(String.join(",", ruleSets)); + } + } + } + + public Map> getGroups() { + Map> m = new HashMap<>(); + for (var pe : groups) { + var name = pe.getKey().substring(PREFIX.length()); + m.put(name, List.of(pe.get().split(","))); + } + return m; + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java new file mode 100644 index 00000000000..b6eae28b991 --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java @@ -0,0 +1,83 @@ +package org.key_project.slicing; + + +import java.util.ArrayList; +import java.util.List; +import javax.swing.*; + +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.settings.SettingsPanel; +import de.uka.ilkd.key.gui.settings.SettingsProvider; +import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.util.Pair; + +import net.miginfocom.layout.CC; + +/** + * Settings for the proof slicing extension. + * + * @author Arne Keller + */ +public class ProofRegroupSettingsProvider extends SettingsPanel implements SettingsProvider { + /** + * Singleton instance of the settings. + */ + private static final ProofRegroupSettings SETTINGS = new ProofRegroupSettings(); + + /** + * Text for introductory explanation + */ + private static final String INTRO_LABEL = "Adjust heuristics groups here."; + + private final List> groups = new ArrayList<>(); + + /** + * Construct a new settings provider. + */ + public ProofRegroupSettingsProvider() { + setHeaderText("Proof Regrouping Options"); + } + + @Override + public String getDescription() { + return "Proof Regrouping"; + } + + /** + * @return the settings managed by this provider + */ + public static ProofRegroupSettings getSettings() { + ProofIndependentSettings.DEFAULT_INSTANCE.addSettings(SETTINGS); + return SETTINGS; + } + + @Override + public JComponent getPanel(MainWindow window) { + ProofRegroupSettings ss = getSettings(); + + pCenter.removeAll(); + pCenter.add(new JLabel(INTRO_LABEL), new CC().span().alignX("left")); + + for (var e : ss.getGroups().entrySet()) { + var ta = + addTextArea(e.getKey(), String.join("\n", e.getValue()), null, emptyValidator()); + groups.add(new Pair<>(e.getKey(), ta)); + } + + return this; + } + + @Override + public void applySettings(MainWindow window) { + ProofRegroupSettings ss = getSettings(); + for (Pair ta : groups) { + ss.updateGroup(ta.first, List.of(ta.second.getText().split("\n"))); + } + } + + + @Override + public int getPriorityOfSettings() { + return 10000; + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java new file mode 100644 index 00000000000..275dfeb3779 --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java @@ -0,0 +1,37 @@ +package org.key_project.slicing; + +import javax.annotation.Nonnull; +import javax.swing.*; + +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.gui.settings.SettingsProvider; + +/** + * Proof slicing extension. + * For more details see the user + * guide. + * + * @author Arne Keller + */ +@KeYGuiExtension.Info(name = "Slicing", + description = "Author: Arne Keller ", + experimental = false, + optional = true, + priority = 9001) +public class RegroupExtension implements KeYGuiExtension, + KeYGuiExtension.Settings, + KeYGuiExtension.Toolbar { + + + @Nonnull + @Override + public JToolBar getToolbar(MainWindow mainWindow) { + return new JToolBar(); + } + + @Override + public SettingsProvider getSettings() { + return new ProofRegroupSettingsProvider(); + } +} diff --git a/keyext.slicing/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/keyext.slicing/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension index 154d90dcbdf..eab98ab1cc6 100644 --- a/keyext.slicing/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension +++ b/keyext.slicing/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension @@ -1 +1,2 @@ -org.key_project.slicing.SlicingExtension \ No newline at end of file +org.key_project.slicing.SlicingExtension +org.key_project.slicing.RegroupExtension \ No newline at end of file From 01c0d5c9f77c47e707d2f02b875f26f2ee5666d0 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 21 Jun 2023 19:30:17 +0200 Subject: [PATCH 15/26] Fix several bugs in reordering --- .../de/uka/ilkd/key/proof/BranchLocation.java | 10 +++++- .../util/collection/ImmutableList.java | 4 +-- .../org/key_project/slicing/ProofReorder.java | 31 +++++++++++++++++-- 3 files changed, 39 insertions(+), 6 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/BranchLocation.java b/key.core/src/main/java/de/uka/ilkd/key/proof/BranchLocation.java index 4ec960c9ab0..a1286420dac 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/BranchLocation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/BranchLocation.java @@ -80,6 +80,9 @@ public static BranchLocation commonPrefix(BranchLocation... locations) { * @return the remaining suffix */ public BranchLocation stripPrefix(BranchLocation prefix) { + if (prefix.size() == location.size()) { + return BranchLocation.ROOT; + } return new BranchLocation(location.stripPrefix(prefix.location)); } @@ -101,6 +104,9 @@ public BranchLocation append(Pair newBranch) { public BranchLocation removeLast() { List> list = location.toList(); list.remove(list.size() - 1); + if (list.isEmpty()) { + return BranchLocation.ROOT; + } return new BranchLocation(ImmutableList.fromList(list)); } @@ -171,7 +177,9 @@ public int hashCode() { @Override public int compareTo(BranchLocation other) { - if (this == BranchLocation.ROOT) { + if (this == other) { + return 0; + } else if (this == BranchLocation.ROOT) { return -1; } else if (other == BranchLocation.ROOT) { return 1; diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java index 731fb8486ca..59cf4136375 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java @@ -374,8 +374,8 @@ default int compareTo(ImmutableList other) { } else if (l2.isEmpty()) { return 1; } - var a = (Comparable) this.head(); - var b = (T) other.head(); + var a = (Comparable) l1.head(); + var b = (T) l2.head(); var value = a.compareTo(b); if (value != 0) { return value; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index 9ad3e837983..7adbafeee53 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -41,12 +41,13 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) todo.add(new Pair<>(BranchLocation.ROOT, proof.root())); while (!todo.isEmpty()) { var t = todo.pop(); - var root = t.second; var loc = t.first; + var root = t.second; if (done.contains(loc)) { continue; } done.add(loc); + System.out.println("doing branch " + loc); Deque q = new ArrayDeque<>(); for (int i = 1; i <= root.sequent().size(); i++) { @@ -60,8 +61,14 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) var nextNode = q.pop(); List finalNewOrder = newOrder; depGraph.outgoingEdgesOf(nextNode).forEach(node -> { - if (!node.getBranchLocation().equals(loc)) { - todo.add(new Pair<>(node.getBranchLocation(), node.getFirstInBranch())); + var newLoc = node.getBranchLocation(); + if (!newLoc.equals(loc)) { + /* + * if (!todo.containsKey(newLoc) && !done.contains(newLoc)) { + * System.out.println("adding branch " + newLoc); + * todo.put(newLoc, node.getFirstInBranch()); + * } + */ return; } @@ -94,10 +101,28 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) outputs.forEach(q::addFirst); }); } + List nextQ = new ArrayList<>(); + newOrder.forEach(node -> node.childrenIterator().forEachRemaining(node2 -> { + if (newOrderSorted.contains(node2) || node2.getAppliedRuleApp() == null + || node2.getBranchLocation() != node.getBranchLocation()) { + return; + } + nextQ.add(node2); + })); + Collections.sort(nextQ); + // this works because there are no taclets in KeY that have no inputs and add a formula + // to the sequent + newOrder.addAll(nextQ); for (int i = 0; i < newOrder.size(); i++) { if (newOrder.get(i).childrenCount() != 1 || newOrder.get(i).child(0).childrenCount() == 0) { var last = newOrder.remove(i); + var c = last.childrenCount(); + c--; + while (c >= 0) { + todo.addFirst(new Pair<>(last.child(c).getBranchLocation(), last.child(c))); + c--; + } newOrder.add(last); break; } From 9e3ef4b91a6ccabb556a3968a1e79bd9da2f646c Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 22 Jun 2023 18:29:50 +0200 Subject: [PATCH 16/26] Better error handling --- .../main/java/de/uka/ilkd/key/gui/TaskTree.java | 5 +---- .../org/key_project/slicing/ProofReorder.java | 15 +++++++++------ .../key_project/slicing/ReorderingReplayer.java | 5 +++++ .../org/key_project/slicing/SlicingExtension.java | 10 +++++++++- 4 files changed, 24 insertions(+), 11 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java index 2c6506ef1dd..b3d04a048e8 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java @@ -1,8 +1,6 @@ package de.uka.ilkd.key.gui; -import java.awt.BorderLayout; -import java.awt.Component; -import java.awt.Font; +import java.awt.*; import java.awt.event.MouseAdapter; import java.awt.event.MouseEvent; import java.awt.event.MouseListener; @@ -328,7 +326,6 @@ public Component getTreeCellRendererComponent(JTree list, Object value, boolean sup.setIcon(keyIcon); } } - } return sup; } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index 7adbafeee53..ae4db025b20 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -101,18 +101,21 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) outputs.forEach(q::addFirst); }); } + // Finally, get all nodes that do not directly connect to the dependency graph of the + // previous branch. These are taclets that do not have any formulas as direct inputs, + // e.g. sign_case_distinction List nextQ = new ArrayList<>(); newOrder.forEach(node -> node.childrenIterator().forEachRemaining(node2 -> { - if (newOrderSorted.contains(node2) || node2.getAppliedRuleApp() == null - || node2.getBranchLocation() != node.getBranchLocation()) { - return; + while (node2 != null && !newOrderSorted.contains(node2) + && node2.getAppliedRuleApp() != null + && node2.getBranchLocation() == node.getBranchLocation()) { + nextQ.add(node2); + node2 = node2.childrenCount() > 0 ? node2.child(0) : null; } - nextQ.add(node2); })); Collections.sort(nextQ); - // this works because there are no taclets in KeY that have no inputs and add a formula - // to the sequent newOrder.addAll(nextQ); + // add the next branches to the queue for (int i = 0; i < newOrder.size(); i++) { if (newOrder.get(i).childrenCount() != 1 || newOrder.get(i).child(0).childrenCount() == 0) { diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java b/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java index c9f05c9f215..3c56295a3b7 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java @@ -12,6 +12,11 @@ import org.key_project.util.collection.ImmutableList; +/** + * Replayer that will reorder a proof based on the provided sorting of the steps. + * + * @author Arne Keller + */ public class ReorderingReplayer extends AbstractProofReplayer { private final SortedMap> steps; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index b85ac648fa3..461e5296ba0 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -12,6 +12,7 @@ import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.core.KeYSelectionEvent; import de.uka.ilkd.key.core.KeYSelectionListener; +import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.extension.api.ContextMenuAdapter; import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; @@ -30,6 +31,9 @@ import org.key_project.slicing.ui.ShowGraphAction; import org.key_project.slicing.ui.SlicingLeftPanel; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * Proof slicing extension. * For more details see the user @@ -50,6 +54,8 @@ public class SlicingExtension implements KeYGuiExtension, KeYGuiExtension.Toolbar, KeYSelectionListener, ProofDisposedListener { + private static final Logger LOGGER = LoggerFactory.getLogger(SlicingExtension.class); + /** * Collection of dependency trackers attached to proofs. */ @@ -189,7 +195,9 @@ public JToolBar getToolbar(MainWindow mainWindow) { ProofReorder.reorderProof(m.getSelectedProof(), trackers.get(m.getSelectedProof()).getDependencyGraph()); } catch (Exception exc) { - exc.printStackTrace(); + LOGGER.error("failed to reorder proof ", exc); + MainWindow.getInstance().getMediator().startInterface(true); + IssueDialog.showExceptionDialog(MainWindow.getInstance(), exc); } }); bar.add(b); From 18076b0e54f23027103c9020c443cd97d382dde7 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sun, 2 Jul 2023 14:41:19 +0200 Subject: [PATCH 17/26] Buttons to add and remove heuristic groups --- .../settings/ProofIndependentSettings.java | 3 + .../ilkd/key/gui/settings/SettingsDialog.java | 2 +- .../ilkd/key/gui/settings/SettingsPanel.java | 28 ++++- .../key/gui/settings/SettingsProvider.java | 16 +++ .../uka/ilkd/key/gui/settings/SettingsUi.java | 4 +- .../ilkd/key/gui/utilities/FormDialog.java | 113 ++++++++++++++++++ .../slicing/ProofRegroupSettings.java | 35 +++++- .../slicing/ProofRegroupSettingsProvider.java | 81 +++++++++++++ 8 files changed, 272 insertions(+), 10 deletions(-) create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java index 29ce985ce9a..ffefb8978c5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java @@ -60,6 +60,9 @@ public void addSettings(Settings settings) { settings.addPropertyChangeListener(settingsListener); if (lastReadedProperties != null) { settings.readSettings(lastReadedProperties); + } else { + // special case: no settings file present + settings.readSettings(new Properties()); } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java index 782e239c548..80a875aca11 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java @@ -32,7 +32,7 @@ public SettingsDialog(MainWindow owner) { setTitle("Settings"); mainWindow = owner; - ui = new SettingsUi(owner); + ui = new SettingsUi(owner, this); JPanel root = new JPanel(new BorderLayout()); root.add(ui); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java index c9ccaaabd7c..e6d1c7b8c57 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java @@ -3,8 +3,11 @@ import java.awt.*; import java.io.File; +import java.util.ArrayList; import java.util.Arrays; +import java.util.HashMap; import java.util.List; +import java.util.Map; import javax.annotation.Nullable; import javax.swing.*; @@ -31,6 +34,8 @@ public abstract class SettingsPanel extends SimpleSettingsPanel { private static final long serialVersionUID = 3465371513326517504L; + private final Map> rows = new HashMap<>(); + protected SettingsPanel() { pCenter.setLayout(new MigLayout(new LC().fillX().wrapAfter(3), new AC().count(3).fill(1) .grow(1000f, 1).size("16px", 2).grow(0f, 0).align("right", 0))); @@ -42,7 +47,6 @@ protected SettingsPanel() { */ protected static JTextArea createInfoArea(String info) { JTextArea textArea = new JTextArea(info); - // textArea.setBackground(this.getBackground()); textArea.setEditable(false); textArea.setLineWrap(true); textArea.setWrapStyleWord(true); @@ -53,7 +57,9 @@ protected static JTextArea createInfoArea(String info) { * @param info * @param components */ - protected void addRowWithHelp(String info, JComponent... components) { + protected List addRowWithHelp(String info, JComponent... components) { + List comps = new ArrayList<>(List.of(components)); + boolean hasInfo = info != null && !info.isEmpty(); for (JComponent component : components) { component.setAlignmentX(LEFT_ALIGNMENT); @@ -68,6 +74,8 @@ protected void addRowWithHelp(String info, JComponent... components) { infoButton = new JLabel(); } pCenter.add(infoButton); + comps.add(infoButton); + return comps; } /** @@ -204,7 +212,21 @@ protected JComboBox addComboBox(String title, String info, int selectionI protected void addTitledComponent(String title, JComponent component, String helpText) { JLabel label = new JLabel(title); label.setLabelFor(component); - addRowWithHelp(helpText, label, component); + var comps = addRowWithHelp(helpText, label, component); + comps.add(label); + rows.put(title, comps); + } + + /** + * Remove a row previously added with {@link #addTitledComponent(String, JComponent, String)}. + * + * @param title title of component + */ + protected void removeTitledComponent(String title) { + for (var c : rows.get(title)) { + pCenter.remove(c); + } + rows.remove(title); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsProvider.java index d51acd292cb..28d6217a342 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsProvider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsProvider.java @@ -39,6 +39,22 @@ public interface SettingsProvider { */ JComponent getPanel(MainWindow window); + /** + * Provides the visual component for the right side. + *

+ * This panel will be wrapped inside a {@link JScrollPane}. + *

+ * You are allowed to reuse the return component. But then you should update the components, + * e.g. text field, during handling of the call. + * + * @param window non-null reference + * @param settingsDialog the settings dialog + * @return + */ + default JComponent getPanel(MainWindow window, JDialog settingsDialog) { + return getPanel(window); + } + /** * Tree children of your settings dialog. *

diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java index d811099fb78..146581af3b2 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java @@ -33,7 +33,7 @@ public class SettingsUi extends JPanel { private final MainWindow mainWindow; // private JScrollPane center; - public SettingsUi(MainWindow mainWindow) { + public SettingsUi(MainWindow mainWindow, SettingsDialog dialog) { this.mainWindow = mainWindow; treeSettingsPanels.setBorder(BorderFactory.createEmptyBorder(5, 5, 5, 5)); treeSettingsPanels.setCellRenderer(new DefaultTreeCellRenderer() { @@ -84,7 +84,7 @@ public void keyReleased(KeyEvent e) { treeSettingsPanels.addTreeSelectionListener(e -> { SettingsTreeNode n = (SettingsTreeNode) e.getPath().getLastPathComponent(); if (n.provider != null && n.provider.getPanel(mainWindow) != null) { - JComponent comp = n.provider.getPanel(mainWindow); + JComponent comp = n.provider.getPanel(mainWindow, dialog); // center.setViewportView(comp); // center.getVerticalScrollBar().setValue(0); // center.setHorizontalScrollBarPolicy(JScrollPane.HORIZONTAL_SCROLLBAR_NEVER); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java new file mode 100644 index 00000000000..40761d6ab24 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java @@ -0,0 +1,113 @@ +package de.uka.ilkd.key.gui.utilities; + +import java.awt.*; +import java.util.ArrayList; +import java.util.List; +import java.util.function.Consumer; +import java.util.function.Function; +import javax.swing.*; + +import de.uka.ilkd.key.util.Pair; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Simple and generic input form dialog. Support {@link JTextField} and {@link JTextArea} as fields. + * + * @author Arne Keller + */ +public class FormDialog extends JDialog { + private static final Logger LOGGER = LoggerFactory.getLogger(FormDialog.class); + + /** + * Construct and show a new form. + * + * @param owner parent dialog + * @param title title of the form + * @param comps components of the dialog: (name, input element) + * @param validate validation function (return a non-null string if there is an error) + * @param onSubmit callback for submit action + * @param onCancel callback for cancel action + */ + public FormDialog(JDialog owner, String title, List> comps, + Function>, String> validate, + Consumer>> onSubmit, Runnable onCancel) { + super(owner); + + setTitle(title); + setModal(true); + setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE); + + JPanel mainPane = new JPanel(); + mainPane.setLayout(new GridBagLayout()); + + var c = new GridBagConstraints(); + c.insets.bottom = 10; + c.insets.top = 10; + c.insets.left = 10; + c.insets.right = 10; + c.gridy = 1; + c.anchor = GridBagConstraints.WEST; + + for (var comp : comps) { + c.gridx = 1; + mainPane.add(new JLabel(comp.first), c.clone()); + c.gridx = 2; + c.fill = GridBagConstraints.HORIZONTAL; + mainPane.add(comp.second, c.clone()); + + c.gridy++; + } + + var submit = new JButton("Submit"); + submit.addActionListener(e -> { + try { + List> data = new ArrayList<>(); + for (var comp : comps) { + data.add(new Pair<>(comp.first, extractValue(comp.second))); + } + var error = validate.apply(data); + if (error != null) { + JOptionPane.showMessageDialog(this, error, "Validation error", + JOptionPane.ERROR_MESSAGE); + return; + } + onSubmit.accept(data); + dispose(); + } catch (Exception err) { + LOGGER.error("submit action failed ", err); + } + }); + + var cancel = new JButton("Cancel"); + cancel.addActionListener(e -> { + onCancel.run(); + dispose(); + }); + + JPanel buttonPane = new JPanel(); + buttonPane.setLayout(new FlowLayout(FlowLayout.RIGHT, 5, 5)); + buttonPane.add(submit); + buttonPane.add(cancel); + + c.gridx = 2; + c.insets = new Insets(5, 5, 5, 5); + mainPane.add(buttonPane, c); + + setContentPane(mainPane); + pack(); + setLocationRelativeTo(owner); + setVisible(true); + } + + private static String extractValue(JComponent comp) { + if (comp instanceof JTextArea) { + return ((JTextArea) comp).getText(); + } else if (comp instanceof JTextField) { + return ((JTextField) comp).getText(); + } else { + throw new IllegalStateException("FormDialog used with incorrect component"); + } + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java index 525b6ed8ae7..43077a8d426 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java @@ -10,6 +10,8 @@ public class ProofRegroupSettings extends AbstractPropertiesSettings { private static final String PREFIX = "[ProofRegrouping]Group"; + private static final List DEFAULT_GROUPS = List.of("Propositional expansion", + "Negation/conjunctive normal form", "Polynomial/inequation normal form", "Simplification"); private final List> groups = new ArrayList<>(); @@ -26,10 +28,10 @@ public void readSettings(Properties props) { } } if (groups.isEmpty()) { - addGroup("Propositional expansion", List.of("alpha", "delta")); - addGroup("Normal form", + addGroup(DEFAULT_GROUPS.get(0), List.of("alpha", "delta")); + addGroup(DEFAULT_GROUPS.get(1), List.of("negationNormalForm", "conjNormalForm")); - addGroup("Polynomials and inequations", + addGroup(DEFAULT_GROUPS.get(2), List.of("polySimp_expand", "polySimp_normalise", "polySimp_newSym", "polySimp_pullOutGcd", "polySimp_applyEq", "polySimp_applyEqRigid", "polySimp_directEquations", "polySimp_applyEqPseudo", @@ -39,7 +41,7 @@ public void readSettings(Properties props) { "inEqSimp_expand", "inEqSimp_saturate", "inEqSimp_pullOutGcd", "inEqSimp_special_nonLin", "simplify_literals")); - addGroup("Simplification", + addGroup(DEFAULT_GROUPS.get(3), List.of("simplify", "simplify_select", "simplify_enlarging")); } } @@ -64,4 +66,29 @@ public Map> getGroups() { } return m; } + + public Map> getUserGroups() { + Map> m = new HashMap<>(); + for (var pe : groups) { + var name = pe.getKey().substring(PREFIX.length()); + if (DEFAULT_GROUPS.contains(name)) { + continue; + } + m.put(name, List.of(pe.get().split(","))); + } + return m; + } + + public void removeGroup(String name) { + PropertyEntry toRemove = null; + for (var pe : groups) { + if (pe.getKey().substring(PREFIX.length()).equals(name)) { + toRemove = pe; + break; + } + } + groups.remove(toRemove); + propertyEntries.remove(toRemove); + properties.remove(toRemove); + } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java index b6eae28b991..319c4e21e3d 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java @@ -8,10 +8,13 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.settings.SettingsPanel; import de.uka.ilkd.key.gui.settings.SettingsProvider; +import de.uka.ilkd.key.gui.utilities.FormDialog; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.util.Pair; import net.miginfocom.layout.CC; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; /** * Settings for the proof slicing extension. @@ -19,6 +22,9 @@ * @author Arne Keller */ public class ProofRegroupSettingsProvider extends SettingsPanel implements SettingsProvider { + private static final Logger LOGGER = + LoggerFactory.getLogger(ProofRegroupSettingsProvider.class); + /** * Singleton instance of the settings. */ @@ -29,6 +35,9 @@ public class ProofRegroupSettingsProvider extends SettingsPanel implements Setti */ private static final String INTRO_LABEL = "Adjust heuristics groups here."; + /** + * The configured groups: name -> text area with heuristic names. + */ private final List> groups = new ArrayList<>(); /** @@ -53,6 +62,11 @@ public static ProofRegroupSettings getSettings() { @Override public JComponent getPanel(MainWindow window) { + return getPanel(window, null); + } + + @Override + public JComponent getPanel(MainWindow window, JDialog dialog) { ProofRegroupSettings ss = getSettings(); pCenter.removeAll(); @@ -64,9 +78,76 @@ public JComponent getPanel(MainWindow window) { groups.add(new Pair<>(e.getKey(), ta)); } + setupAddAndRemoveButtons(dialog, ss); + return this; } + private void setupAddAndRemoveButtons(JDialog dialog, ProofRegroupSettings ss) { + // remove any previously added buttons + for (int i = 0; i < pCenter.getComponentCount(); i++) { + if (pCenter.getComponent(i) instanceof JButton) { + pCenter.remove(i); + i--; + } + } + + var addNew = new JButton("Add new group"); + addNew.addActionListener(e -> { + try { + new FormDialog(dialog, "Add new group", + List.of(new Pair<>("Name", new JTextField()), + new Pair<>("Heuristics", new JTextArea())), + data -> { + var name = data.get(0).second; + if (ss.getGroups().containsKey(name)) { + return "Group name already in use!"; + } + return null; + }, + data -> { + var name = data.get(0).second; + var content = data.get(1).second; + var ta = + addTextArea(name, "", null, emptyValidator()); + ta.setText(content); + groups.add(new Pair<>(name, ta)); + ss.addGroup(name, List.of(ta.getText().split("\n"))); + + setupAddAndRemoveButtons(dialog, ss); + dialog.validate(); + dialog.repaint(); + }, () -> { + // ignore cancel + }); + } catch (Exception err) { + err.printStackTrace(); + } + }); + pCenter.add(addNew, "wrap"); + for (var group : ss.getUserGroups().keySet()) { + var remove = new JButton("Remove " + group); + remove.addActionListener(e -> { + try { + ss.removeGroup(group); + for (var groupPair : groups) { + if (groupPair.first.equals(group)) { + removeTitledComponent(groupPair.first); + groups.remove(groupPair); + setupAddAndRemoveButtons(dialog, ss); + dialog.validate(); + dialog.repaint(); + break; + } + } + } catch (Exception error) { + LOGGER.error("failed to remove group", error); + } + }); + pCenter.add(remove, "wrap"); + } + } + @Override public void applySettings(MainWindow window) { ProofRegroupSettings ss = getSettings(); From d79c97932cd00801b5ca961694fd8d128ebbd8d2 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sun, 2 Jul 2023 20:08:53 +0200 Subject: [PATCH 18/26] Fix handling of NoPos rule apps --- .../org/key_project/slicing/ProofReorder.java | 38 ++++++++++++------- 1 file changed, 24 insertions(+), 14 deletions(-) diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index ae4db025b20..322cde09b73 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -22,6 +22,7 @@ import org.key_project.slicing.graph.AnnotatedEdge; import org.key_project.slicing.graph.DependencyGraph; import org.key_project.slicing.graph.GraphNode; +import org.key_project.slicing.graph.PseudoInput; public final class ProofReorder { private ProofReorder() { @@ -57,6 +58,26 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) } List newOrder = new ArrayList<>(); Set newOrderSorted = new HashSet<>(); + + // First, get all nodes that do not directly connect to the dependency graph of the + // previous branch. These are taclets that do not have any formulas as direct inputs, + // e.g. sign_case_distinction. + // However, if one of these nodes splits the proof, it will be done last. + Node finalNode = null; + Node toCheck = root; + while (toCheck.getBranchLocation() == loc) { + DependencyNodeData data = toCheck.lookup(DependencyNodeData.class); + if (data.inputs.size() == 1 && data.inputs.get(0).first instanceof PseudoInput) { + if (toCheck.childrenCount() > 1) { + finalNode = toCheck; + break; + } + newOrder.add(toCheck); + newOrder.add(toCheck); + } + toCheck = toCheck.child(0); + } + while (!q.isEmpty()) { var nextNode = q.pop(); List finalNewOrder = newOrder; @@ -101,20 +122,6 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) outputs.forEach(q::addFirst); }); } - // Finally, get all nodes that do not directly connect to the dependency graph of the - // previous branch. These are taclets that do not have any formulas as direct inputs, - // e.g. sign_case_distinction - List nextQ = new ArrayList<>(); - newOrder.forEach(node -> node.childrenIterator().forEachRemaining(node2 -> { - while (node2 != null && !newOrderSorted.contains(node2) - && node2.getAppliedRuleApp() != null - && node2.getBranchLocation() == node.getBranchLocation()) { - nextQ.add(node2); - node2 = node2.childrenCount() > 0 ? node2.child(0) : null; - } - })); - Collections.sort(nextQ); - newOrder.addAll(nextQ); // add the next branches to the queue for (int i = 0; i < newOrder.size(); i++) { if (newOrder.get(i).childrenCount() != 1 @@ -130,6 +137,9 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) break; } } + if (finalNode != null) { + newOrder.add(finalNode); + } steps.put(loc, newOrder); } From f91bf7fa6d3a63720cbcfee5147a78854faa8e8a Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 8 Nov 2023 18:37:15 +0100 Subject: [PATCH 19/26] Spotless --- key.core/src/main/java/de/uka/ilkd/key/rule/PosRuleApp.java | 3 +++ .../java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java | 3 +-- .../main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java | 3 +++ .../main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java | 3 +++ .../de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java | 3 +++ .../main/java/org/key_project/util/collection/GraphUtil.java | 3 +++ .../main/java/org/key_project/slicing/DependencyTracker.java | 4 ++-- .../src/main/java/org/key_project/slicing/ProofRegroup.java | 3 +++ .../java/org/key_project/slicing/ProofRegroupSettings.java | 3 +++ .../org/key_project/slicing/ProofRegroupSettingsProvider.java | 3 +++ .../src/main/java/org/key_project/slicing/ProofReorder.java | 3 +++ .../main/java/org/key_project/slicing/RegroupExtension.java | 3 +++ .../main/java/org/key_project/slicing/ReorderingReplayer.java | 3 +++ .../main/java/org/key_project/slicing/SlicingExtension.java | 3 +-- .../java/org/key_project/slicing/graph/TrackedFunction.java | 3 +++ 15 files changed, 40 insertions(+), 6 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/PosRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/PosRuleApp.java index 493732009e6..62c3ed53725 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/PosRuleApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/PosRuleApp.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.rule; import de.uka.ilkd.key.logic.PosInOccurrence; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java index 16a4d478ff0..1215f7e5ec3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java @@ -6,6 +6,7 @@ * this class implements a TreeModel that can be displayed using the JTree class framework */ +import java.util.List; import javax.swing.tree.TreeNode; import de.uka.ilkd.key.proof.Node; @@ -14,8 +15,6 @@ import org.jspecify.annotations.NonNull; -import java.util.List; - class GUIProofTreeNode extends GUIAbstractTreeNode { private GUIAbstractTreeNode[] children; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java index 40761d6ab24..0cd2c374ec3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.utilities; import java.awt.*; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java index 9faa6fa490c..5e242c06f99 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof.reference; import de.uka.ilkd.key.proof.Node; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java index ae69104c587..9076ff94228 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof.reference; import de.uka.ilkd.key.logic.Term; diff --git a/key.util/src/main/java/org/key_project/util/collection/GraphUtil.java b/key.util/src/main/java/org/key_project/util/collection/GraphUtil.java index aea5a9760ca..2dbf1e87c8a 100644 --- a/key.util/src/main/java/org/key_project/util/collection/GraphUtil.java +++ b/key.util/src/main/java/org/key_project/util/collection/GraphUtil.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.collection; import java.util.ArrayDeque; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java index df5b7058c6e..4ce5635ea8e 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java @@ -13,11 +13,11 @@ import de.uka.ilkd.key.logic.OpCollector; import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.logic.PosInTerm; +import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.Function; import de.uka.ilkd.key.logic.op.Operator; -import de.uka.ilkd.key.logic.PosInTerm; -import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.proof.BranchLocation; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java index 12dea9865b1..ed78dcc0719 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.slicing; import java.util.ArrayDeque; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java index 43077a8d426..ec032d20e32 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.slicing; import java.util.ArrayList; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java index 319c4e21e3d..091e5b9112d 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.slicing; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index 322cde09b73..496ccb6fed5 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.slicing; import java.io.File; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java index 5154030a98e..80d4855adec 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.slicing; import javax.swing.*; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java b/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java index 38f592d4ac9..013594763f2 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.slicing; import java.util.*; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index 4227439b8f1..d7059893ac3 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -33,11 +33,10 @@ import org.key_project.slicing.ui.ShowGraphAction; import org.key_project.slicing.ui.SlicingLeftPanel; +import org.jspecify.annotations.NonNull; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import org.jspecify.annotations.NonNull; - /** * Proof slicing extension. * For more details see the user diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java index 219b70ea336..9aedb130a7a 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.slicing.graph; import java.util.Objects; From ebae922907d6c5587d9ffc9c34183157ffbca380 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 8 Nov 2023 18:48:47 +0100 Subject: [PATCH 20/26] Fix merge errors --- .git-blame-ignore-revs | 2 ++ .../de/uka/ilkd/key/logic/op/Function.java | 9 ----- .../key/nparser/builder/DefaultBuilder.java | 9 +++++ .../main/java/de/uka/ilkd/key/proof/Goal.java | 2 +- .../de/uka/ilkd/key/rule/PosTacletApp.java | 12 +++++++ .../de/uka/ilkd/key/util/LinkedHashMap.java | 1 - .../java/de/uka/ilkd/key/gui/TaskTree.java | 5 ++- .../gui/plugins/caching/CachingExtension.java | 8 ++--- .../plugins/caching/GotoReferenceAction.java | 2 +- .../caching/ReferenceSearchButton.java | 4 +-- .../plugins/caching/ReferenceSearchTable.java | 4 +-- .../ilkd/key/proof/reference/ClosedBy.java | 36 ------------------- .../slicing/DependencyTracker.java | 3 +- .../slicing/graph/DependencyGraph.java | 10 +++--- ...ilkd.key.gui.extension.api.KeYGuiExtension | 2 +- 15 files changed, 46 insertions(+), 63 deletions(-) delete mode 100644 key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs index 55a1b0ff102..7e57347e10d 100644 --- a/.git-blame-ignore-revs +++ b/.git-blame-ignore-revs @@ -4,3 +4,5 @@ b1ed8d6bc836ea40f357a839707d41fbb04ed6e2 # commit with manual formatting corrections a9fcedc6c8d96f2480549254a307b3fbe31f04bd +# formatting +f91bf7fa6d3a63720cbcfee5147a78854faa8e8a \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java index abf1215907b..23a62fa54de 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java @@ -6,7 +6,6 @@ import de.uka.ilkd.key.logic.Name; import de.uka.ilkd.key.logic.sort.NullSort; import de.uka.ilkd.key.logic.sort.Sort; -import de.uka.ilkd.key.proof.Node; import org.key_project.util.Strings; import org.key_project.util.collection.ImmutableArray; @@ -20,7 +19,6 @@ public class Function extends AbstractSortedOperator { private final boolean unique; private final boolean skolemConstant; - private Node introducedBy = null; // ------------------------------------------------------------------------- @@ -128,11 +126,4 @@ public Function rename(Name newName) { return new Function(newName, sort(), argSorts(), whereToBind(), unique, skolemConstant); } - public void setIntroducedBy(Node introducedBy) { - this.introducedBy = introducedBy; - } - - public Node getIntroducedBy() { - return introducedBy; - } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java index db2d44e6375..70bece72ac1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java @@ -6,6 +6,7 @@ import java.util.ArrayList; import java.util.Collection; import java.util.List; +import java.util.ResourceBundle; import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.Services; @@ -37,6 +38,9 @@ public class DefaultBuilder extends AbstractBuilder { public static final String LIMIT_SUFFIX = "$lmtd"; + private static final ResourceBundle bundle = + ResourceBundle.getBundle("de.uka.ilkd.key.nparser.builder.resources"); + protected final Services services; protected final NamespaceSet nss; @@ -119,6 +123,11 @@ public Sort visitArg_sorts_or_formula_helper(KeYParser.Arg_sorts_or_formula_help } } + /* + * @Override public Sort visitAny_sortId(KeYParser.Any_sortIdContext ctx) { Pair p = + * accept(ctx.any_sortId_help()); return toArraySort(p, ctx.EMPTYBRACKETS().size()); } + */ + /** * looks up a function, (program) variable or static query of the given name varfunc_id and the * argument terms args in the namespaces and java info. diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java index fe0adb35843..cba45dca750 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java @@ -658,7 +658,7 @@ private void adaptNamespacesNewGoals(final ImmutableList goalList) { for (Goal goal : goalList) { goal.node().addLocalProgVars(newProgVars); for (Function f : newFunctions) { - f.setIntroducedBy(goal.node().parent()); + FunctionTracker.setIntroducedBy(f, goal.node.parent()); } goal.node().addLocalFunctions(newFunctions); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java index e421c084bef..5eecf22e2e8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java @@ -71,6 +71,18 @@ public static PosTacletApp createPosTacletApp(FindTaclet taclet, MatchConditions return createPosTacletApp(taclet, matchCond.getInstantiations(), null, pos, services); } + + /** + * creates a PosTacletApp for the given taclet and a position information + * + * @param taclet the FindTaclet + * @param pos the PosInOccurrence storing the position where to apply the Taclet + */ + private PosTacletApp(FindTaclet taclet, PosInOccurrence pos) { + super(taclet); + this.pos = pos; + } + /** * creates a PosTacletApp for the given taclet with some known instantiations and a position * information diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMap.java b/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMap.java index f68c9fc72f3..1bcb464aeaf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMap.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMap.java @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.util; - import java.util.Iterator; import java.util.Map; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java index 96e2e53b66b..41d08a7e693 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java @@ -3,7 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui; -import java.awt.*; +import java.awt.BorderLayout; +import java.awt.Component; +import java.awt.Font; import java.awt.event.MouseAdapter; import java.awt.event.MouseEvent; import java.awt.event.MouseListener; @@ -347,6 +349,7 @@ public Component getTreeCellRendererComponent(JTree list, Object value, boolean setToolTipText("Open proof"); } } + } return this; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java index d3a376ff7ab..84b4a82fe2d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java @@ -114,9 +114,9 @@ public void ruleApplied(ProofEvent e) { goal.setEnabled(false); goal.node().register(c, ClosedBy.class); - c.getProof() + c.proof() .addProofDisposedListenerFirst( - new CopyBeforeDispose(mediator, c.getProof(), p)); + new CopyBeforeDispose(mediator, c.proof(), p)); } } } @@ -247,7 +247,7 @@ public void proofDisposing(ProofDisposedEvent e) { } else { newProof.closedGoals().stream() .filter(x -> x.node().lookup(ClosedBy.class) != null - && x.node().lookup(ClosedBy.class).getProof() == referencedProof) + && x.node().lookup(ClosedBy.class).proof() == referencedProof) .forEach(x -> { newProof.reOpenGoal(x); x.node().deregister(x.node().lookup(ClosedBy.class), ClosedBy.class); @@ -363,7 +363,7 @@ public void actionPerformed(ActionEvent e) { Goal current = node.proof().getClosedGoal(node); try { mediator.stopInterface(true); - new CopyingProofReplayer(c.getProof(), node.proof()).copy(c.getNode(), current); + new CopyingProofReplayer(c.proof(), node.proof()).copy(c.node(), current); mediator.startInterface(true); } catch (Exception ex) { LOGGER.error("failed to copy proof ", ex); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/GotoReferenceAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/GotoReferenceAction.java index e88e6a81e36..4071642cdf9 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/GotoReferenceAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/GotoReferenceAction.java @@ -39,7 +39,7 @@ public GotoReferenceAction(KeYMediator mediator, Node node) { @Override public void actionPerformed(ActionEvent e) { - Node ref = node.lookup(ClosedBy.class).getNode(); + Node ref = node.lookup(ClosedBy.class).node(); mediator.getSelectionModel().setSelectedNode(ref); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java index fea52aaafa7..dec2bab3847 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java @@ -59,9 +59,9 @@ public void actionPerformed(ActionEvent e) { p.closeGoal(goal); goal.node().register(c, ClosedBy.class); - c.getProof() + c.proof() .addProofDisposedListenerFirst(new CachingExtension.CopyBeforeDispose( - mediator, c.getProof(), p)); + mediator, c.proof(), p)); } } var dialog = diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java index f9f3bd20556..645a539f746 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java @@ -98,9 +98,9 @@ public Object getValueAt(int row, int column) { if (c == null) { return "no reference found"; } else { - int i = mediator.getCurrentlyOpenedProofs().indexOf(c.getProof()) + 1; + int i = mediator.getCurrentlyOpenedProofs().indexOf(c.proof()) + 1; return String.format("reference available (proof %d, node %d)", i, - c.getNode().serialNr()); + c.node().serialNr()); } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java deleted file mode 100644 index 5e242c06f99..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java +++ /dev/null @@ -1,36 +0,0 @@ -/* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2 - * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.proof.reference; - -import de.uka.ilkd.key.proof.Node; -import de.uka.ilkd.key.proof.Proof; - -/** - * Indicates that a branch has been closed by "reference" to another closed proof. - * - * @author Arne Keller - */ -public class ClosedBy { - /** - * The proof referenced. - */ - private Proof proof; - /** - * The node referenced. - */ - private Node node; - - public ClosedBy(Proof proof, Node node) { - this.proof = proof; - this.node = node; - } - - public Proof getProof() { - return proof; - } - - public Node getNode() { - return node; - } -} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java index 4ce5635ea8e..198f5b90515 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java @@ -19,6 +19,7 @@ import de.uka.ilkd.key.logic.op.Function; import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.proof.BranchLocation; +import de.uka.ilkd.key.proof.FunctionTracker; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; @@ -197,7 +198,7 @@ private List> inputsOfNode(Node n, Set continue; } - var a = ((Function) z).getIntroducedBy(); + var a = FunctionTracker.getIntroducedBy(((Function) z)); if (a != null && a != n) { input.add(new Pair<>( graph.getFunctionNode((Function) z, a.getBranchLocation()), false)); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java index 7c5cd050641..4cf60e9684c 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java @@ -9,6 +9,7 @@ import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.op.Function; import de.uka.ilkd.key.proof.BranchLocation; +import de.uka.ilkd.key.proof.FunctionTracker; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.util.Pair; @@ -374,7 +375,7 @@ public TrackedFunction getFunctionNode(Function function, BranchLocation loc) { return candidate; } graph.addVertex(candidate); - var edges = edgeDataReversed.get(function.getIntroducedBy()); + var edges = edgeDataReversed.get(FunctionTracker.getIntroducedBy(function)); var sourcesDone = new HashSet<>(); Collection newEdges = new ArrayList<>(); for (var x : edges) { @@ -383,12 +384,13 @@ public TrackedFunction getFunctionNode(Function function, BranchLocation loc) { continue; } sourcesDone.add(g); - AnnotatedEdge e = new AnnotatedEdge(function.getIntroducedBy(), false); + AnnotatedEdge e = new AnnotatedEdge(FunctionTracker.getIntroducedBy(function), false); graph.addEdge(g, candidate, e); newEdges.add(e); } - edgeDataReversed.get(function.getIntroducedBy()).addAll(newEdges); - DependencyNodeData n = function.getIntroducedBy().lookup(DependencyNodeData.class); + edgeDataReversed.get(FunctionTracker.getIntroducedBy(function)).addAll(newEdges); + DependencyNodeData n = + FunctionTracker.getIntroducedBy(function).lookup(DependencyNodeData.class); if (n != null) { n.outputs.add(candidate); } diff --git a/keyext.slicing/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/keyext.slicing/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension index eab98ab1cc6..49e7314e4b6 100644 --- a/keyext.slicing/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension +++ b/keyext.slicing/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension @@ -1,2 +1,2 @@ org.key_project.slicing.SlicingExtension -org.key_project.slicing.RegroupExtension \ No newline at end of file +org.key_project.slicing.RegroupExtension From 1d1aa1d093e161d54e4ef67bda4681997d9260fe Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 8 Nov 2023 18:59:48 +0100 Subject: [PATCH 21/26] Repair reordering functionality --- .../uka/ilkd/key/proof/FunctionTracker.java | 26 +++++++++++++++++++ .../org/key_project/slicing/ProofReorder.java | 5 ++++ .../slicing/ReorderingReplayer.java | 2 +- .../key_project/slicing/SlicingExtension.java | 6 +++++ 4 files changed, 38 insertions(+), 1 deletion(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/proof/FunctionTracker.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/FunctionTracker.java b/key.core/src/main/java/de/uka/ilkd/key/proof/FunctionTracker.java new file mode 100644 index 00000000000..31b4cb26ccd --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/FunctionTracker.java @@ -0,0 +1,26 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.proof; + +import java.lang.ref.WeakReference; +import java.util.WeakHashMap; + +import de.uka.ilkd.key.logic.op.Function; + +public final class FunctionTracker { + private static final WeakHashMap> mapping = new WeakHashMap<>(); + + private FunctionTracker() { + + } + + public static void setIntroducedBy(Function f, Node n) { + mapping.put(f, new WeakReference<>(n)); + } + + public static Node getIntroducedBy(Function f) { + var x = mapping.get(f); + return x != null ? x.get() : null; + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index 496ccb6fed5..57f93d9c6b4 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -35,6 +35,7 @@ private ProofReorder() { public static void reorderProof(Proof proof, DependencyGraph depGraph) throws IOException, ProofInputException, ProblemLoaderException, IntermediateProofReplayer.BuiltInConstructionException { + depGraph.ensureProofIsTracked(proof); MainWindow.getInstance().getMediator().stopInterface(true); SortedMap> steps = new TreeMap<>(); @@ -70,6 +71,10 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) Node toCheck = root; while (toCheck.getBranchLocation() == loc) { DependencyNodeData data = toCheck.lookup(DependencyNodeData.class); + if (data == null) { + finalNode = toCheck.parent(); + break; // closed goal + } if (data.inputs.size() == 1 && data.inputs.get(0).first instanceof PseudoInput) { if (toCheck.childrenCount() > 1) { finalNode = toCheck; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java b/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java index 013594763f2..fc0a0cbd1e4 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java @@ -41,7 +41,7 @@ public void copy() nodeQueue.addAll(e.getValue()); } - while (!nodeQueue.isEmpty()) { + while (!nodeQueue.isEmpty() && !queue.isEmpty()) { Node nextNode = nodeQueue.pop(); Goal nextGoal = queue.pop(); // skip nextNode if it is a closed goal diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index d7059893ac3..9e3d29abe05 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -193,6 +193,12 @@ public JToolBar getToolbar(MainWindow mainWindow) { b.setText("Reorder"); b.addActionListener(e -> { KeYMediator m = MainWindow.getInstance().getMediator(); + Proof p = m.getSelectedProof(); + if (!p.closed()) { + JOptionPane.showMessageDialog(MainWindow.getInstance(), + "Cannot reorder incomplete proof", "Error", JOptionPane.ERROR_MESSAGE); + return; + } try { ProofReorder.reorderProof(m.getSelectedProof(), trackers.get(m.getSelectedProof()).getDependencyGraph()); From c812a7b804d82859b662c13d9a5d25498f3e015f Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sun, 12 Nov 2023 16:27:57 +0100 Subject: [PATCH 22/26] Fix proof reordering --- .../src/main/java/org/key_project/slicing/ProofReorder.java | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index 57f93d9c6b4..81caa9eb524 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -54,6 +54,7 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) done.add(loc); System.out.println("doing branch " + loc); + // q: the list of dependency graph nodes "currently available" for proof steps Deque q = new ArrayDeque<>(); for (int i = 1; i <= root.sequent().size(); i++) { var node = depGraph.getGraphNode(proof, loc, @@ -72,7 +73,6 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) while (toCheck.getBranchLocation() == loc) { DependencyNodeData data = toCheck.lookup(DependencyNodeData.class); if (data == null) { - finalNode = toCheck.parent(); break; // closed goal } if (data.inputs.size() == 1 && data.inputs.get(0).first instanceof PseudoInput) { @@ -88,7 +88,6 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) while (!q.isEmpty()) { var nextNode = q.pop(); - List finalNewOrder = newOrder; depGraph.outgoingEdgesOf(nextNode).forEach(node -> { var newLoc = node.getBranchLocation(); if (!newLoc.equals(loc)) { @@ -122,7 +121,7 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) q.addLast(nextNode); return; } - finalNewOrder.add(node); + newOrder.add(node); newOrderSorted.add(node); var outputs = depGraph.outputsOf(node).collect(Collectors.toList()); From 186341038dc1f70b1be6d5d11e82ddc8e394332e Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sun, 12 Nov 2023 16:41:20 +0100 Subject: [PATCH 23/26] Fix another reordering edge case --- .../src/main/java/org/key_project/slicing/ProofReorder.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index 81caa9eb524..a8c78e7c93b 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -80,7 +80,7 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) finalNode = toCheck; break; } - newOrder.add(toCheck); + // Do this one first. newOrder.add(toCheck); } toCheck = toCheck.child(0); From f1177a4f647aa13149fe89c92a2613e6284c2705 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sun, 12 Nov 2023 16:59:29 +0100 Subject: [PATCH 24/26] Fix pruning after regrouping --- .../gui/prooftree/GUIAbstractTreeNode.java | 4 +- .../org/key_project/slicing/ProofRegroup.java | 15 ++-- .../org/key_project/slicing/ProofReorder.java | 5 ++ .../key_project/slicing/RegroupExtension.java | 78 +++++++++++++++++-- 4 files changed, 86 insertions(+), 16 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java index 2f937cdc2fa..ff83b4c1bde 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java @@ -65,7 +65,9 @@ public TreeNode[] getPath() { LinkedList path = new LinkedList<>(); TreeNode n = this; path.addFirst(n); - while ((n = n.getParent()) != null) { + // walk up the parent chain + // (robustness: do not continue indefinitely for self-parents) + while (n.getParent() != n && (n = n.getParent()) != null) { path.addFirst(n); } return path.toArray(new TreeNode[0]); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java index ed78dcc0719..c9736169979 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java @@ -36,7 +36,7 @@ public static void regroupProof(Proof proof, DependencyGraph graph) { * * simplify_enlarging, simplify, simplify_select */ - var GROUPS = ProofRegroupSettingsProvider.getSettings().getGroups(); + var groups = ProofRegroupSettingsProvider.getSettings().getGroups(); Deque q = new ArrayDeque<>(); q.add(proof.root()); while (!q.isEmpty()) { @@ -49,12 +49,12 @@ public static void regroupProof(Proof proof, DependencyGraph graph) { continue; } Rule rule = r.rule(); - if (rule instanceof Taclet) { - var ruleSets = ((Taclet) rule).getRuleSets(); + if (rule instanceof Taclet taclet) { + var ruleSets = taclet.getRuleSets(); String matchingGroup = null; for (var name : ruleSets) { - for (String i : GROUPS.keySet()) { - if (GROUPS.get(i).contains(name.toString())) { + for (String i : groups.keySet()) { + if (groups.get(i).contains(name.toString())) { matchingGroup = i; break; } @@ -70,8 +70,7 @@ public static void regroupProof(Proof proof, DependencyGraph graph) { var n2 = n.child(0); var r2 = n2.getAppliedRuleApp(); var rule2 = r2.rule(); - if (r2 instanceof PosRuleApp && rule2 instanceof Taclet) { - var p2 = (PosRuleApp) r2; + if (r2 instanceof PosRuleApp p2 && rule2 instanceof Taclet) { var graphNode = graph.getGraphNode(proof, n2.getBranchLocation(), p2.posInOccurrence()); Node finalN = n; @@ -82,7 +81,7 @@ public static void regroupProof(Proof proof, DependencyGraph graph) { var ruleSets2 = ((Taclet) rule2).getRuleSets(); var found = false; for (var name : ruleSets2) { - if (GROUPS.get(matchingGroup).contains(name.toString())) { + if (groups.get(matchingGroup).contains(name.toString())) { found = true; break; } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index a8c78e7c93b..2a0edac4327 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -27,6 +27,11 @@ import org.key_project.slicing.graph.GraphNode; import org.key_project.slicing.graph.PseudoInput; +/** + * Proof reordering functionality. + * + * @author Arne Keller + */ public final class ProofReorder { private ProofReorder() { diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java index 80d4855adec..334929a2ee4 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java @@ -3,28 +3,38 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.slicing; +import java.util.ArrayList; +import java.util.List; import javax.swing.*; +import de.uka.ilkd.key.control.InteractionListener; +import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; import de.uka.ilkd.key.gui.settings.SettingsProvider; +import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.macros.ProofMacro; +import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo; +import de.uka.ilkd.key.rule.BuiltInRule; +import de.uka.ilkd.key.rule.IBuiltInRuleApp; +import de.uka.ilkd.key.rule.RuleApp; /** - * Proof slicing extension. - * For more details see the user - * guide. + * Proof regrouping and reordering extension. * * @author Arne Keller */ -@KeYGuiExtension.Info(name = "Slicing", +@KeYGuiExtension.Info(name = "Reordering and regrouping", description = "Author: Arne Keller ", experimental = false, optional = true, priority = 9001) public class RegroupExtension implements KeYGuiExtension, - KeYGuiExtension.Settings, - KeYGuiExtension.Toolbar { - + KeYGuiExtension.Startup, KeYGuiExtension.Settings, + KeYGuiExtension.Toolbar, InteractionListener { @Override public JToolBar getToolbar(MainWindow mainWindow) { @@ -35,4 +45,58 @@ public JToolBar getToolbar(MainWindow mainWindow) { public SettingsProvider getSettings() { return new ProofRegroupSettingsProvider(); } + + @Override + public void init(MainWindow window, KeYMediator mediator) { + mediator.getUI().getProofControl().addInteractionListener(this); + } + + @Override + public void runPrune(Node node) { + if (node.isHideInProofTree()) { + // Perhaps there are some nodes below the prune target in this group. + // These should be removed from the proof tree view. + var groupNode = node.parent(); + while (groupNode.getGroup() == null) { + var prev = groupNode; + groupNode = groupNode.parent(); + // robustness: no infinite loop + // (should never happen anyhow) + if (prev == groupNode) { + return; + } + } + var groupNodes = groupNode.getGroup(); + var removedAfter = groupNodes.indexOf(node); + groupNode.setGroup(new ArrayList<>(groupNodes.subList(0, removedAfter + 1))); + } + } + + @Override + public void settingChanged(Proof proof, de.uka.ilkd.key.settings.Settings settings, + SettingType type, String message) { + + } + + @Override + public void runMacro(Node node, ProofMacro macro, PosInOccurrence posInOcc, + ProofMacroFinishedInfo info) { + + } + + @Override + public void runBuiltInRule(Node node, IBuiltInRuleApp app, BuiltInRule rule, + PosInOccurrence pos, boolean forced) { + + } + + @Override + public void runAutoMode(List initialGoals, Proof proof, ApplyStrategyInfo info) { + + } + + @Override + public void runRule(Node goal, RuleApp app) { + + } } From 3107e2057c739938f7861e9a348d448a84eb272a Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sun, 12 Nov 2023 17:09:43 +0100 Subject: [PATCH 25/26] Move actions to appropriate extension --- .../key_project/slicing/RegroupExtension.java | 55 ++++++++++++++++++- .../key_project/slicing/SlicingExtension.java | 46 +--------------- 2 files changed, 55 insertions(+), 46 deletions(-) diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java index 334929a2ee4..bfa1e8a4cab 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java @@ -9,6 +9,7 @@ import de.uka.ilkd.key.control.InteractionListener; import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; import de.uka.ilkd.key.gui.settings.SettingsProvider; @@ -22,6 +23,9 @@ import de.uka.ilkd.key.rule.IBuiltInRuleApp; import de.uka.ilkd.key.rule.RuleApp; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * Proof regrouping and reordering extension. * @@ -35,10 +39,59 @@ public class RegroupExtension implements KeYGuiExtension, KeYGuiExtension.Startup, KeYGuiExtension.Settings, KeYGuiExtension.Toolbar, InteractionListener { + private static final Logger LOGGER = LoggerFactory.getLogger(RegroupExtension.class); @Override public JToolBar getToolbar(MainWindow mainWindow) { - return new JToolBar(); + JToolBar bar = new JToolBar(); + JButton b = new JButton(); + b.setText("Reorder"); + b.addActionListener(e -> { + KeYMediator m = MainWindow.getInstance().getMediator(); + Proof p = m.getSelectedProof(); + if (!p.closed()) { + JOptionPane.showMessageDialog(MainWindow.getInstance(), + "Cannot reorder incomplete proof", "Error", JOptionPane.ERROR_MESSAGE); + return; + } + try { + var depTracker = m.getSelectedProof().lookup(DependencyTracker.class); + if (depTracker == null) { + JOptionPane.showMessageDialog(MainWindow.getInstance(), + "Cannot reorder proof without dependency tracker", "Error", + JOptionPane.ERROR_MESSAGE); + return; + } + var depGraph = depTracker.getDependencyGraph(); + ProofReorder.reorderProof(m.getSelectedProof(), depGraph); + } catch (Exception exc) { + LOGGER.error("failed to reorder proof ", exc); + MainWindow.getInstance().getMediator().startInterface(true); + IssueDialog.showExceptionDialog(MainWindow.getInstance(), exc); + } + }); + bar.add(b); + JButton b2 = new JButton(); + b2.setText("Regroup"); + b2.addActionListener(e -> { + KeYMediator m = MainWindow.getInstance().getMediator(); + try { + var depTracker = m.getSelectedProof().lookup(DependencyTracker.class); + if (depTracker == null) { + JOptionPane.showMessageDialog(MainWindow.getInstance(), + "Cannot regroup proof without dependency tracker", "Error", + JOptionPane.ERROR_MESSAGE); + return; + } + var depGraph = depTracker.getDependencyGraph(); + ProofRegroup.regroupProof(m.getSelectedProof(), depGraph); + } catch (Exception exc) { + LOGGER.error("", exc); + IssueDialog.showExceptionDialog(MainWindow.getInstance(), exc); + } + }); + bar.add(b2); + return bar; } @Override diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index 9e3d29abe05..2849b6d50a5 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -14,7 +14,6 @@ import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.core.KeYSelectionEvent; import de.uka.ilkd.key.core.KeYSelectionListener; -import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.extension.api.ContextMenuAdapter; import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; @@ -34,8 +33,6 @@ import org.key_project.slicing.ui.SlicingLeftPanel; import org.jspecify.annotations.NonNull; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; /** * Proof slicing extension. @@ -54,11 +51,8 @@ public class SlicingExtension implements KeYGuiExtension, KeYGuiExtension.Startup, KeYGuiExtension.LeftPanel, KeYGuiExtension.Settings, - KeYGuiExtension.Toolbar, KeYSelectionListener, ProofDisposedListener { - private static final Logger LOGGER = LoggerFactory.getLogger(SlicingExtension.class); - /** * Collection of dependency trackers attached to proofs. */ @@ -119,7 +113,7 @@ public List getContextActions(@NonNull KeYMediator mediator, } @Override - public void selectedProofChanged(KeYSelectionEvent e) { + public void selectedProofChanged(KeYSelectionEvent e) { createTrackerForProof(e.getSource().getSelectedProof()); } @@ -185,42 +179,4 @@ public SettingsProvider getSettings() { public void enableSafeModeForNextProof() { this.enableSafeModeForNextProof = true; } - - @Override - public JToolBar getToolbar(MainWindow mainWindow) { - JToolBar bar = new JToolBar(); - JButton b = new JButton(); - b.setText("Reorder"); - b.addActionListener(e -> { - KeYMediator m = MainWindow.getInstance().getMediator(); - Proof p = m.getSelectedProof(); - if (!p.closed()) { - JOptionPane.showMessageDialog(MainWindow.getInstance(), - "Cannot reorder incomplete proof", "Error", JOptionPane.ERROR_MESSAGE); - return; - } - try { - ProofReorder.reorderProof(m.getSelectedProof(), - trackers.get(m.getSelectedProof()).getDependencyGraph()); - } catch (Exception exc) { - LOGGER.error("failed to reorder proof ", exc); - MainWindow.getInstance().getMediator().startInterface(true); - IssueDialog.showExceptionDialog(MainWindow.getInstance(), exc); - } - }); - bar.add(b); - JButton b2 = new JButton(); - b2.setText("Regroup"); - b2.addActionListener(e -> { - KeYMediator m = MainWindow.getInstance().getMediator(); - try { - ProofRegroup.regroupProof(m.getSelectedProof(), - trackers.get(m.getSelectedProof()).getDependencyGraph()); - } catch (Exception exc) { - exc.printStackTrace(); - } - }); - bar.add(b2); - return bar; - } } From 7246b1e03a77e6645d55624578a338f7b265d7b9 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 8 Mar 2024 12:38:30 +0100 Subject: [PATCH 26/26] Fix merge errors + test for FunctionTracker --- .../de/uka/ilkd/key/java/Recoder2KeY.java | 1 - .../de/uka/ilkd/key/logic/OpCollector.java | 3 +- .../de/uka/ilkd/key/logic/op/Function.java | 129 ---------------- .../uka/ilkd/key/proof/FunctionTracker.java | 8 +- .../main/java/de/uka/ilkd/key/proof/Goal.java | 1 + .../proof/replay/AbstractProofReplayer.java | 10 -- .../java/de/uka/ilkd/key/rule/Taclet.java | 6 +- .../rule/tacletbuilder/TacletGenerator.java | 2 +- .../ilkd/key/gui/prooftree/ProofTreeView.java | 3 - .../ilkd/key/gui/utilities/FormDialog.java | 40 +++-- .../proof/reference/ProgramMethodFinder.java | 39 ----- .../slicing/DependencyTracker.java | 12 +- .../slicing/ProofRegroupSettings.java | 33 ++-- .../slicing/ProofRegroupSettingsProvider.java | 17 ++- .../org/key_project/slicing/ProofReorder.java | 19 ++- .../slicing/graph/DependencyGraph.java | 2 +- .../slicing/graph/TrackedFunction.java | 3 +- .../slicing/FunctionTrackerTest.java | 34 +++++ .../testcase/testFunctionTracker.proof | 143 ++++++++++++++++++ 19 files changed, 259 insertions(+), 246 deletions(-) delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java delete mode 100644 key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java create mode 100644 keyext.slicing/src/test/java/org/key_project/slicing/FunctionTrackerTest.java create mode 100644 keyext.slicing/src/test/resources/testcase/testFunctionTracker.proof diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java index d0d8456447a..04f81ecef57 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java @@ -22,7 +22,6 @@ import de.uka.ilkd.key.proof.io.consistency.FileRepo; import de.uka.ilkd.key.util.*; import de.uka.ilkd.key.util.LinkedHashMap; -import de.uka.ilkd.key.util.Pair; import de.uka.ilkd.key.util.parsing.HasLocation; import org.key_project.logic.Name; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/OpCollector.java b/key.core/src/main/java/de/uka/ilkd/key/logic/OpCollector.java index 178786cef84..9cc8fbc03a6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/OpCollector.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/OpCollector.java @@ -9,7 +9,8 @@ import java.util.Set; import de.uka.ilkd.key.logic.op.ElementaryUpdate; -import de.uka.ilkd.key.logic.op.Operator; + +import org.key_project.logic.op.Operator; /** * Collects all operators occurring in the traversed term. diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java deleted file mode 100644 index 23a62fa54de..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java +++ /dev/null @@ -1,129 +0,0 @@ -/* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2 - * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.logic.op; - -import de.uka.ilkd.key.logic.Name; -import de.uka.ilkd.key.logic.sort.NullSort; -import de.uka.ilkd.key.logic.sort.Sort; - -import org.key_project.util.Strings; -import org.key_project.util.collection.ImmutableArray; - - -/** - * Objects of this class represent function and predicate symbols. Note that program variables are a - * separate syntactic category, and not a type of function. - */ -public class Function extends AbstractSortedOperator { - - private final boolean unique; - private final boolean skolemConstant; - - - // ------------------------------------------------------------------------- - // constructors - // ------------------------------------------------------------------------- - - Function(Name name, Sort sort, ImmutableArray argSorts, - ImmutableArray whereToBind, boolean unique, boolean isRigid, - boolean isSkolemConstant) { - super(name, argSorts, sort, whereToBind, isRigid); - - this.unique = unique; - skolemConstant = isSkolemConstant; - assert sort != Sort.UPDATE; - assert !(unique && sort == Sort.FORMULA); - assert !(sort instanceof NullSort) || name.toString().equals("null") - : "Functions with sort \"null\" are not allowed: " + this; - } - - public Function(Name name, Sort sort, ImmutableArray argSorts, - ImmutableArray whereToBind, boolean unique) { - this(name, sort, argSorts, whereToBind, unique, true, false); - } - - public Function(Name name, Sort sort, ImmutableArray argSorts, - ImmutableArray whereToBind, boolean unique, boolean isSkolemConstant) { - this(name, sort, argSorts, whereToBind, unique, true, isSkolemConstant); - } - - public Function(Name name, Sort sort, Sort[] argSorts, Boolean[] whereToBind, boolean unique) { - this(name, sort, new ImmutableArray<>(argSorts), - whereToBind == null ? null : new ImmutableArray<>(whereToBind), unique); - } - - public Function(Name name, Sort sort, Sort[] argSorts, Boolean[] whereToBind, boolean unique, - boolean isSkolemConstant) { - this(name, sort, new ImmutableArray<>(argSorts), - whereToBind == null ? null : new ImmutableArray<>(whereToBind), unique, - isSkolemConstant); - } - - Function(Name name, Sort sort, ImmutableArray argSorts, boolean isRigid) { - this(name, sort, argSorts, null, false, isRigid, false); - } - - public Function(Name name, Sort sort, ImmutableArray argSorts) { - this(name, sort, argSorts, null, false); - } - - public Function(Name name, Sort sort, Sort... argSorts) { - this(name, sort, argSorts, null, false); - } - - public Function(Name name, Sort sort, boolean isSkolemConstant, Sort... argSorts) { - this(name, sort, argSorts, null, false, isSkolemConstant); - } - - public Function(Name name, Sort sort) { - this(name, sort, new ImmutableArray<>(), null, false); - } - - public Function(Name name, Sort sort, boolean isSkolemConstant) { - this(name, sort, new ImmutableArray<>(), null, false, true, isSkolemConstant); - } - - - // ------------------------------------------------------------------------- - // public interface - // ------------------------------------------------------------------------- - - /** - * Indicates whether the function or predicate symbol has the "uniqueness" property. For two - * unique symbols f1: A1 -> B1, f2: A2 -> B2 by definition we have (1) f1(x) != f1(y) for all x, - * y in A1 with x != y (i.e., injectivity), and (2) f1(x) != f2(y) for all x in A1, y in A2. - */ - public final boolean isUnique() { - return unique; - } - - public final boolean isSkolemConstant() { - return skolemConstant; - } - - @Override - public final String toString() { - return (name() + (whereToBind() == null ? "" : "{" + whereToBind() + "}")); - } - - /** - * Returns a parsable string representation of the declaration of this function or predicate - * symbol. - */ - public final String proofToString() { - StringBuilder s = - new StringBuilder((sort() == Sort.FORMULA ? "" : sort().toString()) + " "); - s.append(name()); - if (arity() > 0) { - s.append(Strings.formatAsList(argSorts(), "(", ",", ")")); - } - s.append(";\n"); - return s.toString(); - } - - public Function rename(Name newName) { - return new Function(newName, sort(), argSorts(), whereToBind(), unique, skolemConstant); - } - -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/FunctionTracker.java b/key.core/src/main/java/de/uka/ilkd/key/proof/FunctionTracker.java index 31b4cb26ccd..82a86b59b1c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/FunctionTracker.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/FunctionTracker.java @@ -6,21 +6,21 @@ import java.lang.ref.WeakReference; import java.util.WeakHashMap; -import de.uka.ilkd.key.logic.op.Function; +import org.key_project.logic.op.Function; public final class FunctionTracker { - private static final WeakHashMap> mapping = new WeakHashMap<>(); + private static final WeakHashMap> MAPPING = new WeakHashMap<>(); private FunctionTracker() { } public static void setIntroducedBy(Function f, Node n) { - mapping.put(f, new WeakReference<>(n)); + MAPPING.put(f, new WeakReference<>(n)); } public static Node getIntroducedBy(Function f) { - var x = mapping.get(f); + var x = MAPPING.get(f); return x != null ? x.get() : null; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java index 99e46e36e15..2df4519234b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java @@ -30,6 +30,7 @@ import de.uka.ilkd.key.util.properties.Properties; import de.uka.ilkd.key.util.properties.Properties.Property; +import org.key_project.logic.op.Function; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java index 13c4af02c1d..a8db47e385f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof.replay; -import java.io.File; import java.util.ArrayList; import java.util.Collection; import java.util.List; @@ -94,15 +93,6 @@ protected ImmutableList reApplyRuleApp(Node node, Goal openGoal) throws IntermediateProofReplayer.BuiltInConstructionException { RuleApp ruleApp = node.getAppliedRuleApp(); ImmutableList nextGoals; - System.out.println( - "reapplying " + node.serialNr() + " " + node.getAppliedRuleApp().rule().displayName() - + " on node " + openGoal.node().serialNr()); - - try { - openGoal.proof().saveToFile(new File("/tmp/p" + openGoal.node().serialNr() + ".proof")); - } catch (Exception e) { - // . - } if (ruleApp.rule() instanceof BuiltInRule) { IBuiltInRuleApp builtInRuleApp = constructBuiltinApp(node, openGoal); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java index d930c46b70f..adda0d65ba5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java @@ -8,7 +8,6 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.logic.op.QuantifiableVariable; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.proof.Goal; @@ -23,6 +22,7 @@ import org.key_project.logic.Name; import org.key_project.logic.Named; +import org.key_project.logic.op.Operator; import org.key_project.util.EqualsModProofIrrelevancy; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; @@ -728,8 +728,8 @@ public Set collectSchemaVars() { } for (Operator op : oc.ops()) { - if (op instanceof SchemaVariable) { - result.add((SchemaVariable) op); + if (op instanceof SchemaVariable sv) { + result.add(sv); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java index 207e9cf806e..a7b9f415b5f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java @@ -812,7 +812,7 @@ private TermAndBoundVarPair replaceBoundLogicVars(Term t, TermServices services) final OpCollector oc = new OpCollector(); oc.visit(t); final Set usedNames = new LinkedHashSet<>(); - for (Operator op : oc.ops()) { + for (var op : oc.ops()) { usedNames.add(op.name()); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java index b0acd48cfe9..d0361823e12 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java @@ -536,9 +536,6 @@ private void setProof(Proof p) { for (int i : rowsToExpand) { delegateView.expandRow(i); } - if (filter != null) { - delegateModel.setFilter(filter, true); - } // Restore previous scroll position. JScrollPane scroller = (JScrollPane) delegateView.getParent().getParent(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java index 0cd2c374ec3..b8b06d9034a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java @@ -4,19 +4,19 @@ package de.uka.ilkd.key.gui.utilities; import java.awt.*; -import java.util.ArrayList; +import java.util.HashMap; import java.util.List; +import java.util.Map; import java.util.function.Consumer; import java.util.function.Function; import javax.swing.*; -import de.uka.ilkd.key.util.Pair; - import org.slf4j.Logger; import org.slf4j.LoggerFactory; /** - * Simple and generic input form dialog. Support {@link JTextField} and {@link JTextArea} as fields. + * Simple and generic input form dialog. Supports {@link JTextField} and {@link JTextArea} as + * fields. * * @author Arne Keller */ @@ -33,9 +33,9 @@ public class FormDialog extends JDialog { * @param onSubmit callback for submit action * @param onCancel callback for cancel action */ - public FormDialog(JDialog owner, String title, List> comps, - Function>, String> validate, - Consumer>> onSubmit, Runnable onCancel) { + public FormDialog(JDialog owner, String title, List comps, + Function, String> validate, + Consumer> onSubmit, Runnable onCancel) { super(owner); setTitle(title); @@ -55,10 +55,10 @@ public FormDialog(JDialog owner, String title, List> co for (var comp : comps) { c.gridx = 1; - mainPane.add(new JLabel(comp.first), c.clone()); + mainPane.add(new JLabel(comp.name), c.clone()); c.gridx = 2; c.fill = GridBagConstraints.HORIZONTAL; - mainPane.add(comp.second, c.clone()); + mainPane.add(comp.element, c.clone()); c.gridy++; } @@ -66,9 +66,9 @@ public FormDialog(JDialog owner, String title, List> co var submit = new JButton("Submit"); submit.addActionListener(e -> { try { - List> data = new ArrayList<>(); + Map data = new HashMap<>(); for (var comp : comps) { - data.add(new Pair<>(comp.first, extractValue(comp.second))); + data.put(comp.name, extractValue(comp.element)); } var error = validate.apply(data); if (error != null) { @@ -104,11 +104,21 @@ public FormDialog(JDialog owner, String title, List> co setVisible(true); } + /** + * An input element with a name to show in the form dialog. + * The element has to be a {@link JTextArea} or {@link JTextField}! + * + * @param name the name + * @param element the element + */ + public record NamedInputElement(String name, JComponent element) { + } + private static String extractValue(JComponent comp) { - if (comp instanceof JTextArea) { - return ((JTextArea) comp).getText(); - } else if (comp instanceof JTextField) { - return ((JTextField) comp).getText(); + if (comp instanceof JTextArea textArea) { + return textArea.getText(); + } else if (comp instanceof JTextField textField) { + return textField.getText(); } else { throw new IllegalStateException("FormDialog used with incorrect component"); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java b/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java deleted file mode 100644 index 9076ff94228..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java +++ /dev/null @@ -1,39 +0,0 @@ -/* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2 - * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.proof.reference; - -import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Visitor; -import de.uka.ilkd.key.logic.op.ProgramMethod; - -public class ProgramMethodFinder implements Visitor { - - private boolean foundProgramMethod = false; - - @Override - public boolean visitSubtree(Term visited) { - return false; - } - - @Override - public void visit(Term visited) { - if (visited.op() instanceof ProgramMethod) { - foundProgramMethod = true; - } - } - - @Override - public void subtreeEntered(Term subtreeRoot) { - - } - - @Override - public void subtreeLeft(Term subtreeRoot) { - - } - - public boolean getFoundProgramMethod() { - return foundProgramMethod; - } -} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java index baed14cc380..1f78a2580e6 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java @@ -16,8 +16,6 @@ import de.uka.ilkd.key.logic.PosInTerm; import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.op.Function; -import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.proof.BranchLocation; import de.uka.ilkd.key.proof.FunctionTracker; import de.uka.ilkd.key.proof.Goal; @@ -39,6 +37,7 @@ import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.rule.inst.InstantiationEntry; +import org.key_project.logic.op.Function; import org.key_project.slicing.analysis.AnalysisResults; import org.key_project.slicing.analysis.DependencyAnalyzer; import org.key_project.slicing.graph.AddedRule; @@ -183,12 +182,11 @@ private List> inputsOfNode(Node n, Set var x = it.next(); InstantiationEntry y = x.value(); Object z = y.getInstantiation(); - if (z instanceof Term) { - z = ((Term) z).op(); + if (z instanceof Term term) { + z = term.op(); } - if (z instanceof Function) { + if (z instanceof Function finalZ) { // skip if z is contained in any of the other inputs - Operator finalZ = (Function) z; if (input.stream().anyMatch(form -> { var graphNode = form.first; if (graphNode instanceof TrackedFormula tf) { @@ -204,7 +202,7 @@ private List> inputsOfNode(Node n, Set var a = FunctionTracker.getIntroducedBy(((Function) z)); if (a != null && a != n) { input.add(new Pair<>( - graph.getFunctionNode((Function) z, a.getBranchLocation()), false)); + graph.getFunctionNode(finalZ, a.getBranchLocation()), false)); } } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java index ec032d20e32..50eb418fbf9 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java @@ -7,25 +7,29 @@ import java.util.HashMap; import java.util.List; import java.util.Map; -import java.util.Properties; import de.uka.ilkd.key.settings.AbstractPropertiesSettings; +import de.uka.ilkd.key.settings.Configuration; public class ProofRegroupSettings extends AbstractPropertiesSettings { - private static final String PREFIX = "[ProofRegrouping]Group"; + private static final String CATEGORY = "ProofRegrouping"; private static final List DEFAULT_GROUPS = List.of("Propositional expansion", "Negation/conjunctive normal form", "Polynomial/inequation normal form", "Simplification"); private final List> groups = new ArrayList<>(); + public ProofRegroupSettings() { + super(CATEGORY); + } + @Override - public void readSettings(Properties props) { - for (var key : props.keySet()) { - var k = (String) key; - var v = props.get(k); - if (k.startsWith(PREFIX)) { - var groupName = k.substring(PREFIX.length()); - var prop = createStringProperty(PREFIX + groupName, ""); + public void readSettings(Configuration configuration) { + var cat = configuration.getSection(category); + if (cat != null) { + for (var entry : cat.getEntries()) { + var groupName = entry.getKey(); + var v = entry.getValue(); + var prop = createStringProperty(groupName, ""); prop.set((String) v); groups.add(prop); } @@ -50,12 +54,12 @@ public void readSettings(Properties props) { } public void addGroup(String name, List ruleSets) { - groups.add(createStringProperty(PREFIX + name, String.join(",", ruleSets))); + groups.add(createStringProperty(name, String.join(",", ruleSets))); } public void updateGroup(String name, List ruleSets) { for (var prop : groups) { - if (prop.getKey().equals(PREFIX + name)) { + if (prop.getKey().equals(name)) { prop.set(String.join(",", ruleSets)); } } @@ -64,7 +68,7 @@ public void updateGroup(String name, List ruleSets) { public Map> getGroups() { Map> m = new HashMap<>(); for (var pe : groups) { - var name = pe.getKey().substring(PREFIX.length()); + var name = pe.getKey(); m.put(name, List.of(pe.get().split(","))); } return m; @@ -73,7 +77,7 @@ public Map> getGroups() { public Map> getUserGroups() { Map> m = new HashMap<>(); for (var pe : groups) { - var name = pe.getKey().substring(PREFIX.length()); + var name = pe.getKey(); if (DEFAULT_GROUPS.contains(name)) { continue; } @@ -85,13 +89,12 @@ public Map> getUserGroups() { public void removeGroup(String name) { PropertyEntry toRemove = null; for (var pe : groups) { - if (pe.getKey().substring(PREFIX.length()).equals(name)) { + if (pe.getKey().equals(name)) { toRemove = pe; break; } } groups.remove(toRemove); propertyEntries.remove(toRemove); - properties.remove(toRemove); } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java index 091e5b9112d..3209c2a98ca 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java @@ -13,7 +13,8 @@ import de.uka.ilkd.key.gui.settings.SettingsProvider; import de.uka.ilkd.key.gui.utilities.FormDialog; import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.util.Pair; + +import org.key_project.util.collection.Pair; import net.miginfocom.layout.CC; import org.slf4j.Logger; @@ -64,12 +65,12 @@ public static ProofRegroupSettings getSettings() { } @Override - public JComponent getPanel(MainWindow window) { + public JPanel getPanel(MainWindow window) { return getPanel(window, null); } @Override - public JComponent getPanel(MainWindow window, JDialog dialog) { + public JPanel getPanel(MainWindow window, JDialog dialog) { ProofRegroupSettings ss = getSettings(); pCenter.removeAll(); @@ -99,18 +100,18 @@ private void setupAddAndRemoveButtons(JDialog dialog, ProofRegroupSettings ss) { addNew.addActionListener(e -> { try { new FormDialog(dialog, "Add new group", - List.of(new Pair<>("Name", new JTextField()), - new Pair<>("Heuristics", new JTextArea())), + List.of(new FormDialog.NamedInputElement("Name", new JTextField()), + new FormDialog.NamedInputElement("Heuristics", new JTextArea())), data -> { - var name = data.get(0).second; + var name = data.get("Name"); if (ss.getGroups().containsKey(name)) { return "Group name already in use!"; } return null; }, data -> { - var name = data.get(0).second; - var content = data.get(1).second; + var name = data.get("Name"); + var content = data.get("Heuristics"); var ta = addTextArea(name, "", null, emptyValidator()); ta.setText(content); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java index 2a0edac4327..2bc52cda589 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -20,7 +20,6 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.proof.io.*; -import de.uka.ilkd.key.util.Pair; import org.key_project.slicing.graph.AnnotatedEdge; import org.key_project.slicing.graph.DependencyGraph; @@ -47,12 +46,12 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) Set done = new HashSet<>(); - Deque> todo = new ArrayDeque<>(); - todo.add(new Pair<>(BranchLocation.ROOT, proof.root())); + Deque todo = new ArrayDeque<>(); + todo.add(new BranchTodo(BranchLocation.ROOT, proof.root())); while (!todo.isEmpty()) { var t = todo.pop(); - var loc = t.first; - var root = t.second; + var loc = t.location; + var root = t.rootNode; if (done.contains(loc)) { continue; } @@ -142,7 +141,8 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) var c = last.childrenCount(); c--; while (c >= 0) { - todo.addFirst(new Pair<>(last.child(c).getBranchLocation(), last.child(c))); + todo.addFirst( + new BranchTodo(last.child(c).getBranchLocation(), last.child(c))); c--; } newOrder.add(last); @@ -157,7 +157,7 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) ProblemLoaderControl control = new DefaultUserInterfaceControl(); Path tmpFile = Files.createTempFile("proof", ".proof"); - proof.saveProofObligationToFile(tmpFile.toFile()); + ProofSaver.saveProofObligationToFile(tmpFile.toFile(), proof); String bootClassPath = proof.getEnv().getJavaModel().getBootClassPath(); AbstractProblemLoader problemLoader = new SingleThreadProblemLoader( @@ -172,7 +172,7 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) // Files.delete(tmpFile); Proof newProof = problemLoader.getProof(); new ReorderingReplayer(proof, newProof, steps).copy(); - newProof.saveToFile(tmpFile.toFile()); + ProofSaver.saveToFile(tmpFile.toFile(), newProof); KeYMediator mediator = MainWindow.getInstance().getMediator(); mediator.startInterface(true); @@ -182,4 +182,7 @@ public static void reorderProof(Proof proof, DependencyGraph depGraph) problemLoader2.setIgnoreWarnings(true); problemLoader2.runAsynchronously(); } + + private record BranchTodo(BranchLocation location, Node rootNode) { + } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java index e03948869ff..a884a6f6bc1 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java @@ -8,13 +8,13 @@ import java.util.stream.StreamSupport; import de.uka.ilkd.key.logic.PosInOccurrence; -import de.uka.ilkd.key.logic.op.Function; import de.uka.ilkd.key.proof.BranchLocation; import de.uka.ilkd.key.proof.FunctionTracker; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.util.Triple; +import org.key_project.logic.op.Function; import org.key_project.slicing.DependencyNodeData; import org.key_project.slicing.DependencyTracker; import org.key_project.util.EqualsModProofIrrelevancy; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java index 9aedb130a7a..2cfaadc34ec 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java @@ -5,9 +5,10 @@ import java.util.Objects; -import de.uka.ilkd.key.logic.op.Function; import de.uka.ilkd.key.proof.BranchLocation; +import org.key_project.logic.op.Function; + /** * A skolem constant tracked in the dependency graph. * diff --git a/keyext.slicing/src/test/java/org/key_project/slicing/FunctionTrackerTest.java b/keyext.slicing/src/test/java/org/key_project/slicing/FunctionTrackerTest.java new file mode 100644 index 00000000000..3e329adb59f --- /dev/null +++ b/keyext.slicing/src/test/java/org/key_project/slicing/FunctionTrackerTest.java @@ -0,0 +1,34 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.slicing; + +import java.io.File; +import java.util.Collection; + +import de.uka.ilkd.key.control.KeYEnvironment; + +import org.key_project.slicing.graph.AnnotatedEdge; +import org.key_project.slicing.graph.TrackedFunction; +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +public class FunctionTrackerTest { + public static final File TEST_CASES_DIRECTORY = FindResources.getTestCasesDirectory(); + + @Test + void tracksSkolemConstantCorrectly() throws Exception { + var file = new File(TEST_CASES_DIRECTORY, "testFunctionTracker.proof"); + var env = KeYEnvironment.load(file); + var proof = env.getLoadedProof(); + var tracker = new DependencyTracker(proof); + var depGraph = tracker.getDependencyGraph(); + Collection edges = depGraph.edgesOf(proof.findAny(x -> x.serialNr() == 4)); + assertEquals(2, edges.size()); + var edge = edges.stream().findFirst().get(); + assertInstanceOf(TrackedFunction.class, edge.getSource()); + } +} diff --git a/keyext.slicing/src/test/resources/testcase/testFunctionTracker.proof b/keyext.slicing/src/test/resources/testcase/testFunctionTracker.proof new file mode 100644 index 00000000000..70ce899f1e8 --- /dev/null +++ b/keyext.slicing/src/test/resources/testcase/testFunctionTracker.proof @@ -0,0 +1,143 @@ +\profile "Java Profile"; + +\settings // Proof-Settings-Config-File +{ + "Choice" : { + "JavaCard" : "JavaCard:off", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "floatRules" : "floatRules:assumeStrictfp", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "wdChecks" : "wdChecks:off", + "wdOperator" : "wdOperator:L" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "JavaCardDLStrategy", + "MaximumNumberOfAutomaticApplications" : 7000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED", + "DEP_OPTIONS_KEY" : "DEP_ON", + "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_ON", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } + } + +\functions { + int b; +} +\problem { + \exists int c; (c = Z(5(#)) & lt(c, b)) + & \exists int c; (c = Z(7(#)) & gt(c, b)) + & \exists int c; c = Z(0(#)) +-> b = Z(6(#)) +} + +\proof { +(keyLog "0" (keyUser "arne" ) (keyVersion "bd6f1082c56a8177268809c89ccd4d7a7a8628d2")) + +(autoModeTime "78") + +(branch "dummy ID" +(rule "impRight" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "exLeft" (formula "3") (inst "sk=c_0") (userinteraction)) +(rule "sign_case_distinction" (inst "signCasesLeft=c_0") (userinteraction)) +(branch "c_0 is negative" + (rule "applyEqRigid" (formula "1") (term "0") (ifseqformula "4") (userinteraction)) + (rule "leq_literals" (formula "1") (userinteraction)) + (rule "closeFalse" (formula "1") (userinteraction)) +) +(branch "c_0 is zero" + (rule "exLeft" (formula "1") (inst "sk=c_1")) + (rule "andLeft" (formula "1")) + (rule "exLeft" (formula "3") (inst "sk=c_2")) + (rule "andLeft" (formula "3")) + (rule "inEqSimp_ltToLeq" (formula "2")) + (rule "polySimp_mulComm0" (formula "2") (term "1,0,0")) + (rule "inEqSimp_gtToGeq" (formula "4")) + (rule "polySimp_mulComm0" (formula "4") (term "1,0,0")) + (rule "applyEqRigid" (formula "2") (term "1,0") (ifseqformula "1")) + (rule "polySimp_addComm1" (formula "2") (term "0")) + (rule "add_literals" (formula "2") (term "0,0")) + (rule "applyEq" (formula "4") (term "1,0") (ifseqformula "3")) + (rule "polySimp_addComm1" (formula "4") (term "0")) + (rule "add_literals" (formula "4") (term "0,0")) + (rule "inEqSimp_sepNegMonomial0" (formula "2")) + (rule "polySimp_mulLiterals" (formula "2") (term "0")) + (rule "polySimp_elimOne" (formula "2") (term "0")) + (rule "inEqSimp_sepNegMonomial1" (formula "4")) + (rule "polySimp_mulLiterals" (formula "4") (term "0")) + (rule "polySimp_elimOne" (formula "4") (term "0")) + (rule "inEqSimp_strengthen0" (formula "4") (ifseqformula "6")) + (rule "add_literals" (formula "4") (term "1")) + (rule "inEqSimp_contradEq3" (formula "6") (ifseqformula "4")) + (rule "mul_literals" (formula "6") (term "1,0,0")) + (rule "add_literals" (formula "6") (term "0,0")) + (rule "qeq_literals" (formula "6") (term "0")) + (builtin "One Step Simplification" (formula "6")) + (rule "false_right" (formula "6")) + (rule "inEqSimp_contradInEq1" (formula "4") (ifseqformula "2")) + (rule "qeq_literals" (formula "4") (term "0")) + (builtin "One Step Simplification" (formula "4")) + (rule "closeFalse" (formula "4")) +) +(branch "c_0 is positive" + (rule "applyEqRigid" (formula "1") (term "0") (ifseqformula "4") (userinteraction)) + (rule "qeq_literals" (formula "1") (userinteraction)) + (rule "closeFalse" (formula "1") (userinteraction)) +) +) +}