[][src]Function z3_sys::Z3_mk_fpa_fp

pub unsafe extern "C" fn Z3_mk_fpa_fp(
    c: Z3_context,
    sgn: Z3_ast,
    exp: Z3_ast,
    sig: Z3_ast
) -> Z3_ast

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 sign` 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.

  • c: logical context
  • sgn: sign
  • exp: exponent
  • sig: significand

See also: