mk_datatypes method

void mk_datatypes(
  1. Z3_context c,
  2. int num_sorts,
  3. Pointer<Z3_symbol> sort_names,
  4. Pointer<Z3_sort> sorts,
  5. Pointer<Z3_constructor_list> constructor_lists,
)

\brief Create mutually recursive datatypes.

\param c logical context. \param num_sorts number of datatype sorts. \param sort_names names of datatype sorts. \param sorts array of datatype sorts. \param constructor_lists list of constructors, one list per sort.

\sa Z3_mk_constructor \sa Z3_mk_constructor_list \sa Z3_mk_datatype

def_API('Z3_mk_datatypes', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, SYMBOL), _out_array(1, SORT), _inout_array(1, CONSTRUCTOR_LIST)))

Implementation

void mk_datatypes(
  Z3_context c,
  int num_sorts,
  ffi.Pointer<Z3_symbol> sort_names,
  ffi.Pointer<Z3_sort> sorts,
  ffi.Pointer<Z3_constructor_list> constructor_lists,
) {
  return _mk_datatypes(
    c,
    num_sorts,
    sort_names,
    sorts,
    constructor_lists,
  );
}