get_numeral_small method

bool get_numeral_small(
  1. Z3_context c,
  2. Z3_ast a,
  3. Pointer<Int64> num,
  4. Pointer<Int64> den,
)

\brief Return numeral value, as a pair of 64 bit numbers if the representation fits.

\param c logical context. \param a term. \param num numerator. \param den denominator.

Return \c true if the numeral value fits in 64 bit numerals, \c false otherwise.

\pre Z3_get_ast_kind(a) == Z3_NUMERAL_AST

def_API('Z3_get_numeral_small', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _out(INT64)))

Implementation

bool get_numeral_small(
  Z3_context c,
  Z3_ast a,
  ffi.Pointer<ffi.Int64> num,
  ffi.Pointer<ffi.Int64> den,
) {
  return _get_numeral_small(
    c,
    a,
    num,
    den,
  );
}