Skip to main content

get_model_domain_elements

Function get_model_domain_elements 

Source
pub unsafe extern "C" fn get_model_domain_elements(
    cvc5: *mut Solver,
    sort: Sort,
    size: *mut usize,
) -> *const Term
Expand description

Get the domain elements of uninterpreted sort s in the current model. The current model interprets s as the finite sort whose domain elements are given in the return value of this function.

@param cvc5 The solver instance. @param sort The uninterpreted sort in question. @param size The size of the resulting domain elements array. @return The domain elements of s in the current model.