Skip to main content

cvc5_mk_const_array

cvc5_sys

Function cvc5_mk_const_array 

Source 
pub unsafe extern "C" fn cvc5_mk_const_array(
    tm: *mut Cvc5TermManager,
    sort: Cvc5Sort,
    val: Cvc5Term,
) -> Cvc5Term
Expand description

Create a constant array with the provided constant value stored at every index. @param tm The term manager instance. @param sort The sort of the constant array (must be an array sort). @param val The constant value to store (must match the sort’s element sort). @return The constant array term.