Function z3_sys::Z3_mk_fpa_sort[−][src]

pub unsafe extern "C" fn Z3_mk_fpa_sort(
    c: Z3_context, 
    ebits: c_uint, 
    sbits: c_uint
) -> Z3_sort
Expand description

Create a FloatingPoint sort.

  • c: logical context
  • ebits: number of exponent bits
  • sbits: number of significand bits

NOTE: ebits must be larger than 1 and sbits must be larger than 2.