mk_fpa_sub method

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

\brief Floating-point subtraction

\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_sub', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))

Implementation

Z3_ast mk_fpa_sub(
  Z3_context c,
  Z3_ast rm,
  Z3_ast t1,
  Z3_ast t2,
) {
  return _mk_fpa_sub(
    c,
    rm,
    t1,
    t2,
  );
}