mk_fpa_numeral_int method

Z3_ast mk_fpa_numeral_int(
  1. Z3_context c,
  2. int v,
  3. Z3_sort ty
)

\brief Create a numeral of FloatingPoint sort from a signed integer.

\param c logical context \param v value \param ty result sort

\c ty must be a FloatingPoint sort

\sa Z3_mk_fpa_fp \sa Z3_mk_fpa_numeral_double \sa Z3_mk_fpa_numeral_float \sa Z3_mk_fpa_numeral_int_uint \sa Z3_mk_fpa_numeral_int64_uint64 \sa Z3_mk_numeral

def_API('Z3_mk_fpa_numeral_int', AST, (_in(CONTEXT), _in(INT), _in(SORT)))

Implementation

Z3_ast mk_fpa_numeral_int(
  Z3_context c,
  int v,
  Z3_sort ty,
) {
  return _mk_fpa_numeral_int(
    c,
    v,
    ty,
  );
}