One Step Simplifier: optimizations (no new rules)

[FliegendeWurst]

This PR is an alternative to #3272, it only includes the optimizations. See the commits in this branch for details. Short description of each optimization:

• replaceKnown is called only on the changed sub-term, does not rescan entire term
• term replacement key hashcode uses depth() and op()
• cycle check switches to set implementation if >30 steps are done
• configurable cycle check and protocol (default: enabled, same as previous state)

Additionally, this PR fixes a bug with the construction of replaceKnown taclet apps inside the OSS. They were horribly broken before.

In the table below, I have benchmarked the optimizations on ShortestPath.java (Finish Symbolic Execution).

Description	Nodes	Rule apps	Time
Baseline	2568	10,521	18.8s
All optimizations	2581	10,537	16.2s (-13%)

The number of rule apps and nodes is different, but that's just because KeY's strategy is not deterministic.

More proofs (Benchmark: strategy)

Proof	Baseline	This PR
Binary Search	2.281s	2.312s
SITA	0.586s, 2.587s, 0.153s	0.588s, 2.556, 0.153s
SumAndMax	1.72s	1.83s
RemoveDup	0.649s, 0.208s, 6.221s	0.649s, 0.221s, 6.203s
Saddleback (no OSS)	42.0s	41.7s
Saddleback (OSS)	46.3s	46.4s

Overall: 0.1% faster.. the real value of these optimizations doesn't show up with the current rulesets

[codecov]

Codecov Report

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

Comparison is base (5b08998) 37.93% compared to head (1d1999a) 37.95%.

Files	Patch %	Lines
...n/java/de/uka/ilkd/key/rule/OneStepSimplifier.java	84.74%	1 Missing and 8 partials ⚠️
.../de/uka/ilkd/key/logic/label/TermLabelManager.java	0.00%	4 Missing ⚠️
...de/uka/ilkd/key/rule/OneStepSimplifierRuleApp.java	0.00%	3 Missing and 1 partial ⚠️
...e/src/main/java/de/uka/ilkd/key/java/Services.java	0.00%	1 Missing and 2 partials ⚠️
...in/java/de/uka/ilkd/key/logic/PosInOccurrence.java	0.00%	1 Missing ⚠️
...rc/main/java/de/uka/ilkd/key/proof/Statistics.java	85.71%	0 Missing and 1 partial ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3280      +/-   ##
============================================
+ Coverage     37.93%   37.95%   +0.01%     
- Complexity    17035    17050      +15     
============================================
  Files          2060     2060              
  Lines        126284   126340      +56     
  Branches      21303    21316      +13     
============================================
+ Hits          47912    47955      +43     
- Misses        72487    72491       +4     
- Partials       5885     5894       +9     

☔ View full report in Codecov by Sentry.
📢 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.

[WolframPfeifer]

For documentation: This PR needs some more evaluation (performance tests) after the latest changes.