mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 01:55:32 +00:00
Code Activity

Add Z3_get_array_arity (#7598)

Browse source
This commit is contained in:
Josh Berdine 2025-03-28 21:42:51 +00:00 • committed by GitHub
parent 934455a24b
commit 63ad2837e2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 24 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/api/api_array.cpp
View file

@ -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);

11
src/api/z3_api.h
View file

@ -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.