Function z3_sys::Z3_mk_tuple_sort [−][src]
pub unsafe extern "C" fn Z3_mk_tuple_sort(
c: Z3_context,
mk_tuple_name: Z3_symbol,
num_fields: c_uint,
field_names: *const Z3_symbol,
field_sorts: *const Z3_sort,
mk_tuple_decl: *mut Z3_func_decl,
proj_decl: *mut Z3_func_decl
) -> Z3_sort
Expand description
Create a tuple type.
A tuple with n
fields has a constructor and n
projections.
This function will also declare the constructor and projection functions.
c
: logical contextmk_tuple_name
: name of the constructor function associated with the tuple type.num_fields
: number of fields in the tuple type.field_names
: name of the projection functions.field_sorts
: type of the tuple fields.mk_tuple_decl
: output parameter that will contain the constructor declaration.proj_decl
: output parameter that will contain the projection function declarations. This field must be a buffer of sizenum_fields
allocated by the user.