mk_real method

Z3_ast mk_real(
  1. Z3_context c,
  2. int num,
  3. int den
)

\brief Create a real from a fraction.

\param c logical context. \param num numerator of rational. \param den denominator of rational.

\pre den != 0

\sa Z3_mk_numeral \sa Z3_mk_int \sa Z3_mk_real_int64 \sa Z3_mk_unsigned_int

def_API('Z3_mk_real', AST, (_in(CONTEXT), _in(INT), _in(INT)))

Implementation

Z3_ast mk_real(
  Z3_context c,
  int num,
  int den,
) {
  return _mk_real(
    c,
    num,
    den,
  );
}