mk_finite_domain_sort method

Z3_sort mk_finite_domain_sort(
  1. Z3_context c,
  2. Z3_symbol name,
  3. int size
)

\brief 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.

\sa Z3_get_finite_domain_sort_size

def_API('Z3_mk_finite_domain_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT64)))

Implementation

Z3_sort mk_finite_domain_sort(
  Z3_context c,
  Z3_symbol name,
  int size,
) {
  return _mk_finite_domain_sort(
    c,
    name,
    size,
  );
}