mk_fpa_numeral_int_uint method

Z3_ast mk_fpa_numeral_int_uint(
  1. Z3_context c,
  2. bool sgn,
  3. int exp,
  4. int sig,
  5. Z3_sort ty,
)

\brief Create a numeral of FloatingPoint sort from a sign bit and two integers.

\param c logical context \param sgn sign bit (true == negative) \param sig significand \param exp exponent \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 \sa Z3_mk_fpa_numeral_int64_uint64 \sa Z3_mk_numeral

def_API('Z3_mk_fpa_numeral_int_uint', AST, (_in(CONTEXT), _in(BOOL), _in(INT), _in(UINT), _in(SORT)))

Implementation

Z3_ast mk_fpa_numeral_int_uint(
  Z3_context c,
  bool sgn,
  int exp,
  int sig,
  Z3_sort ty,
) {
  return _mk_fpa_numeral_int_uint(
    c,
    sgn,
    exp,
    sig,
    ty,
  );
}