diff --git a/src/api/api_array.cpp b/src/api/api_array.cpp index 7aa3a87bf..cb254dbdd 100644 --- a/src/api/api_array.cpp +++ b/src/api/api_array.cpp @@ -294,14 +294,19 @@ extern "C" { return Z3_mk_store(c, set, elem, Z3_mk_false(c)); } + static bool is_array_sort(Z3_context c, Z3_sort t) { + return + to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() && + to_sort(t)->get_decl_kind() == ARRAY_SORT; + } + 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); RESET_ERROR_CODE(); CHECK_VALID_AST(t, nullptr); - if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() && - to_sort(t)->get_decl_kind() == ARRAY_SORT) { - Z3_sort r = reinterpret_cast(to_sort(t)->get_parameter(0).get_ast()); + if (is_array_sort(c, t)) { + Z3_sort r = of_sort(get_array_domain(to_sort(t), 0)); RETURN_Z3(r); } SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); @@ -314,10 +319,8 @@ extern "C" { LOG_Z3_get_array_sort_domain_n(c, t, idx); RESET_ERROR_CODE(); CHECK_VALID_AST(t, nullptr); - if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() && - to_sort(t)->get_decl_kind() == ARRAY_SORT && - get_array_arity(to_sort(t)) > idx) { - Z3_sort r = reinterpret_cast(get_array_domain(to_sort(t), idx)); + if (is_array_sort(c, t) && get_array_arity(to_sort(t)) > idx) { + Z3_sort r = of_sort(get_array_domain(to_sort(t), idx)); RETURN_Z3(r); } SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); @@ -330,10 +333,8 @@ extern "C" { LOG_Z3_get_array_sort_range(c, t); RESET_ERROR_CODE(); CHECK_VALID_AST(t, nullptr); - if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() && - to_sort(t)->get_decl_kind() == ARRAY_SORT) { - unsigned n = to_sort(t)->get_num_parameters(); - Z3_sort r = reinterpret_cast(to_sort(t)->get_parameter(n-1).get_ast()); + if (is_array_sort(c, t)) { + Z3_sort r = of_sort(get_array_range(to_sort(t))); RETURN_Z3(r); } SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); diff --git a/src/api/java/ArraySort.java b/src/api/java/ArraySort.java index 30f4178fa..3d3ef3041 100644 --- a/src/api/java/ArraySort.java +++ b/src/api/java/ArraySort.java @@ -35,6 +35,18 @@ public class ArraySort extends Sort Native.getArraySortDomain(getContext().nCtx(), getNativeObject())); } + /** + * The domain of a multi-dimensional array sort. + * @throws Z3Exception + * @throws Z3Exception on error + * @return a sort + **/ + public D getDomain(int idx) + { + return (D) Sort.create(getContext(), + Native.getArraySortDomainN(getContext().nCtx(), getNativeObject(), idx)); + } + /** * The range of the array sort. * @throws Z3Exception