Proof slicing extension (#3026)

Continuation of
https://git.key-project.org/key/key/-/merge_requests/596. All review
comments have been adressed.
______________________

This branch introduces the proof analysis and slicing algorithms
implemented for my bachelor's thesis for inclusion in the next KeY
version.

# Why?

Neat data structure (dependency graph) and algorithm that help many
usecases: "optimizing" the loading time of finished proofs,
investigating the efficiency of KeY's heuristics, reducing the size of
incomplete proofs, ...

Also see https://git.key-project.org/key/key-docs/-/merge_requests/7

# Features and Impact

Many new features available in the GUI: inspecting the dependency graph
of a proof, proof analysis, proof slicing, ...

The build script has been changed to save the full git commit hash as
KeY version.

## Changes in key.core

- new `EqualsModProofIrrelevancy` interface to ignore certain details
when comparing objects across proofs (currently only origin labels)
- `Node`: `stepIndex` and `branchLocation`
- `BranchLocation` class to represent a location in the proof tree
- `KeYMediator`: `fireProofLoaded` event (called just before a loaded
proof is replayed)
- `ProofSaver`: option to only save the proof obligation
- `OneStepSimplifier`: when reloading a proof, restrict the formulas
available to the Simplifier to the previously used formulas
- `Taclet`: `addedBy` field to indicate which proof step defined a
taclet
- `ModularSMTLib2Translator`, `SMTFocusResults`: new facilities to ask
the SMT solver for an unsat core and hide formulas not present in the
unsat core from the sequent

## Changes in key.util
- `Graph`, `DirectedGraph`, `GraphEdge`, `DefaultEdge`: simple
implementation of a directed graph

# Review

The most "interesting" class to review is probably SlicingProofReplayer,
since some parts of it are very similar to the
IntermediateProofReplayer.

# Persons involved

Commit c9f59aeba25cde9f9db4fc608e99f235575377bc by Mattias Ulbrich
(experiments with SMT unsat cores) is included in this branch. It was
only intended as a "temporary hack", but it proved to be quite useful
and has been adapted slightly to handle SMT solvers that do not produce
unsat cores.
________________________

Comment edited by @WolframPfeifer: Attached the original description.

.gitignore

@@ -60,7 +60,7 @@ key.core/src/main/gen
 key.core/src/main/resources/de/uka/ilkd/key/smt/newsmt2/DefinedSymbolsHandler.preamble.xml
 
 # this file is automatically generated by gradle task :key.core:generateSolverPropsList
-key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes
+key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/solvers.txt
 
 key/key.ui/examples/**/**.proof
 **/testresults/**

key.core/build.gradle

@@ -173,7 +173,7 @@ task generateVersionFiles() {
 
     outputs.files sha1, branch, versionf
 
-    def gitRevision = gitRevParse('--short HEAD')
+    def gitRevision = gitRevParse('HEAD')
     def gitBranch = gitRevParse('--abbrev-ref HEAD')
 
     doLast {

key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java

@@ -4,12 +4,14 @@
 import java.util.LinkedList;
 import java.util.List;
 import java.util.Properties;
+import java.util.function.Consumer;
 import java.util.logging.Logger;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.macros.ProofMacroFinishedInfo;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.ProofAggregate;
+import de.uka.ilkd.key.proof.RuleAppListener;
 import de.uka.ilkd.key.proof.init.IPersistablePO.LoadedPOContainer;
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.ProblemInitializer;
@@ -201,12 +203,17 @@ public void taskFinished(TaskFinishedInfo info) {
     @Override
     public AbstractProblemLoader load(Profile profile, File file, List<File> classPath,
             File bootClassPath, List<File> includes, Properties poPropertiesToForce,
-            boolean forceNewProfileOfNewProofs) throws ProblemLoaderException {
+            boolean forceNewProfileOfNewProofs,
+            Consumer<Proof> callback) throws ProblemLoaderException {
         AbstractProblemLoader loader = null;
         try {
             loader = new SingleThreadProblemLoader(file, classPath, bootClassPath, includes,
                 profile, forceNewProfileOfNewProofs, this, false, poPropertiesToForce);
-            loader.load();
+            if (callback != null) {
+                loader.load(callback);
+            } else {
+                loader.load();
+            }
             return loader;
         } catch (ProblemLoaderException e) {
             if (loader != null && loader.getProof() != null) {

key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java

@@ -3,11 +3,13 @@
 import java.io.File;
 import java.util.List;
 import java.util.Properties;
+import java.util.function.Consumer;
 
 import de.uka.ilkd.key.java.JavaInfo;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.parser.Location;
 import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.RuleAppListener;
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.proof.init.ProofInputException;
@@ -247,9 +249,39 @@ public static KeYEnvironment<DefaultUserInterfaceControl> load(Profile profile,
             List<File> classPaths, File bootClassPath, List<File> includes,
             Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler,
             boolean forceNewProfileOfNewProofs) throws ProblemLoaderException {
+        return load(profile, location, classPaths, bootClassPath, includes, poPropertiesToForce,
+            ruleCompletionHandler,
+            null, forceNewProfileOfNewProofs);
+    }
+
+    /**
+     * Loads the given location and returns all required references as {@link KeYEnvironment}. The
+     * {@link MainWindow} is not involved in the whole process.
+     *
+     * @param profile The {@link Profile} to use.
+     * @param location The location to load.
+     * @param classPaths The class path entries to use.
+     * @param bootClassPath The boot class path to use.
+     * @param includes Optional includes to consider.
+     * @param poPropertiesToForce Some optional PO {@link Properties} to force.
+     * @param ruleCompletionHandler An optional {@link RuleCompletionHandler}.
+     * @param callbackProofLoaded An optional callback (called when the proof is loaded, before
+     *        replay)
+     * @param forceNewProfileOfNewProofs {@code} true
+     *        {@link AbstractProblemLoader#profileOfNewProofs} will be used as {@link Profile} of
+     *        new proofs, {@code false} {@link Profile} specified by problem file will be used for
+     *        new proofs.
+     * @return The {@link KeYEnvironment} which contains all references to the loaded location.
+     * @throws ProblemLoaderException Occurred Exception
+     */
+    public static KeYEnvironment<DefaultUserInterfaceControl> load(Profile profile, File location,
+            List<File> classPaths, File bootClassPath, List<File> includes,
+            Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler,
+            Consumer<Proof> callbackProofLoaded,
+            boolean forceNewProfileOfNewProofs) throws ProblemLoaderException {
         DefaultUserInterfaceControl ui = new DefaultUserInterfaceControl(ruleCompletionHandler);
         AbstractProblemLoader loader = ui.load(profile, location, classPaths, bootClassPath,
-            includes, poPropertiesToForce, forceNewProfileOfNewProofs);
+            includes, poPropertiesToForce, forceNewProfileOfNewProofs, callbackProofLoaded);
         InitConfig initConfig = loader.getInitConfig();
 
         return new KeYEnvironment<DefaultUserInterfaceControl>(ui, initConfig, loader.getProof(),

key.core/src/main/java/de/uka/ilkd/key/control/UserInterfaceControl.java

@@ -3,9 +3,11 @@
 import java.io.File;
 import java.util.List;
 import java.util.Properties;
+import java.util.function.Consumer;
 
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.ProofAggregate;
+import de.uka.ilkd.key.proof.RuleAppListener;
 import de.uka.ilkd.key.proof.init.AbstractProfile;
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.Profile;
@@ -19,7 +21,7 @@
  * Provides the user interface independent logic to manage multiple proofs. This includes:
  * <ul>
  * <li>Functionality to load files via {@link #load(Profile, File, List<File>, File, List<File>,
- * Properties, boolean)}.</li>
+ * Properties, boolean, Consumer<Proof>)}.</li>
  * <li>Functionality to instantiate new {@link Proof}s via
  * {@link #createProof(InitConfig, ProofOblInput)}.</li>
  * <li>Functionality to register existing {@link Proof}s in the user interface via
@@ -65,12 +67,14 @@ public interface UserInterfaceControl {
      *        {@link AbstractProblemLoader#profileOfNewProofs} will be used as {@link Profile} of
      *        new proofs, {@code false} {@link Profile} specified by problem file will be used for
      *        new proofs.
+     * @param callbackProofLoaded receives the proof after it is loaded, but before it is replayed
      * @return The opened {@link AbstractProblemLoader}.
      * @throws ProblemLoaderException Occurred Exception.
      */
     AbstractProblemLoader load(Profile profile, File file, List<File> classPaths,
             File bootClassPath, List<File> includes, Properties poPropertiesToForce,
-            boolean forceNewProfileOfNewProofs) throws ProblemLoaderException;
+            boolean forceNewProfileOfNewProofs,
+            Consumer<Proof> callbackProofLoaded) throws ProblemLoaderException;
 
     /**
      * Instantiates a new {@link Proof} in this {@link UserInterfaceControl} for the given

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

@@ -4,10 +4,11 @@
 import de.uka.ilkd.key.java.NameAbstractionTable;
 import de.uka.ilkd.key.pp.PrettyPrinter;
 import de.uka.ilkd.key.java.StatementBlock;
+import org.key_project.util.EqualsModProofIrrelevancy;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
-public class JavaBlock {
+public final class JavaBlock implements EqualsModProofIrrelevancy {
     private static final Logger LOGGER = LoggerFactory.getLogger(JavaBlock.class);
 
     /**
@@ -22,6 +23,7 @@ public class JavaBlock {
     public static final JavaBlock EMPTY_JAVABLOCK = new JavaBlock(new StatementBlock());
 
     private final JavaProgramElement prg;
+    private int hashCode = -1;
 
 
     /**
@@ -125,4 +127,27 @@ public String toString() {
         return printer.result();
     }
 
+    @Override
+    public boolean equalsModProofIrrelevancy(Object obj) {
+        if (!(obj instanceof JavaBlock)) {
+            return false;
+        }
+        if (this == obj) {
+            return true;
+        }
+        JavaBlock other = (JavaBlock) obj;
+        // quite inefficient, but sufficient
+        return toString().equals(other.toString());
+    }
+
+    @Override
+    public int hashCodeModProofIrrelevancy() {
+        if (hashCode == -1) {
+            hashCode = toString().hashCode();
+            if (hashCode == -1) {
+                hashCode = 0;
+            }
+        }
+        return hashCode;
+    }
 }

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

@@ -1,13 +1,14 @@
 package de.uka.ilkd.key.logic;
 
+import java.util.Objects;
+import java.util.stream.Collectors;
+
+import org.key_project.util.EqualsModProofIrrelevancy;
+import org.key_project.util.collection.ImmutableArray;
+import org.key_project.util.java.CollectionUtil;
 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 org.key_project.util.collection.ImmutableArray;
-import org.key_project.util.java.CollectionUtil;
-
-import java.util.Objects;
-import java.util.stream.Collectors;
 
 /**
  * The labeled term class is used for terms that have a label attached.
@@ -19,7 +20,7 @@
  * @see Term
  * @see TermImpl
  */
-class LabeledTermImpl extends TermImpl {
+class LabeledTermImpl extends TermImpl implements EqualsModProofIrrelevancy {
 
     /**
      * @see #getLabels()
@@ -111,6 +112,44 @@ public int computeHashCode() {
         return hash;
     }
 
+    @Override
+    public boolean equalsModProofIrrelevancy(Object o) {
+        if (!super.equalsModProofIrrelevancy(o)) {
+            return false;
+        }
+
+        if (o instanceof LabeledTermImpl) {
+            final LabeledTermImpl cmp = (LabeledTermImpl) o;
+            if (labels.size() == cmp.labels.size()) {
+                for (int i = 0, sz = labels.size(); i < sz; i++) {
+                    // skip irrelevant (origin) labels that differ for no real reason
+                    if (!labels.get(i).isProofRelevant()) {
+                        continue;
+                    }
+                    // this is not optimal, but as long as number of labels limited ok
+                    if (!cmp.labels.contains(labels.get(i))) {
+                        return false;
+                    }
+                }
+                return true;
+            }
+            return false;
+        } else {
+            return o.getClass() == TermImpl.class;
+        }
+    }
+
+    @Override
+    public int hashCodeModProofIrrelevancy() {
+        int hash = super.hashCodeModProofIrrelevancy();
+        for (int i = 0, sz = labels.size(); i < sz; i++) {
+            if (labels.get(i).isProofRelevant()) {
+                hash += 7 * labels.get(i).hashCode();
+            }
+        }
+        return hash;
+    }
+
     @Override
     public String toString() {
         StringBuilder result = new StringBuilder(super.toString());

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

@@ -27,10 +27,12 @@ private Semisequent() {
 
     /**
      * creates a new Semisequent with the Semisequent elements in seqList; the provided list must be
-     * redundance free, i.e., the created sequent must be exactly the same as when creating the
+     * redundancy free, i.e., the created sequent must be exactly the same as when creating the
      * sequent by subsequently inserting all formulas
+     *
+     * @param seqList list of sequent formulas
      */
-    Semisequent(ImmutableList<SequentFormula> seqList) {
+    public Semisequent(ImmutableList<SequentFormula> seqList) {
         assert !seqList.isEmpty();
         this.seqList = seqList;
     }

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

@@ -279,6 +279,13 @@ public int formulaNumberInSequent(boolean inAntec, SequentFormula cfma) {
             "Ghost formula " + cfma + " in sequent " + this + " [antec=" + inAntec + "]");
     }
 
+    /**
+     * Get a sequent formula by its position in the sequent.
+     * The first formula has number 1.
+     *
+     * @param formulaNumber formula number
+     * @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);

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

@@ -2,6 +2,7 @@
 
 import de.uka.ilkd.key.logic.op.AbstractTermTransformer;
 import de.uka.ilkd.key.logic.sort.Sort;
+import org.key_project.util.EqualsModProofIrrelevancy;
 
 
 /**
@@ -12,11 +13,18 @@
  * class by providing a way to add additional annotations or to cache local information about the
  * formula.
  */
-public class SequentFormula {
+public class SequentFormula implements EqualsModProofIrrelevancy {
 
     private final Term term;
 
+    /**
+     * Cached value for {@link #hashCode()}.
+     */
     private final int hashCode;
+    /**
+     * Cached value for {@link #hashCodeModProofIrrelevancy()}.
+     */
+    private final int hashCode2;
 
     /**
      * creates a new SequentFormula
@@ -29,6 +37,7 @@ public SequentFormula(Term term) {
         }
         this.term = term;
         this.hashCode = term.hashCode() * 13;
+        this.hashCode2 = term.hashCodeModProofIrrelevancy();
     }
 
     /** @return the stored Term */
@@ -56,4 +65,23 @@ public String toString() {
     public int hashCode() {
         return hashCode;
     }
+
+    @Override
+    public boolean equalsModProofIrrelevancy(Object obj) {
+        if (this == obj) {
+            return true;
+        }
+        if (obj instanceof SequentFormula) {
+            SequentFormula cmp = (SequentFormula) obj;
+            if (term.equalsModProofIrrelevancy(cmp.formula())) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    @Override
+    public int hashCodeModProofIrrelevancy() {
+        return hashCode2;
+    }
 }

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

@@ -1,6 +1,8 @@
 package de.uka.ilkd.key.logic;
 
 import javax.annotation.Nullable;
+
+import org.key_project.util.EqualsModProofIrrelevancy;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableSet;
 
@@ -33,7 +35,7 @@
  * Term supports the {@link Visitor} pattern. Two different visit strategies are currently
  * supported: {@link Term#execPostOrder(Visitor)} and {@link Term#execPreOrder(Visitor)}.
  */
-public interface Term extends SVSubstitute, Sorted {
+public interface Term extends SVSubstitute, Sorted, EqualsModProofIrrelevancy {
 
     /**
      * The top operator (e.g., in "A and B" this is "and", in f(x,y) it is "f").