search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
133 stars 33 forks source link

Smart constructors for the FP theory #746

Open Halbaroth opened 1 year ago

Halbaroth commented 1 year ago

The current Expr module does not expose smart constructors for FP theory as the Z3.FloatingPoint does. I noticed this lack while writing the interface for AE in the project https://github.com/wasp-platform/encoding. We should implement at least the constructors defined by the FP theory https://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml.

bclement-ocp commented 1 year ago

We don't have support for the smtlib FloatingPoint theory as far as I'm aware (we only have support for floating-point rounding with underflow, but nothing related to NaNs, infinites, or overflow), so I expect more work than just providing smart constructors.

Halbaroth commented 1 year ago

I know :/. We should work on it at some point.