mk_fpa_numeral_double method

Z3_ast mk_fpa_numeral_double(
  1. Z3_context c,
  2. double v,
  3. Z3_sort ty
)

\brief Create a numeral of FloatingPoint sort from a double.

This function is used to create numerals that fit in a double value. It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.

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

\c ty must be a FloatingPoint sort

\sa Z3_mk_fpa_fp \sa Z3_mk_fpa_numeral_float \sa Z3_mk_fpa_numeral_int \sa Z3_mk_fpa_numeral_int_uint \sa Z3_mk_fpa_numeral_int64_uint64 \sa Z3_mk_numeral

def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT)))

Implementation

Z3_ast mk_fpa_numeral_double(
  Z3_context c,
  double v,
  Z3_sort ty,
) {
  return _mk_fpa_numeral_double(
    c,
    v,
    ty,
  );
}