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