mk_tuple_sort method

Z3_sort mk_tuple_sort(Z3_context c, Z3_symbol mk_tuple_name, int num_fields, Pointer<Z3_symbol> field_names, Pointer<Z3_sort> field_sorts, Pointer<Z3_func_decl> mk_tuple_decl, Pointer<Z3_func_decl> proj_decl,)

\brief Create a tuple type.

A tuple with \c n fields has a constructor and \c n projections. This function will also declare the constructor and projection functions.

\param c logical context \param mk_tuple_name name of the constructor function associated with the tuple type. \param num_fields number of fields in the tuple type. \param field_names name of the projection functions. \param field_sorts type of the tuple fields. \param mk_tuple_decl output parameter that will contain the constructor declaration. \param proj_decl output parameter that will contain the projection function declarations. This field must be a buffer of size \c num_fields allocated by the user.

def_API('Z3_mk_tuple_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _out(FUNC_DECL), _out_array(2, FUNC_DECL)))

Implementation

Z3_sort mk_tuple_sort(
  Z3_context c,
  Z3_symbol mk_tuple_name,
  int num_fields,
  ffi.Pointer<Z3_symbol> field_names,
  ffi.Pointer<Z3_sort> field_sorts,
  ffi.Pointer<Z3_func_decl> mk_tuple_decl,
  ffi.Pointer<Z3_func_decl> proj_decl,
) {
  return _mk_tuple_sort(
    c,
    mk_tuple_name,
    num_fields,
    field_names,
    field_sorts,
    mk_tuple_decl,
    proj_decl,
  );
}