FP: expose alt-ergo built-ins for FPA

[Stevendeo]

The builtin function float available in alt-ergo should be accessible for SMT2, as well as other built-ins such as the rounding mode.

CF #746

• Rounding mode : expose as RoundingMode
• Rounding function : expose as (_ ae.round)
• Define the other alt-ergo built-ins that should be accessible and how to access them.

[bclement-ocp]

* [ ]  Define the other alt-ergo built-ins that should be accessible and how to access them.

I think that these two are the only one relevant for floating points.

As for the others:

• real_of_int and int_floor are already available as to_real and to_int (from the Reals_Ints theory).
• The abs_XXX, min_XXX, max_XXX functions pre-date the introduction of if-then-else in Alt-Ergo and I don't think we should be recommending their use outside of the preludes (they are used for internal reasoning).
• int_ceil and the power functions could be exposed; I'm not sure — I think they also are mostly intended for internal reasoning in the preludes
• sqrt_real could be exposed (but again not FPA related)

If there are some of these functions we'd rather not expose — we need to check with the Why3 team that it's OK for them to not have access when/if they migrate to the SMT2 format.

[Stevendeo]

Should we close this issue now #876 is merged?