Supporting the float theory of the SMT-LIB

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo

https://alt-ergo.ocamlpro.com/

Other

133 stars 33 forks source link

Supporting the float theory of the SMT-LIB #904

Open Halbaroth opened 1 year ago

Halbaroth commented 1 year ago

The current implementation of Alt-Ergo doesn't support the float theory https://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml but a theory about round functions from the real to subset of real corresponding to finite floats with fixed precision. In particular, our implementation doesn't support infinity values or NaN values.

bclement-ocp commented 11 months ago

Postponing after discussion with the Why3 team, not a priority for now.