Function z3_sys::Z3_model_get_num_sorts [−][src]
pub unsafe extern "C" fn Z3_model_get_num_sorts(
c: Z3_context,
m: Z3_model
) -> c_uint
Expand description
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
.