Function z3_sys::Z3_mk_datatype

pub unsafe extern "C" fn Z3_mk_datatype(
    c: Z3_context,
    name: Z3_symbol,
    num_constructors: c_uint,
    constructors: *mut Z3_constructor
) -> Z3_sort

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

• c: logical context.
• name: name of datatype.
• num_constructors: number of constructors passed in.
• constructors: array of constructor containers.