Float binding issues

[Dessix]

The high-level library provides limited Float support, but what is present seems to be below the minimum necessary to make use of float sorts.

• The bindings do not expose a means of retrieving a float value from a solved Float Ast.
• Floats cannot be displayed as their human-readable value, instead displaying hex forms of the raw sign, exponent, and mantissa bits. While these values can technically be extracted and reparsed to bypass the first limitation, this is unlikely to be the library's intended solution.
• There is no provided way to convert Floats to and from Real values or expose necessary RoundingMode functionality to implement such Real conversions in a useful manner.
• Binding missing Float behaviour as a library consumer is heavily limited by No way to access the raw Z3_sort from Sort<'ctx> or Z3_context from Context #290, which also limits attempts at improvements which could eventually be integrated into the library if they prove useful.
• Z3_mk_fpa_mul is bound incorrectly, as may be other trinops; It is supposed to receive mul(ctx, roundingMode, fpAst, fpAst), but is instead receiving mul(ctx, fpAst, fpAst, fpAst), which causes floats to always hit the is_null assertion during the mul invocation; This appears to be untested.

[dragazo]

I think the first point is possible with Float::as_f64 on the result of Model::eval provided with a Float.