mk_fpa_add method

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

\brief Floating-point addition

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

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

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

Implementation

Z3_ast mk_fpa_add(
  Z3_context c,
  Z3_ast rm,
  Z3_ast t1,
  Z3_ast t2,
) {
  return _mk_fpa_add(
    c,
    rm,
    t1,
    t2,
  );
}