Skip to main content

mk_fp

cvc5_sys

Function mk_fp 

Source 
pub unsafe extern "C" fn mk_fp(
    tm: *mut TermManager,
    exp: u32,
    sig: u32,
    val: Term,
) -> Term
Expand description

Create a floating-point value from a bit-vector given in IEEE-754 format. @param tm The term manager instance. @param exp Size of the exponent. @param sig Size of the significand. @param val Value of the floating-point constant as a bit-vector term. @return The floating-point value.