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.