Improve heap simplification

[unp1]

Intended Change

Improve performance of heap simplifications.

Motivation: Current work on symbolic execution of larger programs revealed some slow-down due to heap simplificaton.

This PR wins for a heap heavy program of
400 code lines: 8 % of time (18s -> 16s)
800 lines: 30 % (50s -> 35s)
1000 lines: 40% (72s -> 44s)

• Main contibutor: Additional heap simplification rules
• Medium: more efficient drop effectless store (hidden quadratic grow in larger proofs)
• Minor: Cache context instantiation in SVInstantiation (hidden quadratic grow (due to immutableMap being just a simpel list also small list))

Plan

• Add correctness proofs for new taclets

Type of pull request

• Refactoring (behaviour should not change or only minimally change)
• There are changes to the (Java) code
• There are changes to the taclet rule base

Ensuring quality

• I added new test case(s) for new functionality:
• I have tested the feature as follows: Several runs of runAll*Proofs (closes same amount of proofs)
• I have checked that runtime performance has not deteriorated: it has improved for heap heavy proofs

Additional information and contact(s)

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