Automatically abbreviate anon heap names

[FliegendeWurst]

By automatically abbreviating heap names, it is much easier to navigate and inspect the sequent view. The screenshots below show the same proof node. Discussion points: Should this option be automatically enabled? Is the naming scheme (heap_loop_X) fine?

Previously (300k characters)	Now (35k characters, 8.5x shorter!)

Heap names after method calls don't need to be abbreviated, they are already just referred to by "heapAfter_commonEntry" or similar.

This PR builds on top of #3251 and #3258. Only the last five commits in this branch are relevant.

[codecov]

Codecov Report

Merging #3268 (64f2358) into main (6c808a3) will decrease coverage by 0.01%.
The diff coverage is 0.00%.

@@             Coverage Diff              @@
##               main    #3268      +/-   ##
============================================
- Coverage     37.74%   37.74%   -0.01%     
  Complexity    16851    16851              
============================================
  Files          2052     2052              
  Lines        125687   125688       +1     
  Branches      21234    21234              
============================================
  Hits          47436    47436              
- Misses        72408    72409       +1     
  Partials       5843     5843              

Files Changed	Coverage Δ
...e/uka/ilkd/key/rule/AbstractLoopInvariantRule.java	5.78% <0.00%> (-0.04%)	⬇️

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

📢 Have feedback on the report? Share it here.

[github-actions]

Thank you for your contribution.

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

[mattulbrich]

A rather more general question: Why use abbreviations and not (Skolem) constants which would not only simplify things on the visual surface. For method calls, a fresh heap constants seems to be introduced for every call, could the same not be done for loops too. (The automation has afaik already been optimised for reoccurrences of the same heap symbol) ... Perhaps we should discuss this in person.

[mattulbrich]

A few remarks from our discussion:

• Insider knowledge: Arrays are best created in a separate method; this clutters the heap considerably less.
• Probably there could and should be a "contract-like rule" for array creation as well, which does not go through all stages of object creation.
• For method invocations, there is a new heap symbol, same could be incorporated into the scoped loop rule, the result would be something like loopHeap_17 = anon(.....) ==> {heap := loopHeap || ...} [...]...
• create(heap,o) could already set all fields to their default value, so no need for this stage of the initialisation (/cc @weigl for the new infrastructure?) We could get rid of memset, too.

[WolframPfeifer]

We decided that the solution with abbreviations is not what we want to have, thus I close this PR now.