Function z3_sys::Z3_mk_fpa_to_fp_float[−][src]

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

Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

Produces a term that represents the conversion of a floating-point term t to 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
  • t: term of FloatingPoint sort
  • s: floating-point sort

s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of floating-point sort.