pub unsafe extern "C" fn Z3_mk_fpa_numeral_float(
    c: Z3_context,
    v: f32,
    ty: Z3_sort
) -> Z3_ast
Expand description

Create a numeral of FloatingPoint sort from a float.

This function is used to create numerals that fit in a float value. It is slightly faster than Z3_mk_numeral since it is not necessary to parse a string.

  • c: logical context
  • v: value
  • ty: sort

ty must be a FloatingPoint sort

See also: