Skip to content

Fix wellFormedEQ* taclets and some improvements for large heaps#3945

Open
unp1 wants to merge 2 commits into
mainfrom
bubel/pullout_heap_stores
Open

Fix wellFormedEQ* taclets and some improvements for large heaps#3945
unp1 wants to merge 2 commits into
mainfrom
bubel/pullout_heap_stores

Conversation

@unp1

@unp1 unp1 commented Jul 26, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

Intended Change

  1. Fixes some wellFormedEQ* taclets that got out of sync with their counterpart
    • I would suggest we add a taclet flag \generateEQ that automatically greates the EQ version, which would allow us to keep the rule files smaller and to avoid these rules getting out of sync (this is not done in this PR)
  2. Improves reasoning with large heaps in updates (e.g. as extreme example: heap_array_400 in examples/performance-test/updateSimplification)

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)
  • New feature (non-breaking change which adds functionality)
  • Breaking change (fix or feature that would cause existing functionality to change): the rule fixes might break some saved proofs
  • There are changes to the taclet rule base

Ensuring quality

  • I made sure that introduced/changed code is well documented (javadoc and inline comments).
  • I have tested the feature as follows: added additional proofs to runAllProofs and checked that no existing problem deteriorates
  • I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@unp1 unp1 self-assigned this Jul 26, 2026
@unp1 unp1 added the Calculus label Jul 26, 2026
@unp1
Fixes some wellFormedEQ rules and improves reasoning about large heaps
4181117 
* some wellFormedEQ rules got out of sync with their counterparts
* pullout large heaps from updates to speed up reasoning
  (extreme example heap_array_200/400 :-)
@unp1
unp1 force-pushed the bubel/pullout_heap_stores branch from dae2316 to 0a41874 Compare July 26, 2026 10:15
@unp1
Make strategy option visible to user
93020ff 
- we need a different way to configure our strategy
  Certain details only in Settings, maybe have the startegy pane be user configurable...
@unp1
unp1 force-pushed the bubel/pullout_heap_stores branch from 0a41874 to 93020ff Compare July 26, 2026 11:48
@unp1
unp1 enabled auto-merge July 26, 2026 11:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@unp1 unp1

Labels

Calculus

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@unp1