Don't dispatch SMT queries that can be proven False via simplification

[msooseth]

Description

This fixes issues where we dispatched a query that was constant False after simplification.

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[blishko]

This works, but I would suggest to spend some more time. I think the design could be improved.
What do I mean by that?
There are more places that call checkSat which might also benefit from this early check.
However, looking at them, there seems to be different strategies what they do with the propositions (and I admittedly do not understand everything that is going on there).
For example, in the function verify in SymExec, the queries are already being filtered for [PBool False] (see canBeSat).
On the other hand, function check in the same file does not seem to be doing anything in this regard.

It seems to me the code would benefit from some abstraction, for example a new function that would encompass both the transformation (assertProps) and dispatching to solver (checkSat). The check for False could be implemented inside this method. If all places that use checkSat now would be ported to use the new function, they would automatically benefit from this optimization.
However, that may require further thinking, as some of these places use cache or dispatch queries in parallel, and I don't know if the code could be easily changed there.

[msooseth]

Thanks! I actually agree with all what you said. Let me have another go at this, with a cleanup. I'll put this back into [DRAFT] and try to create such a helper function. It's a LOT of code repetition. It was a bad first attempt, sort of good for highlighting that it's messed up. I'll try doing it cleaner. Will be a bigger change but hopefully make the code a lot more readable and uniform.

[msooseth]

@blishko I have now adjusted it to use a subfunction. You were 100% right, it's a lot cleaner. There's still one use of the plain checkSat function, the solution obtaining code. I plan on writing a solution minimization PR, as it's been asked for by multiple people. This PR is now a ton cleaner and is essentially standalone, which is how it's supposed to be, hopefully :)

Note that we now pass App into more places, which is great for the long run, too. I had to use this MonadUnliftIO thing to unlift the IO from the App and then push it back in, but I think it's actually super-clean and readable. Used only where necessary, and it's quite clean and tidy I think. The only other way is to read out the conf, then runEnv conf $ ... but I find that less clean and more prone to error.

[blishko]

Pretty nice!