[−][src]Function z3_sys::Z3_mk_fpa_to_fp_real
pub unsafe extern "C" fn Z3_mk_fpa_to_fp_real(
c: Z3_context,
rm: Z3_ast,
t: Z3_ast,
s: Z3_sort
) -> Z3_ast
Conversion of a term of real sort into a term of FloatingPoint sort.
Produces a term that represents the conversion of term t
of real sort 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 sortt
: term of Real sorts
: floating-point sort
s
must be a FloatingPoint sort, rm
must be of RoundingMode sort, t
must be of
Real sort.