[−][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 contextsgn
: signexp
: exponentsig
: significand