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,
);
}