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 FloatAst.
[ ] 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 #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.
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.Float
Ast
.Float
s 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.Float
s to and fromReal
values or expose necessaryRoundingMode
functionality to implement suchReal
conversions in a useful manner.Float
behaviour as a library consumer is heavily limited by #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 othertrinop
s; It is supposed to receivemul(ctx, roundingMode, fpAst, fpAst)
, but is instead receivingmul(ctx, fpAst, fpAst, fpAst)
, which causes floats to always hit theis_null
assertion during themul
invocation; This appears to be untested.