RuleCommand can now deal with rules that have schema variables for logical variables

mattulbrich commented 1 month ago

Rules in script could not be applied if there were free logical variable schema variables around.

This is the case for class invariant rules and others.

The commit fixes the issue by copying code from how it is done for interactive rule applications.

Intended Change

More rules can be applied.

Type of pull request

Bug fix (non-breaking change which fixes an issue)
Refactoring (behaviour should not change or only minimally change)
There are changes to the (Java) code

Ensuring quality

I have tested the feature as follows: FM case study

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

codecov[bot] commented 1 month ago

Codecov Report

Attention: Patch coverage is 11.11111% with 8 lines in your changes missing coverage. Please review.

Project coverage is 38.03%. Comparing base (345c9c6) to head (1b48b9e). Report is 53 commits behind head on main.

Files	Patch %	Lines
...va/de/uka/ilkd/key/macros/scripts/RuleCommand.java	11.11%	6 Missing and 2 partials :warning:

Additional details and impacted files

```diff @@ Coverage Diff @@ ## main #3482 +/- ## ========================================= Coverage 38.03% 38.03% - Complexity 17084 17089 +5 ========================================= Files 2099 2099 Lines 127194 127274 +80 Branches 21368 21386 +18 ========================================= + Hits 48375 48409 +34 - Misses 72856 72892 +36 - Partials 5963 5973 +10 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

mattulbrich commented 4 weeks ago

This PR is relevant for the FM tutorial.

@Drodt @WolframPfeifer @flo2702 @wadoon

KeYProject / key