mk_enumeration_sort method

Z3_sort mk_enumeration_sort(Z3_context c, Z3_symbol name, int n, Pointer<Z3_symbol> enum_names, Pointer<Z3_func_decl> enum_consts, Pointer<Z3_func_decl> enum_testers,)

\brief Create a enumeration sort.

An enumeration sort with \c n elements. This function will also declare the functions corresponding to the enumerations.

\param c logical context \param name name of the enumeration sort. \param n number of elements in enumeration sort. \param enum_names names of the enumerated elements. \param enum_consts constants corresponding to the enumerated elements. \param enum_testers predicates testing if terms of the enumeration sort correspond to an enumeration.

For example, if this function is called with three symbols A, B, C and the name S, then \c s is a sort whose name is S, and the function returns three terms corresponding to A, B, C in \c enum_consts. The array \c enum_testers has three predicates of type \ccode{(s -> Bool)}. The first predicate (corresponding to A) is true when applied to A, and false otherwise. Similarly for the other predicates.

def_API('Z3_mk_enumeration_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SYMBOL), _out_array(2, FUNC_DECL), _out_array(2, FUNC_DECL)))

Implementation

Z3_sort mk_enumeration_sort(
  Z3_context c,
  Z3_symbol name,
  int n,
  ffi.Pointer<Z3_symbol> enum_names,
  ffi.Pointer<Z3_func_decl> enum_consts,
  ffi.Pointer<Z3_func_decl> enum_testers,
) {
  return _mk_enumeration_sort(
    c,
    name,
    n,
    enum_names,
    enum_consts,
    enum_testers,
  );
}