Function z3_sys::Z3_mk_fpa_numeral_double

source · 
pub unsafe extern "C" fn Z3_mk_fpa_numeral_double(
    c: Z3_context,
    v: f64,
    ty: Z3_sort
) -> Z3_ast
Expand description

Create a numeral of FloatingPoint sort from a double.

This function is used to create numerals that fit in a double value. It is slightly faster than Z3_mk_numeral

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

ty must be a FloatingPoint sort

See also: