Function z3_sys::Z3_mk_tuple_sort

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

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 context
• mk_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 size num_fields allocated by the user.