Proof Slicing: make dependency tracking optional (#3309)

Fixes #3301 by adding an option to disable the dependency tracker and
adding a way to create the dependency graph after the proof is done.

cc @unp1

Author: unp1

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

@@ -24,7 +24,7 @@
  */
 public class Sequent implements Iterable<SequentFormula> {
 
-    public static final Sequent EMPTY_SEQUENT = new NILSequent();
+    public static final Sequent EMPTY_SEQUENT = NILSequent.INSTANCE;
 
     /**
      * creates a new Sequent with empty succedent
@@ -184,6 +184,7 @@ public SequentChangeInfo addFormula(ImmutableList<SequentFormula> insertions,
      *         have been added or removed
      */
     public SequentChangeInfo replaceFormula(int formulaNr, SequentFormula replacement) {
+        checkFormulaIndex(formulaNr);
         formulaNr--;
         boolean inAntec = formulaNr < antecedent.size();
 
@@ -326,9 +327,7 @@ public int formulaNumberInSequent(PosInOccurrence pio) {
      * @return the sequent formula at that position
      */
     public SequentFormula getFormulabyNr(int formulaNumber) {
-        if (formulaNumber <= 0 || formulaNumber > size()) {
-            throw new RuntimeException("No formula nr. " + formulaNumber + " in seq. " + this);
-        }
+        checkFormulaIndex(formulaNumber);
         if (formulaNumber <= antecedent.size()) {
             return antecedent.get(formulaNumber - 1);
         }
@@ -357,7 +356,12 @@ public Iterator<SequentFormula> iterator() {
         return new SequentIterator(antecedent(), succedent());
     }
 
+    /**
+     * @param formulaNumber formula number (1-based)
+     * @return whether that formula is in the antecedent
+     */
     public boolean numberInAntec(int formulaNumber) {
+        checkFormulaIndex(formulaNumber);
         return formulaNumber <= antecedent.size();
     }
 
@@ -419,7 +423,11 @@ public boolean varIsBound(QuantifiableVariable v) {
         return false;
     }
 
-    static class NILSequent extends Sequent {
+    private static final class NILSequent extends Sequent {
+        private static final NILSequent INSTANCE = new NILSequent();
+
+        private NILSequent() {
+        }
 
         @Override
         public boolean isEmpty() {
@@ -530,4 +538,17 @@ public boolean contains(SequentFormula form) {
     public ImmutableList<SequentFormula> asList() {
         return antecedent.asList().append(succedent.asList());
     }
+
+    /**
+     * Check that the provided formula number is a 1-based index and in bounds.
+     * Throws an {@link IllegalArgumentException} otherwise.
+     *
+     * @param formulaNumber the formula number
+     */
+    private void checkFormulaIndex(int formulaNumber) {
+        if (formulaNumber <= 0 || formulaNumber > size()) {
+            throw new IllegalArgumentException(
+                "No formula nr. " + formulaNumber + " in seq. " + this);
+        }
+    }
 }

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

@@ -255,7 +255,7 @@ private void fireAutomaticStateChanged(boolean oldAutomatic, boolean newAutomati
     private void setNode(Node p_node) {
         if (node().sequent() != p_node.sequent()) {
             node = p_node;
-            resetTagManager();
+            tagManager = new FormulaTagManager(this);
         } else {
             node = p_node;
         }
@@ -458,18 +458,6 @@ public void clearAndDetachRuleAppIndex() {
         ruleAppIndex.clearAndDetachCache();
     }
 
-    // @Deprecated
-    // public void setProgramVariables(Namespace ns) {
-    // // final Iterator<Named> it=ns.elements().iterator();
-    // // ImmutableSet<ProgramVariable> s = DefaultImmutableSet.<ProgramVariable>nil();
-    // // while (it.hasNext()) {
-    // // s = s.add((ProgramVariable)it.next());
-    // // }
-    // // node().setGlobalProgVars(DefaultImmutableSet.<ProgramVariable>nil());
-    // // proof().getNamespaces().programVariables().set(s);
-    // // setGlobalProgVars(s);
-    // }
-
     public void addProgramVariable(ProgramVariable pv) {
         localNamespaces.programVariables().addSafely(pv);
     }
@@ -532,6 +520,7 @@ public void removeLastAppliedRuleApp() {
      * creates n new nodes as children of the referenced node and new n goals that have references
      * to these new nodes.
      *
+     * @param n number of goals to create
      * @return the list of new created goals.
      */
     @Nonnull
@@ -571,10 +560,6 @@ public ImmutableList<Goal> split(int n) {
         return goalList;
     }
 
-    private void resetTagManager() {
-        tagManager = new FormulaTagManager(this);
-    }
-
     public void setBranchLabel(String s) {
         node.getNodeInfo().setBranchLabel(s);
     }
@@ -600,14 +585,21 @@ private void resetLocalSymbols() {
         localNamespaces = newNS.copyWithParent();
     }
 
+    /**
+     * Perform the provided rule application on this goal.
+     * Returns the new goal(s), if any.
+     * This will also populate a {@link RuleAppInfo} object and fire the corresponding event.
+     * The state of the proof is also updated.
+     *
+     * @param ruleApp the rule app
+     * @return new goal(s)
+     */
     public ImmutableList<Goal> apply(final RuleApp ruleApp) {
-
         final Proof proof = proof();
 
         final NodeChangeJournal journal = new NodeChangeJournal(proof, this);
         addGoalListener(journal);
 
-
         final Node n = node;
 
         /*
@@ -630,19 +622,14 @@ public ImmutableList<Goal> apply(final RuleApp ruleApp) {
 
         proof.getServices().saveNameRecorder(n);
 
-        if (goalList != null) { // TODO: can goalList be null?
-            if (goalList.isEmpty()) {
-                proof.closeGoal(this);
-            } else {
-                proof.replace(this, goalList);
-                if (ruleApp instanceof TacletApp && ((TacletApp) ruleApp).taclet().closeGoal()) {
-                    // the first new goal is the one to be closed
-                    proof.closeGoal(goalList.head());
-                }
-                if (ruleApp instanceof SMTRuleApp) {
-                    // the first new goal is the one to be closed
-                    proof.closeGoal(goalList.head());
-                }
+        if (goalList.isEmpty()) {
+            proof.closeGoal(this);
+        } else {
+            proof.replace(this, goalList);
+            if (ruleApp instanceof TacletApp tacletApp && tacletApp.taclet().closeGoal()
+                    || ruleApp instanceof SMTRuleApp) {
+                // the first new goal is the one to be closed
+                proof.closeGoal(goalList.head());
             }
         }
 
@@ -680,6 +667,7 @@ private void adaptNamespacesNewGoals(final ImmutableList<Goal> goalList) {
         }
     }
 
+    @Override
     public String toString() {
         LogicPrinter lp = LogicPrinter.purePrinter(new NotationInfo(), proof().getServices());
         lp.printSequent(node.sequent());
@@ -711,9 +699,6 @@ public void makeLocalNamespacesFrom(NamespaceSet ns) {
         this.localNamespaces = ns.copyWithParent().copyWithParent();
     }
 
-    /**
-     *
-     */
     public List<RuleApp> getAllBuiltInRuleApps() {
         final BuiltInRuleAppIndex index = ruleAppIndex().builtInRuleAppIndex();
         LinkedList<RuleApp> ruleApps = new LinkedList<>();

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

@@ -456,6 +456,13 @@ public Iterator<Node> childrenIterator() {
         return new NodeIterator(children.iterator());
     }
 
+    /**
+     * @return the direct children of this node.
+     */
+    public Collection<Node> children() {
+        return Collections.unmodifiableList(children);
+    }
+
     /**
      * @return an iterator for all nodes in the subtree.
      */

key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java

@@ -86,7 +86,7 @@ public RuleJustification getRuleJustification() {
         }
     }
 
-    /** name of the taclet */
+    /** unique name of the taclet */
     private final Name name;
 
     /** name displayed by the pretty printer */

key.util/src/main/java/org/key_project/util/collection/IdentityHashSet.java

@@ -0,0 +1,113 @@
+/* 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.Collection;
+import java.util.IdentityHashMap;
+import java.util.Iterator;
+import java.util.Set;
+
+/**
+ * Hash set using the object's identity instead of their hashcode to determine uniqueness.
+ *
+ * @param <T> elmeent type
+ * @author Arne Keller
+ */
+public class IdentityHashSet<T> implements Set<T> {
+    /**
+     * Backing store.
+     */
+    private final IdentityHashMap<T, Object> innerMap = new IdentityHashMap<>();
+
+    /**
+     * Construct an empty set.
+     */
+    public IdentityHashSet() {
+
+    }
+
+    /**
+     * Copy provided elements into a new set.
+     *
+     * @param list elements to add
+     */
+    public IdentityHashSet(ImmutableList<T> list) {
+        list.forEach(this::add);
+    }
+
+    @Override
+    public int size() {
+        return innerMap.size();
+    }
+
+    @Override
+    public boolean isEmpty() {
+        return innerMap.isEmpty();
+    }
+
+    @Override
+    public boolean contains(Object o) {
+        return innerMap.containsKey(o);
+    }
+
+    @Override
+    public Iterator<T> iterator() {
+        return innerMap.keySet().iterator();
+    }
+
+    @Override
+    public Object[] toArray() {
+        return innerMap.keySet().toArray();
+    }
+
+    @Override
+    public <T1> T1[] toArray(T1[] a) {
+        return innerMap.keySet().toArray(a);
+    }
+
+    @Override
+    public boolean add(T o) {
+        return innerMap.put(o, o) == null;
+    }
+
+    @Override
+    public boolean remove(Object o) {
+        var contained = innerMap.containsKey(o);
+        innerMap.remove(o);
+        return contained;
+    }
+
+    @Override
+    public boolean addAll(Collection<? extends T> c) {
+        var changed = false;
+        for (T o : c) {
+            changed |= add(o);
+        }
+        return changed;
+    }
+
+    @Override
+    public void clear() {
+        innerMap.clear();
+    }
+
+    @Override
+    public boolean removeAll(Collection<?> c) {
+        var changed = false;
+        for (Object o : c) {
+            changed |= remove(o);
+        }
+        return changed;
+    }
+
+    @Override
+    public boolean retainAll(Collection<?> c) {
+        return innerMap.keySet().retainAll(c);
+    }
+
+    @Override
+    public boolean containsAll(Collection<?> c) {
+        return innerMap.keySet().containsAll(c);
+    }
+}