Function z3_sys::Z3_model_get_num_sorts

pub unsafe extern "C" fn Z3_model_get_num_sorts(
    c: Z3_context,
    m: Z3_model
) -> c_uint

Return the number of uninterpreted sorts that m assigns an interpretation to.

Z3 also provides an interpretation for uninterpreted sorts used in a formula. The interpretation for a sort s is a finite set of distinct values. We say this finite set is the “universe” of s.

See also:

• Z3_model_get_sort
• Z3_model_get_sort_universe