Skip to main content

cvc5_mk_integer

cvc5_sys

Function cvc5_mk_integer 

Source 
pub unsafe extern "C" fn cvc5_mk_integer(
    tm: *mut Cvc5TermManager,
    s: *const c_char,
) -> Cvc5Term
Expand description

Create an integer constant from a string. @param tm The term manager instance. @param s The string representation of the constant, may represent an integer (e.g., “123”). @return A constant of sort Integer assuming s represents an integer)