[Feature Request] - Support of from_int function from Why3 on literals

[PaulBonnot]

The SmtLib standard specifies a function to_real : https://smtlib.cs.uiowa.edu/theories-Reals_Ints.shtml Currently, Alt-Ergo supports a similar function real_of_int in it's fpa theory : https://github.com/OCamlPro/alt-ergo/blob/next/src/preludes/fpa-theory-2019-10-08-19h00.ae#L55 The corresponding function in Why3 is from_int : https://why3.lri.fr/stdlib/real.html#from_int_117

It would be useful if Alt-Ergo could evaluate the real corresponding to this function applied on a literal. A simple example in Why3 would be :

use real.FromInt
goal from_int_val : from_int 100 = 100.0

Also, currently the real_of_int function only exists within the floating point theory, but I think it would be useful to have it even without floats.

[Stevendeo]

The real_of_int builtin function is indeed defined in the fpa theory, and with the option --use-fpa you do not need to include the whole fpa theory : just add logic real_of_int : int -> real and alt-ergo will interpret it as wanted. The --use-fpa option activates a flag which sets the set of function of the fpa theory as special operators.

Here is an example which is proved by alt-ergo --use-fpa:

logic real_of_int : int -> real

goal g: real_of_int(100) = 100.

Is using this option an issue for you? Does the inclusion of the whole fpa theory impacts alt-ergo's performances?

I am not sure about adding this builtin when not using fpa though. In my opinion the previous example should not return Valid without specifying more on real_of_int.

[Stevendeo]

Let me clarify something: it is not a good idea to use the option --use-fpa without the prelude; it was just a hack for having a working minimal example. In that case, goal g: real_of_int(100) = 100. is proven by alt-ergo file.ae --prelude ... --use-fpa

[PaulBonnot]

Indeed it works well with the the option and the inclusion of the prelude. I added some support for the fpa option in Why3 : https://gitlab.inria.fr/why3/why3/-/merge_requests/738