diff --git a/src/api/api_array.cpp b/src/api/api_array.cpp index 522976f01..6613892df 100644 --- a/src/api/api_array.cpp +++ b/src/api/api_array.cpp @@ -300,6 +300,19 @@ extern "C" { to_sort(t)->get_decl_kind() == ARRAY_SORT; } + unsigned Z3_API Z3_get_array_arity(Z3_context c, Z3_sort s) { + Z3_TRY; + LOG_Z3_get_array_arity(c, s); + RESET_ERROR_CODE(); + sort * a = to_sort(s); + if (Z3_get_sort_kind(c, s) != Z3_ARRAY_SORT) { + SET_ERROR_CODE(Z3_INVALID_ARG, "sort should be an array"); + return 0; + } + return get_array_arity(a); + Z3_CATCH_RETURN(0); + } + Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t) { Z3_TRY; LOG_Z3_get_array_sort_domain(c, t); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index bc10d5278..daf14ae71 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4497,6 +4497,17 @@ extern "C" { */ bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r); + /** + \brief Return the arity (number of dimensions) of the given array sort. + + \pre Z3_get_sort_kind(s) == Z3_ARRAY_SORT + + \sa Z3_get_array_sort_domain_n + + def_API('Z3_get_array_arity', UINT, (_in(CONTEXT), _in(SORT))) + */ + unsigned Z3_API Z3_get_array_arity(Z3_context c, Z3_sort s); + /** \brief Return the domain of the given array sort. In the case of a multi-dimensional array, this function returns the sort of the first dimension.