Improve trigonometric abstractions

[stilscher]

This PR improves the abstraction of the cos function if the argument is neither nan nor inf by

• storing also the inverted relationship between arguments of math functions and (assigned variable, math function) in the tmpSpecial analysis
• being more precise in the abstraction of cos(x) in case one can assure that variables representing isInf(x) and isNaN are definitely false

[michael-schwarz]

This yields 4 more successful tasks, I'll start it on the server.

[sim642]

Since this is still in need of refactoring/cleanup, it's too late to include for SV-COMP 2024. Four additional tasks out of ~32000 is not worth the risk for a possible regression.

[michael-schwarz]

Four additional tasks out of ~32000 is not worth the risk for a possible regression.

There is no regression, we ran it overnight on all tasks with full timeouts.

[sim642]

It's not just about SV-COMP though. It will be the representative version of Goblint for the entire year to come. If something doesn't yet meet our own standards, then it's not ready for such release. This is just too last minute, considering the freezing deadline we set for ourselves.

[michael-schwarz]

Ok. I think it would've been nice for Sarah's work this past week to be reflected in that version, but I won't push too hard.

[sim642]

Why is the TmpSpecialInv query needed? TmpSpecial itself already is a certain inverse (for refining the argument based on the return value), so TmpSpecialInv is some kind of inverse of the inverse. Is that not just normal forward evaluation? The new query is also used in eval not invariant.