Only group rule apps on the same pos

Author: FliegendeWurst

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();
 

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();
+}

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

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

@@ -7,18 +7,21 @@
 
 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<List<String>> 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) {
+    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) {

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

@@ -198,7 +198,8 @@ public JToolBar getToolbar(MainWindow mainWindow) {
         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();
             }