mk_fpa_zero method

Z3_ast mk_fpa_zero(
  1. Z3_context c,
  2. Z3_sort s,
  3. bool negative
)

\brief Create a floating-point zero of sort \c s.

\param c logical context \param s target sort \param negative indicates whether the result should be negative

When \c negative is \c true, -zero will be generated instead of +zero.

\sa Z3_mk_fpa_inf \sa Z3_mk_fpa_nan

def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))

Implementation

Z3_ast mk_fpa_zero(
  Z3_context c,
  Z3_sort s,
  bool negative,
) {
  return _mk_fpa_zero(
    c,
    s,
    negative,
  );
}