Function z3_sys::Z3_mk_fpa_numeral_int64_uint64

source · 
pub unsafe extern "C" fn Z3_mk_fpa_numeral_int64_uint64(
    c: Z3_context,
    sgn: Z3_bool,
    exp: i64,
    sig: u64,
    ty: Z3_sort
) -> Z3_ast
Expand description

Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.

  • c: logical context
  • sgn: sign bit (true == negative)
  • sig: significand
  • exp: exponent
  • ty: result sort

ty must be a FloatingPoint sort

See also: