mk_fpa_div method

Z3_ast mk_fpa_div(
  1. Z3_context c,
  2. Z3_ast rm,
  3. Z3_ast t1,
  4. Z3_ast t2,
)

\brief Floating-point division

\param c logical context \param rm term of RoundingMode sort \param t1 term of FloatingPoint sort. \param t2 term of FloatingPoint sort

The nodes \c rm must be of RoundingMode sort, \c t1 and \c t2 must have the same FloatingPoint sort.

def_API('Z3_mk_fpa_div', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))

Implementation

Z3_ast mk_fpa_div(
  Z3_context c,
  Z3_ast rm,
  Z3_ast t1,
  Z3_ast t2,
) {
  return _mk_fpa_div(
    c,
    rm,
    t1,
    t2,
  );
}