[−][src]Function z3_sys::Z3_mk_fpa_to_fp_int_real
pub unsafe extern "C" fn Z3_mk_fpa_to_fp_int_real(
c: Z3_context,
rm: Z3_ast,
exp: Z3_ast,
sig: Z3_ast,
s: Z3_sort
) -> Z3_ast
Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
Produces a term that represents the conversion of sig * 2^exp into a
floating-point term of sort s
. If necessary, the result will be rounded
according to rounding mode rm
.
c
: logical contextrm
: term of RoundingMode sortexp
: exponent term of Int sortsig
: significand term of Real sorts
: FloatingPoint sort
s
must be a FloatingPoint sort, rm
must be of RoundingMode sort,
exp
must be of int sort, sig
must be of real sort.