Proof reordering (WIP)

[FliegendeWurst]

Experiment to logically group steps in proof.

Two main features:

• "Reorder" proof steps such that adjacent proof steps modify the same formula (no interweaving of two simplification chains)
• "Regroup" proof steps in the proof tree view (UI only)

TODOs

• Handle pruning correctly after regrouping
• Tests
• Documentation

The order of proof steps is determined as follows:

1. Steps with no inputs (no find / assumes)
2. Steps ordered by the dep. graph data
3. (optional) Step with no input that splits (e.g. sign_case_distinction)

To order the steps based on the dependency graph a queue of "available" graph nodes is managed. This queue is repeatedly iterated through to check for edges (steps) that are applicable. If they aren't the node is added to the end of the queue again. (More details will follow soon™)

[github-actions]

Thank you for your contribution.

The test artifacts are available on Artiweb.
The newest artifact is here.

[codecov]

Codecov Report

Attention: Patch coverage is 12.13675% with 514 lines in your changes are missing coverage. Please review.

Project coverage is 37.86%. Comparing base (9ad6cc8) to head (3107e20).

❗ Current head 3107e20 differs from pull request most recent head 7246b1e. Consider uploading reports for the commit 7246b1e to get more accurate results

Files	Patch %	Lines
...ain/java/org/key_project/slicing/ProofReorder.java	0.00%	98 Missing ⚠️
..._project/slicing/ProofRegroupSettingsProvider.java	0.00%	76 Missing ⚠️
...java/org/key_project/slicing/RegroupExtension.java	0.00%	61 Missing ⚠️
...ain/java/org/key_project/slicing/ProofRegroup.java	0.00%	58 Missing ⚠️
.../org/key_project/slicing/ProofRegroupSettings.java	0.00%	52 Missing ⚠️
...ava/org/key_project/slicing/graph/DotExporter.java	0.00%	29 Missing ⚠️
...va/org/key_project/slicing/ReorderingReplayer.java	0.00%	27 Missing ⚠️
...org/key_project/util/collection/ImmutableList.java	0.00%	24 Missing ⚠️
...ava/org/key_project/util/collection/GraphUtil.java	0.00%	18 Missing ⚠️
...core/src/main/java/de/uka/ilkd/key/proof/Node.java	21.05%	15 Missing ⚠️
... and 9 more

Additional details and impacted files

@@             Coverage Diff             @@
##               main    #3141     +/-   ##
===========================================
  Coverage     37.85%   37.86%             
+ Complexity    17042    16953     -89     
===========================================
  Files          2082     2063     -19     
  Lines        127290   126069   -1221     
  Branches      21441    21321    -120     
===========================================
- Hits          48183    47730    -453     
+ Misses        73194    72484    -710     
+ Partials       5913     5855     -58     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[WolframPfeifer]

The branch pfeifer/proofReorderingMainMerge contains my attempts to update the changes. I don't update the PR since it does not work at the moment, but I think there are only slight adaptations needed to fix it.

Something that already does not work on this PR without main merge: When trying to add a group in the settings, the dialog appears "behind" and input is blocked by the settings window, thus unusable. Probably, the parent of the dialog just needs to be set correctly.