[][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 context
  • rm: term of RoundingMode sort
  • exp: exponent term of Int sort
  • sig: significand term of Real sort
  • s: 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.