feat: Support more Alt-Ergo primitives

[bclement-ocp]

This patch adds typing support for the following Alt-Ergo primitives:

• fpa_rounding_mode and its constructors (equivalent to RoundingMode in SMT-LIB);
• real_of_int (equivalent to to_real in SMT-LIB);
• real_is_int (equivalent to is_int in SMT-LIB);
• abs_int (equivalent to abs in SMT-LIB);
• int_floor (equialent to floor_to_int in SMT-LIB)

Note: These have been selected because they map directly to SMT-LIB types and primitives. There are additional floating-point (and real) primitives that do not exist at the SMT-LIB level, such as the round function. It is not clear at this point whether they should be added in Dolmen itself or in a separate plugin.

[Gbury]

Thanks !

As discussed offline, any primitive that is officially part of the alt-ergo's native language (something that you can actually decide as an alt-ergo dev), should indeed be implemented in dolmen itself (and not require any plugin), independently of whether they map directly to SMT-LIB primitives or not.

It's up to you whether you want to add all of the alt-ergo primitives in this PR, or via multiple PRs. Just tell me when you're satisfied with this PR and I'll review and merge it.

[bclement-ocp]

After thinking about it I am a bit on the fence on the topic. I would like the Dolmen experience to be consistent w.r.t builtins: either a builtin is fully supported by dolmen, including printing to SMT-LIB, or it is not at all and requires a plugin (once the corresponding PR is merged). Unfortunately this is already not the case (due to e.g. exponentiation and abs_real).

I'll think about it for a bit; in the meantime, I think this PR is uncontroversial and can be merged.