Function z3_sys::Z3_mk_datatypes [−][src]
pub unsafe extern "C" fn Z3_mk_datatypes(
c: Z3_context,
num_sorts: c_uint,
sort_names: *const Z3_symbol,
sorts: *mut Z3_sort,
constructor_lists: *mut Z3_constructor_list
)
Expand description
Create mutually recursive datatypes.
c
: logical context.num_sorts
: number of datatype sorts.sort_names
: names of datatype sorts.sorts
: array of datatype sorts.constructor_lists
: list of constructors, one list per sort.