Skip to content

Proof caching: use dependency graph to increase hit rate - #3305

Merged
WolframPfeifer merged 42 commits into
KeYProject:mainfrom
FliegendeWurst:caching-sliced
Feb 8, 2024
Merged

Proof caching: use dependency graph to increase hit rate#3305
WolframPfeifer merged 42 commits into
KeYProject:mainfrom
FliegendeWurst:caching-sliced

Conversation

@FliegendeWurst

@FliegendeWurst FliegendeWurst commented Oct 19, 2023

Copy link
Copy Markdown
Member

Previously when searching for a reference, the entire sequent of the old proof had to be present in the new proof.
Now, only the useful subset of the old sequent has to be present.
Tested by a unit test.

Additional functionality:

  • new "shortened chains" dependency graph rendering mode.
  • button in toolbar (and checkbox in options menu) to disable proof caching
  • new context menu action on nodes closed by cache to re-open them
  • when a referenced proof branch is pruned (= open again), any references to that branch are automatically removed (reopening previously "closed by cache" proofs)

@github-actions

github-actions Bot commented Oct 19, 2023

Copy link
Copy Markdown

Thank you for your contribution.

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

@FliegendeWurst FliegendeWurst self-assigned this Oct 20, 2023
Comment thread key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java
@FliegendeWurst FliegendeWurst added the keyext.slicing Module: keyext.slicing label Oct 26, 2023
@FliegendeWurst FliegendeWurst added the Feature New feature or request label Oct 30, 2023
@FliegendeWurst
FliegendeWurst marked this pull request as ready for review October 30, 2023 17:43
Comment thread key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java Outdated
@unp1
unp1 enabled auto-merge October 30, 2023 18:02
auto-merge was automatically disabled October 30, 2023 19:40

Head branch was pushed to by a user without write access

@codecov

codecov Bot commented Nov 2, 2023

Copy link
Copy Markdown

Codecov Report

Attention: 333 lines in your changes are missing coverage. Please review.

Comparison is base (603b2ca) 37.93% compared to head (82b0ac9) 37.72%.

Files Patch % Lines
...ava/org/key_project/slicing/graph/DotExporter.java 0.00% 41 Missing ⚠️
...org/key_project/slicing/graph/DependencyGraph.java 9.30% 39 Missing ⚠️
...ilkd/key/gui/plugins/caching/CachingExtension.java 0.00% 33 Missing ⚠️
.../gui/plugins/caching/actions/CloseByReference.java 0.00% 30 Missing ⚠️
...d/key/gui/plugins/caching/CachingPruneHandler.java 0.00% 26 Missing ⚠️
...ore/src/main/java/de/uka/ilkd/key/proof/Proof.java 0.00% 25 Missing ⚠️
...i/plugins/caching/actions/CloseAllByReference.java 0.00% 23 Missing ⚠️
...i/plugins/caching/actions/CopyReferencedProof.java 0.00% 20 Missing ⚠️
..._project/slicing/graph/AnnotatedShortenedEdge.java 0.00% 14 Missing ⚠️
...i/plugins/caching/toolbar/CachingToggleAction.java 0.00% 13 Missing ⚠️
... and 14 more
Additional details and impacted files
@@             Coverage Diff              @@
##               main    #3305      +/-   ##
============================================
- Coverage     37.93%   37.72%   -0.22%     
+ Complexity    17030    17017      -13     
============================================
  Files          2060     2076      +16     
  Lines        126300   126942     +642     
  Branches      21304    21378      +74     
============================================
- Hits          47913    47889      -24     
- Misses        72499    73156     +657     
- Partials       5888     5897       +9     

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

@WolframPfeifer WolframPfeifer left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for this improvement! As already discussed, for easier generation of a meaningful changelog, the PR title could be improved. I have only two small remarks/requests (see comments in code).

@WolframPfeifer WolframPfeifer added the Reviewer Feedback Feedback from the review needs to be addressed label Nov 3, 2023
@FliegendeWurst FliegendeWurst changed the title Proof caching: use dependency graph information Proof caching: use dependency graph information to increase hit rate Nov 4, 2023
@WolframPfeifer WolframPfeifer added Review Request Waiting for review and removed Reviewer Feedback Feedback from the review needs to be addressed labels Jan 25, 2024
@FliegendeWurst FliegendeWurst added the keyext.caching Module: keyext.caching label Feb 1, 2024

@WolframPfeifer WolframPfeifer left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for these nicely documented PR with convenience and efficiency features!

The only small suggestion from my side would be to remove the white box from the icon, such that it fits our icon design better.

@WolframPfeifer WolframPfeifer added Reviewer Feedback Feedback from the review needs to be addressed and removed Review Request Waiting for review labels Feb 6, 2024
@FliegendeWurst

Copy link
Copy Markdown
Member Author

The only small suggestion from my side would be to remove the white box from the icon, such that it fits our icon design better.

This is now done.

@WolframPfeifer
WolframPfeifer self-requested a review February 8, 2024 10:33
@WolframPfeifer
WolframPfeifer added this pull request to the merge queue Feb 8, 2024
Merged via the queue into KeYProject:main with commit 2182fa5 Feb 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Feature New feature or request keyext.caching Module: keyext.caching keyext.slicing Module: keyext.slicing Reviewer Feedback Feedback from the review needs to be addressed

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants