alt-ergo icon indicating copy to clipboard operation
alt-ergo copied to clipboard

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

Open claudemarche opened this issue 6 months ago • 4 comments

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!

claudemarche avatar Jun 11 '25 08:06 claudemarche