Function z3_sys::Z3_mk_finite_domain_sort [−][src]
pub unsafe extern "C" fn Z3_mk_finite_domain_sort(
c: Z3_context,
name: Z3_symbol,
size: u64
) -> Z3_sort
Expand description
Create a named finite domain sort.
To create constants that belong to the finite domain, use the APIs for creating numerals and pass a numeric constant together with the sort returned by this call. The numeric constant should be between 0 and the less than the size of the domain.