Fix slicing bug related to Evaluate Query

[FliegendeWurst]

Intended Change

This PR fixes a slicing failure with a specific proof. In that particular case, the dynamically added taclet was slightly too different for the previous code to pick it up.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• Refactoring (behaviour should not change or only minimally change)
• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to change)
• There are changes to the (Java) code
• There are changes to the taclet rule base
• There are changes to the deployment/CI infrastructure (gradle, github, ...)
• Other:

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: slicing now works for the (confidential) proof file
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

cc @WolframPfeifer who reported the bug

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

[WolframPfeifer]

This PR fixes one of the original bug (file belongs to a student exercise, thus I do not want to attach it for the moment). However, there is a follow-up bug with the same file. Could you also look into the second bug, please?

[FliegendeWurst]

I think the other bug you are referring to is fixed by #3438

[WolframPfeifer]

I think the other bug you are referring to is fixed by #3438

Yes, thanks. I did not notice the other fix.

[WolframPfeifer]

The original bug seems to be fixed now, thanks!

Can you please take a look at my comments in the code (not sure about them, though)?

[FliegendeWurst]

I really don't understand the test failure. None of the changes in this PR change anything relevant to normal proof search. I'll do a no-op commit and push again.

[tobias-rnh]

I really don't understand the test failure. None of the changes in this PR change anything relevant to normal proof search. I'll do a no-op commit and push again.

I was having trouble with tests failing for no reason at all in the last few weeks too. First it was the unit tests only on Ubuntu and then the integration test testRunAllFunProofs. The caches in the repository were completely filled and after making some space, we got the tests to pass. I don't know if this could also be the problem here, but it might be worth a try.

[WolframPfeifer]

@FliegendeWurst I created a new PR (#3794), which aims to bring the fixes from here to the current main (quite tricky, because equality modulo proof is implemented completely differently now). Can you have a look at it? For my example (which I also uploaded now in my PR), it seems to work. However, I am not sure about the following: The equality comparison methods modulo proof for AntecSuccTacletGoalTemplate and RewriteTacletGoalTemplate are never called, since Java uses static binding on method parameters (in contrast to the dynamic binding that happens on this PR). However, apparently they are not needed?!

Furthermore, it seems that I had to revert a change you made here in AbstractProofReplayer (line 241):
You replaced currGoal.indexOfTaclets().getPartialInstantiatedApps() with currGoal.indexOfTaclets().allNoPosTacletApps(). I do not really understand this change, but the original variant (before this PR) seems to work in my example (otherwise, the dynamically created rule replaceKnownSelect_... was not found). What was the intention behind your change, or did you do it experimentally like I did 😉?

If you do not object, I would see if the tests succeed and merge #3794, and close this PR here.

[FliegendeWurst]

Furthermore, it seems that I had to revert a change you made here in AbstractProofReplayer (line 241): You replaced currGoal.indexOfTaclets().getPartialInstantiatedApps() with currGoal.indexOfTaclets().allNoPosTacletApps()

I'm not sure why I did that. Seems good to revert it.

However, apparently they are not needed?!

I think some implementations I added without really considering the need. So they can probably be omitted.