Function z3_sys::Z3_mk_fpa_to_fp_unsigned

pub unsafe extern "C" fn Z3_mk_fpa_to_fp_unsigned(
    c: Z3_context, 
    rm: Z3_ast, 
    t: Z3_ast, 
    s: Z3_sort
) -> Z3_ast

Conversion of a 2’s complement unsigned bit-vector term into a term of FloatingPoint sort.

Produces a term that represents the conversion of the bit-vector term t into a floating-point term of sort s. The bit-vector t is taken to be in unsigned 2’s complement format. If necessary, the result will be rounded according to rounding mode rm.

• c: logical context
• rm: term of RoundingMode sort
• t: term of bit-vector sort
• s: floating-point sort

s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of bit-vector sort.