Smart constructors for the FP theory

[Halbaroth]

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]

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]

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