Modification of simplify

[janheuer]

A formula "exists X (X = 1)" should be simplified to "#true" with the currently available simplifications, but using the simplify function this does not happen.

The problem is that the syntax tree is traversed once and the substitute_defined_variables simplification can only be applied when the root of the tree is reached. Therefore, the evaluate comparisons simplifications will not be applied as the root is not a comparison.

Instead of using a fixpoint algorithm it is sufficient to first apply substitute_defined_variables to the whole syntax tree and then use apply_all to apply all the other simplifications.

Of course a fixpoint algorithm is still necessary for more complicated examples (e.g. "exists X (X = 1 or exists Y (Y = 1 and Y != 1))" should simplify to "#true" but with the proposed modification it only simplifies to "#exists X (X = 1)", to reach "#true" it would require a second application of the simplify algorithm). But maybe this could still be useful as an option that:

• simplifies more than just apply_all,
• but only needs one additional traversal of the syntax tree instead of a full fixpoint algorithm.