Add Z3_get_array_arity

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

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.