mk_fpa_fp method

Z3_ast mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig,)

\brief Create an expression of FloatingPoint sort from three bit-vector expressions.

This is the operator named `fp' in the SMT FP theory definition. Note that \c sgn is required to be a bit-vector of size 1. Significand and exponent are required to be longer than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes of the arguments. The exponent is assumed to be in IEEE-754 biased representation.

\param c logical context \param sgn sign \param exp exponent \param sig significand

\sa Z3_mk_fpa_numeral_double \sa Z3_mk_fpa_numeral_float \sa Z3_mk_fpa_numeral_int \sa Z3_mk_fpa_numeral_int_uint \sa Z3_mk_fpa_numeral_int64_uint64 \sa Z3_mk_numeral

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

Implementation

Z3_ast mk_fpa_fp(
  Z3_context c,
  Z3_ast sgn,
  Z3_ast exp,
  Z3_ast sig,
) {
  return _mk_fpa_fp(
    c,
    sgn,
    exp,
    sig,
  );
}