mk_fpa_mul method

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

\brief Floating-point multiplication

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

Implementation

Z3_ast mk_fpa_mul(
  Z3_context c,
  Z3_ast rm,
  Z3_ast t1,
  Z3_ast t2,
) {
  return _mk_fpa_mul(
    c,
    rm,
    t1,
    t2,
  );
}