Function z3_sys::Z3_mk_fpa_to_fp_unsigned [−][src]
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
Expand description
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 contextrm
: term of RoundingMode sortt
: term of bit-vector sorts
: floating-point sort
s
must be a FloatingPoint sort, rm
must be of RoundingMode sort, t
must be
of bit-vector sort.