feat: Support more Alt-Ergo primitives

Gbury / dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction

BSD 2-Clause "Simplified" License

80 stars 17 forks source link

feat: Support more Alt-Ergo primitives #220

Open bclement-ocp opened 2 months ago

bclement-ocp commented 2 months ago

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 commented 2 months ago

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 commented 2 months ago

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.