Function z3_sys::Z3_mk_finite_domain_sort

pub unsafe extern "C" fn Z3_mk_finite_domain_sort(
    c: Z3_context, 
    name: Z3_symbol, 
    size: u64
) -> Z3_sort

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.

See also:

• Z3_get_finite_domain_sort_size