alt-ergo
alt-ergo copied to clipboard
WIP: Simplify preprocess
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
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.