Linearized symbolic execution in proof tree

[FliegendeWurst]

This PR adds a new option to the proof tree to "linearize symbolic execution".
This option changes the proof tree to be slightly more linear. In effect, the "Normal Execution" branch will (visually) continue on the parent branch. See the screenshots below for what the new view filter looks like.

previous	now

cut_direct applications are also linearized:

[codecov]

Codecov Report

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

Comparison is base (9634682) 37.94% compared to head (4f1acae) 37.91%.

Files	Patch %	Lines
...e/uka/ilkd/key/nparser/builder/TacletPBuilder.java	83.33%	1 Missing ⚠️
...lkd/key/rule/tacletbuilder/TacletGoalTemplate.java	75.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3237      +/-   ##
============================================
- Coverage     37.94%   37.91%   -0.03%     
+ Complexity    17036    17029       -7     
============================================
  Files          2060     2060              
  Lines        126284   126292       +8     
  Branches      21303    21304       +1     
============================================
- Hits          47914    47889      -25     
- Misses        72486    72517      +31     
- Partials       5884     5886       +2     

☔ 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.

[mattulbrich]

How is determined which is the "main" branch and which are the "side" branches. For a cut, e.g., both should be side branches. I like this option (we have done it like this in ivil and a bit in dive), and would favour to see it on the main branch.

[FliegendeWurst]

How is determined which is the "main" branch and which are the "side" branches.

Currently only the "Normal Execution [...]" branch is considered the main branch.

[FliegendeWurst]

The implementation has been updated to also consider e.g. the TRUE branch of cut_direct as the main branch:

This is achieved using a new goal template tagging mechanism.