Proof slicing extension

[FliegendeWurst]

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.

[WolframPfeifer]

I finally completed the review, it was quite a lot of code (> 10,000 LOC)!

The slicing extension is very well crafted in my opinion and a great addition to KeY. As we know from the evaluation in the Bachelor's thesis, slicing proofs often greatly reduces their size. Also, the code is very well documented (JavaDoc, internal comments, and a page in key-docs). Thanks for that!

I have a few minor requests for change. Could you please address them?

Finally, I noticed that some examples such as SumAndMax and BinarySearch can not be proven "as automatically" as with earlier KeY releases. Pressing the green button or running Full Auto Pilot alone is not sufficient (needs another "Try Close" afterward). However, this is already the case in the main branch currently and thus not your fault.

[mattulbrich]

Thanks indeed.

Finally, I noticed that some examples such as SumAndMax and BinarySearch can not be proven "as automatically" as with earlier KeY releases. Pressing the green button or running Full Auto Pilot alone is not sufficient (needs another "Try Close" afterward). However, this is already the case in the main branch currently and thus not your fault.

How did that happen? 😲 We have so man quality measures in place and yet the most prominent example does not work anymore?

[FliegendeWurst]

I have adressed all review comments.

[WolframPfeifer]

Everything is fine now, thanks!