Skip to main content

mk_const_array

cvc5_sys

Function mk_const_array 

Source 
pub unsafe extern "C" fn mk_const_array(
    tm: *mut TermManager,
    sort: Sort,
    val: Term,
) -> Term
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.