mk_fpa_to_fp_bv method

Z3_ast mk_fpa_to_fp_bv(
  1. Z3_context c,
  2. Z3_ast bv,
  3. Z3_sort s
)

\brief Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.

Produces a term that represents the conversion of a bit-vector term \c bv to a floating-point term of sort \c s.

\param c logical context \param bv a bit-vector term \param s floating-point sort

\c s must be a FloatingPoint sort, \c t must be of bit-vector sort, and the bit-vector size of \c bv must be equal to \ccode{ebits+sbits} of \c s. The format of the bit-vector is as defined by the IEEE 754-2008 interchange format.

def_API('Z3_mk_fpa_to_fp_bv', AST, (_in(CONTEXT),_in(AST),_in(SORT)))

Implementation

Z3_ast mk_fpa_to_fp_bv(
  Z3_context c,
  Z3_ast bv,
  Z3_sort s,
) {
  return _mk_fpa_to_fp_bv(
    c,
    bv,
    s,
  );
}