mk_fpa_inf method

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

\brief Create a floating-point infinity 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, -oo will be generated instead of +oo.

\sa Z3_mk_fpa_nan \sa Z3_mk_fpa_zero

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

Implementation

Z3_ast mk_fpa_inf(
  Z3_context c,
  Z3_sort s,
  bool negative,
) {
  return _mk_fpa_inf(
    c,
    s,
    negative,
  );
}