mk_datatype method

Z3_sort mk_datatype(
  1. Z3_context c,
  2. Z3_symbol name,
  3. int num_constructors,
  4. Pointer<Z3_constructor> constructors,
)

\brief Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.

\param c logical context. \param name name of datatype. \param num_constructors number of constructors passed in. \param constructors array of constructor containers.

\sa Z3_mk_constructor \sa Z3_mk_constructor_list \sa Z3_mk_datatypes

def_API('Z3_mk_datatype', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _inout_array(2, CONSTRUCTOR)))

Implementation

Z3_sort mk_datatype(
  Z3_context c,
  Z3_symbol name,
  int num_constructors,
  ffi.Pointer<Z3_constructor> constructors,
) {
  return _mk_datatype(
    c,
    name,
    num_constructors,
    constructors,
  );
}