Loop invariant based extraction of redundancy sets

[Paswalt]

This pull request is referring to #681

Since a significant portion of the codebase changed, and a lot of time has passed since I have last looked at the PR, I decided to create a new branch. It was easier to just create things anew than modify all the previous work. I will also close the very outdated branch to avoid keeping around too many of them, since it is not relevant anymore.

As a short summary what was done:

• A new result class was added, just as in Requirement redundancies: Approximation of explanation via invariants #681 which carries additional information for a redundant requirement
• A new case in the VerificationResultTransformer class was added, just as in Requirement redundancies: Approximation of explanation via invariants #681 to be able to handle incoming InvariantResults and print out the approximations that we derive from the invariant
• A new class called InvariantResultTransformer includes methods to parse the AST the InvariantResult carries. This responsibility was moved out of the result class for better style.

I would be happy for a (short) review. I think most of what I added should not conflict with anything else, in the hopes that this can be merged soon, so the ideas of my thesis can help people by analyzing requirements for redundancies :)

There's still two improvements that are missing, but I couldn't implement them spontaneously like this new version of the simple loop invariant based approximation. The other ideas will be handled through new PRs once the details on this first simple method are decided and once it is added, as it will take some time to look at all the new things in the meantime, and also at the new way to get invariants from arbitrary locations.

Things I am working on in the future:

• Get access to the location invariant of our choice again, via the new method enabled by recent changes to the codebase
• Add variable analysis as in https://github.com/ultimate-pa/ultimate/tree/wip/pw/redundancyExplanationVar which will be very easy once the initial approximation is properly implemented

Many thanks in advance!

(PS I should have used the closing keyword for the other PR here, sorry, it's late)

[maul-esel]

Looks good! I left some comments for (small) fixes and possible simplifications.

[schuessf]

This PR looks good, everything is properly capsuled inside PEAToBoogie without any consequences on other plugins.

[Paswalt]

I hope I have adequately replied to most review feedback. Is there something I forgot? Since I am new, how does a merge generally happen, is it okay if I do it or will it be done by someone else?

[maul-esel]

Since I am new, how does a merge generally happen, is it okay if I do it or will it be done by someone else?

The (informal) rule is that there should be two approvals, and of course no unresolved issues from any of the reviews. Then the person who opened the PR (i.e. you) merges.