Arne Keller
Arne Keller
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...
## Description Automated proof search, replaceKnown accounts for 43% of *all* CPU time: (the view below is zoomed in) ![image](https://github.com/KeYProject/key/assets/12560461/4e4172fa-d47d-4ad4-84a7-28c85fe2bc44) As far as I can tell, almost no replace_known_left /...
## Description Loading a proof with origin tracking enabled can take up to 20% more time. ## Reproducible Depends on the proof, I guess. ### Steps to reproduce 1. Enable...
Tracking issue for *all* font scaling bugs. ## Description Changing the global font factor produces some weird artifacts. - [ ] Icon size does not adapt - [ ] Settings...
## Description As far as I can tell, it is not possible to express `int::seqGet` in a specification. `(int) \dl_seqGet` (or `(int)s[i]`) results in a moduloInt: ![Screenshot_20230823_145115](https://github.com/KeYProject/key/assets/12560461/7ee62328-cbc8-4e33-9eac-1b20e87ce721) I have implemented...
## Description When searching in a large sequent, a StackOverflowError is printed to stderr. ``` Exception in thread "AWT-EventQueue-0" java.lang.StackOverflowError at java.base/java.util.regex.Pattern$Slice.match(Pattern.java:4088) at java.base/java.util.regex.Pattern$BmpCharPropertyGreedy.match(Pattern.java:4329) at java.base/java.util.regex.Pattern$Slice.match(Pattern.java:4088) at java.base/java.util.regex.Pattern$BmpCharPropertyGreedy.match(Pattern.java:4329) at java.base/java.util.regex.Pattern$Slice.match(Pattern.java:4088)...