One Step Simplifier: optimizations and new rules

[FliegendeWurst]

This PR fixes #3248 and supersedes #3256 and #3257 by optimizing the One Step Simplifier in several ways. See the commits in this branch for details.

Additionally, the following rules are added to a new oss ruleset included in the OSS:

• selectOfStore, selectOfCreate, selectOfAnon, selectOfMemset, selectCreatedOfAnon, dismissNonSelectedField
• elementOfUnion, elementOfArrayRange (elementOfSingleton and similar could also be useful)
• sortsDisjointModuloNull
• ifthenelse_negated
• castDel

This means that the One Step Simplifier can now simplify many heap terms in a single step. Previously this required many more proof nodes. For the file linked below, this additional ruleset is required (see #3248 (comment)). The ruleset is handled specially in the Simplifier so it will not be applied inside a Quantifier, seqDef Function or UpdateJunctor (essentially it should only simplify heap selects where every parameter is known).

See #3280 for benchmarks on the optimizations.

When adding the new rules, the OSS can do much more, but does not need much more time. Thanks to the optimization of the cycle check, its impact is not very high.

Description	Nodes	Rule apps	Time
with new rules	2229	98,473	33.5s
with new rules (no cycle check)	2229	98,473	32.0s

cc @WolframPfeifer @mattulbrich

[github-actions]

Thank you for your contribution.

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

[codecov]

Codecov Report

Merging #3272 (72ea1ba) into main (6c808a3) will increase coverage by 0.00%.
The diff coverage is 80.41%.

@@            Coverage Diff            @@
##               main    #3272   +/-   ##
=========================================
  Coverage     37.74%   37.74%           
- Complexity    16851    16867   +16     
=========================================
  Files          2052     2052           
  Lines        125687   125754   +67     
  Branches      21234    21254   +20     
=========================================
+ Hits          47436    47463   +27     
- Misses        72408    72432   +24     
- Partials       5843     5859   +16     

Files Changed	Coverage Δ
...e/src/main/java/de/uka/ilkd/key/java/Services.java	71.42% <0.00%> (-1.49%)	⬇️
...ain/java/de/uka/ilkd/key/logic/SequentFormula.java	72.72% <ø> (ø)
.../de/uka/ilkd/key/logic/label/TermLabelManager.java	81.76% <0.00%> (-0.67%)	⬇️
...de/uka/ilkd/key/rule/OneStepSimplifierRuleApp.java	69.23% <0.00%> (-30.77%)	⬇️
...rc/main/java/de/uka/ilkd/key/proof/Statistics.java	64.48% <85.71%> (+0.59%)	⬆️
...n/java/de/uka/ilkd/key/rule/OneStepSimplifier.java	83.63% <89.06%> (+0.53%)	⬆️
...in/java/de/uka/ilkd/key/logic/PosInOccurrence.java	85.29% <100.00%> (+0.21%)	⬆️
...src/main/java/de/uka/ilkd/key/logic/PosInTerm.java	78.98% <100.00%> (+7.55%)	⬆️
...va/de/uka/ilkd/key/macros/SMTPreparationMacro.java	22.22% <100.00%> (+9.72%)	⬆️
...in/java/de/uka/ilkd/key/nparser/ProofReplayer.java	89.47% <100.00%> (ø)

... and 12 files with indirect coverage changes

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

📢 Have feedback on the report? Share it here.