Skip to main content

mk_fp_pos_zero

cvc5_sys

Function mk_fp_pos_zero 

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

Create a positive zero floating-point constant (Cvc5TermManager* tm, SMT-LIB: +zero). @param tm The term manager instance. @param exp Number of bits in the exponent. @param sig Number of bits in the significand. @return The floating-point constant.