Most functionality around Float types is unbound. Adding bindings without editing or forking this library is impossible without the extreme hack of declaring copies of the structs and transmuting references between them to trick Rust into accessing the private fields z3_sort or z3_ctx.
I was attempting to invoke z3_sys's Z3_mk_fpa_to_fp_real, but it requires raw access to the Z3_sort values, as well as a rounding mode, but functions like z3_sys::Z3_mk_fpa_rne require an instance of the raw Z3_context, which lack a high-level wrapper.
Most functionality around
Floattypes is unbound. Adding bindings without editing or forking this library is impossible without the extreme hack of declaring copies of the structs and transmuting references between them to trick Rust into accessing the private fieldsz3_sortorz3_ctx.I was attempting to invoke
z3_sys'sZ3_mk_fpa_to_fp_real, but it requires raw access to theZ3_sortvalues, as well as a rounding mode, but functions likez3_sys::Z3_mk_fpa_rnerequire an instance of the rawZ3_context, which lack a high-level wrapper.