get_datatype_sort_constructor_accessor method

Z3_func_decl get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, int idx_c, int idx_a,)

\brief Return idx_a'th accessor for the idx_c'th constructor.

\pre Z3_get_sort_kind(t) == Z3_DATATYPE_SORT \pre idx_c < Z3_get_datatype_sort_num_constructors(c, t) \pre idx_a < Z3_get_domain_size(c, Z3_get_datatype_sort_constructor(c, idx_c))

\sa Z3_get_datatype_sort_num_constructors \sa Z3_get_datatype_sort_constructor \sa Z3_get_datatype_sort_recognizer

def_API('Z3_get_datatype_sort_constructor_accessor', FUNC_DECL, (_in(CONTEXT), _in(SORT), _in(UINT), _in(UINT)))

Implementation

Z3_func_decl get_datatype_sort_constructor_accessor(
  Z3_context c,
  Z3_sort t,
  int idx_c,
  int idx_a,
) {
  return _get_datatype_sort_constructor_accessor(
    c,
    t,
    idx_c,
    idx_a,
  );
}