WIP: Simplify preprocess

[Stevendeo]

The preprocessing of a formula sometimes allow Alt-Ergo to discard useless patterns (especially on ite where the condition is trivial).
Three options are included in this PR:

• -simplify [y|n] activates (disactivates) the prepreocessing
• -simplify-th activates the use the theory in the simplification
• `-simplify-verbose' activates the debug messages

[Gbury]

A few things seem strange to me in this PR. Most of them I wrote in comments, but from a more global point of view:

• the expression simplifier is somewhat modular, but only with respect to booleans, which is a specialization that I find weird. I'd much prefer if arithmetic simplification would be done modularly, by the arithmetic theory, etc...
• the definitions of values is very (too much) specific, and actually incorrect with respect to the arbitrary precision integers that alt-ergo should be able to handle

[Stevendeo]

the definitions of values is very (too much) specific, and actually incorrect with respect to the arbitrary precision integers that alt-ergo should be able to handle

Indeed, the simplifyer now uses Zarith in place of floats.

the expression simplifier is somewhat modular, but only with respect to booleans, which is a specialization that I find weird. I'd much prefer if arithmetic simplification would be done modularly, by the arithmetic theory, etc...

You are right, I didn't took time to use theories for solving constant expressions as the preprocess was initially design to be fully agnostic. I extended the signature of theory to include arithmetic solving. We could export the type value for having a simpler theory signature, or extend the signature of the theory for each case.
This would be even better if the environment was updated along the simplificaton, as variables & expressions could be replaced along the simplification process.

[CLAassistant]

All committers have signed the CLA.