Function z3_sys::Z3_mk_fpa_to_fp_bv

pub unsafe extern "C" fn Z3_mk_fpa_to_fp_bv(
    c: Z3_context, 
    bv: Z3_ast, 
    s: Z3_sort
) -> Z3_ast

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 context
• bv: a bit-vector term
• s: 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.