Extra functions supported by Alt-Ergo (SMT input) / documentation

[claudemarche]

Following a patch to Why3 proposed by @bclement-ocp, Why3 makes use of extra functions ae.pow and ae.sqrt_real. However, when I test it seems that ae.sqrt_real is not recognized.

I had a look at the manual but couldn't find any mention of ae.pow, ae.sqrt_real or any other functions supported except ae.round and ae.float{16|32|64}

Moreover, it seems that ae.pow operates both on integers and real numbers. I would be worth to document what would be the meaning of ae.pow for negative second argument. Or when both are 0.

Would it be possible to clarify the list of extra functions supported, with their domains of definition?

Thanks!

[bclement-ocp]

Ah, my apologies — we initially intended to support the non-standard primitives in the SMT-LIB format with an ae prefix, but only implemented printing for them, not parsing. That's my mistake. These should be removed from the Why3 driver for now, I think.

Regarding the semantics of ae.pow, they are the same as that of exponentiation (** and **.) in the native language. That is (ae.pow x y) is:

• Not specified when y is an integer ;
• Not specified when y is negative (for the version returning integers) ;
• 0^0 is 1 (although that is arguably a bug and should also be unspecified)

[claudemarche]

• Not specified when y is an integer ;

? What do you mean ?

[claudemarche]

Anyway, thanks for the feedback. Let me remind the main purpose of this issue: please document all that in the manual!

[bclement-ocp]

• Not specified when y is an integer ;

? What do you mean ?

Sorry, should be not specified when y is not an integer.

Let me remind the main purpose of this issue: please document all that in the manual!

Sure, they will be documented after they are actually implemented ;)