Function z3_sys::Z3_get_numeral_small [−][src]
pub unsafe extern "C" fn Z3_get_numeral_small(
c: Z3_context,
a: Z3_ast,
num: *mut i64,
den: *mut i64
) -> bool
Expand description
Return numeral value, as a pair of 64 bit numbers if the representation fits.
c
: logical context.a
: term.num
: numerator.den
: denominator.
Return true
if the numeral value fits in 64 bit numerals, false
otherwise.
Preconditions:
Z3_get_ast_kind(a) == AstKind::Numeral