Function z3_sys::Z3_mk_fpa_to_fp_bv [−][src]
pub unsafe extern "C" fn Z3_mk_fpa_to_fp_bv(
c: Z3_context,
bv: Z3_ast,
s: Z3_sort
) -> Z3_ast
Expand description
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
Produces a term that represents the conversion of a bit-vector term bv
to a
floating-point term of sort s
.
c
: logical contextbv
: a bit-vector terms
: floating-point sort
s
must be a FloatingPoint sort, t
must be of bit-vector sort, and the bit-vector
size of bv
must be equal to ebits+sbits of s
. The format of the bit-vector is
as defined by the IEEE 754-2008 interchange format.