Function z3_sys::Z3_fpa_get_numeral_significand_uint64

source ·

pub unsafe extern "C" fn Z3_fpa_get_numeral_significand_uint64(
    c: Z3_context,
    t: Z3_ast,
    n: *mut u64
) -> bool

Expand description

Return the significand value of a floating-point numeral as a uint64.

c: logical context
t: a floating-point numeral
n: pointer to output uint64

Remarks: This function extracts the significand bits in t, without the hidden bit or normalization. Sets the ErrorCode::InvalidArg error code if the significand does not fit into a uint64. NaN is an invalid argument.