additional array functions exposed over API, ping #1223

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_array.cpp

@@ -34,6 +34,19 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const* domain, Z3_sort range) {
+        Z3_TRY;
+        LOG_Z3_mk_array_sort_n(c, n, domain, range);
+        RESET_ERROR_CODE();
+        vector<parameter> params;
+        for (unsigned i = 0; i < n; ++i) params.push_back(parameter(to_sort(domain[i])));
+        params.push_back(parameter(to_sort(range)));
+        sort * ty =  mk_c(c)->m().mk_sort(mk_c(c)->get_array_fid(), ARRAY_SORT, params.size(), params.c_ptr());
+        mk_c(c)->save_ast_trail(ty);
+        RETURN_Z3(of_sort(ty));
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i) {
         Z3_TRY;
         LOG_Z3_mk_select(c, a, i);
@@ -57,6 +70,35 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs) {
+        Z3_TRY;
+        LOG_Z3_mk_select_n(c, a, n, idxs);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        expr * _a        = to_expr(a);
+        // expr * _i        = to_expr(i);
+        sort * a_ty = m.get_sort(_a);
+        // sort * i_ty = m.get_sort(_i);
+        if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) {
+            SET_ERROR_CODE(Z3_SORT_ERROR);
+            RETURN_Z3(0);
+        }
+        ptr_vector<sort> domain;
+        ptr_vector<expr> args;
+        args.push_back(_a);
+        domain.push_back(a_ty);
+        for (unsigned i = 0; i < n; ++i) {
+            args.push_back(to_expr(idxs[i]));
+            domain.push_back(m.get_sort(to_expr(idxs[i])));
+        }
+        func_decl * d   = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_SELECT, 2, a_ty->get_parameters(), domain.size(), domain.c_ptr());
+        app * r        = m.mk_app(d, args.size(), args.c_ptr());
+        mk_c(c)->save_ast_trail(r);
+        check_sorts(c, r);
+        RETURN_Z3(of_ast(r));
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v) {
         Z3_TRY;
         LOG_Z3_mk_store(c, a, i, v);
@@ -82,6 +124,37 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs, Z3_ast v) {
+        Z3_TRY;
+        LOG_Z3_mk_store_n(c, a, n, idxs, v);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        expr * _a        = to_expr(a);
+        expr * _v        = to_expr(v);
+        sort * a_ty = m.get_sort(_a);
+        sort * v_ty = m.get_sort(_v);
+        if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) {
+            SET_ERROR_CODE(Z3_SORT_ERROR);
+            RETURN_Z3(0);
+        }
+        ptr_vector<sort> domain;
+        ptr_vector<expr> args;
+        args.push_back(_a);
+        domain.push_back(a_ty);
+        for (unsigned i = 0; i < n; ++i) {
+            args.push_back(to_expr(idxs[i]));
+            domain.push_back(m.get_sort(to_expr(idxs[i])));
+        }
+        args.push_back(_v);
+        domain.push_back(v_ty);
+        func_decl * d   = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_STORE, 2, a_ty->get_parameters(), domain.size(), domain.c_ptr());
+        app * r        = m.mk_app(d, args.size(), args.c_ptr());
+        mk_c(c)->save_ast_trail(r);
+        check_sorts(c, r);
+        RETURN_Z3(of_ast(r));
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args) {
         Z3_TRY;
         LOG_Z3_mk_map(c, f, n, args);
@@ -188,6 +261,18 @@ extern "C" {
     MK_BINARY(Z3_mk_set_subset, mk_c(c)->get_array_fid(), OP_SET_SUBSET, SKIP);
     MK_BINARY(Z3_mk_array_ext, mk_c(c)->get_array_fid(), OP_ARRAY_EXT, SKIP);
 
+    Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f) {
+        Z3_TRY;
+        LOG_Z3_mk_as_array(c, f);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        array_util a(m);
+        app * r = a.mk_as_array(to_func_decl(f));
+        mk_c(c)->save_ast_trail(r);
+        return of_ast(r);
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_ast Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set) {
         return Z3_mk_select(c, set, elem);
     }
@@ -222,7 +307,8 @@ extern "C" {
         CHECK_VALID_AST(t, 0);
         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<Z3_sort>(to_sort(t)->get_parameter(1).get_ast());
+            unsigned n = to_sort(t)->get_num_parameters();
+            Z3_sort r = reinterpret_cast<Z3_sort>(to_sort(t)->get_parameter(n-1).get_ast());
             RETURN_Z3(r);
         }
         SET_ERROR_CODE(Z3_INVALID_ARG);

src/api/c++/z3++.h

@@ -250,6 +250,8 @@ namespace z3 {
            Example: Given a context \c c, <tt>c.array_sort(c.int_sort(), c.bool_sort())</tt> is an array sort from integer to Boolean.
         */
         sort array_sort(sort d, sort r);
+        sort array_sort(sort_vector const& d, sort r);
+
         /**
            \brief Return an enumeration sort: enum_names[0], ..., enum_names[n-1].
            \c cs and \c ts are output parameters. The method stores in \c cs the constants corresponding to the enumerated elements,
@@ -2327,6 +2329,11 @@ namespace z3 {
     inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
 
     inline sort context::array_sort(sort d, sort r) { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }
+    inline sort context::array_sort(sort_vector const& d, sort r) {
+        array<Z3_sort> dom(d);
+        Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s); 
+    }
+
     inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
         array<Z3_symbol> _enum_names(n);
         for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
@@ -2573,11 +2580,32 @@ namespace z3 {
         a.check_error();
         return expr(a.ctx(), r);
     }
+    inline expr select(expr const & a, expr_vector const & i) {
+        check_context(a, i);
+        array<Z3_ast> idxs(i);
+        Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
+        a.check_error();
+        return expr(a.ctx(), r);
+    }
+
     inline expr store(expr const & a, int i, expr const & v) { return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }
     inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
     inline expr store(expr const & a, int i, int v) {
         return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
     }
+    inline expr store(expr const & a, expr_vector const & i, expr const & v) {
+        check_context(a, i); check_context(a, v);
+        array<Z3_ast> idxs(i);
+        Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
+        a.check_error();
+        return expr(a.ctx(), r);
+    }
+
+    inline expr as_array(func_decl & f) { 
+        Z3_ast r = Z3_mk_as_array(f.ctx(), f); 
+        f.check_error();  
+        return expr(f.ctx(), r); 
+    }
 
 #define MK_EXPR1(_fn, _arg)                     \
     Z3_ast r = _fn(_arg.ctx(), _arg);           \

src/api/dotnet/ArraySort.cs

@@ -63,6 +63,13 @@ namespace Microsoft.Z3
             Contract.Requires(domain != null);
             Contract.Requires(range != null);
         }
+        internal ArraySort(Context ctx, Sort[] domain, Sort range)
+            : base(ctx, Native.Z3_mk_array_sort_n(ctx.nCtx, (uint)domain.Length, AST.ArrayToNative(domain), range.NativeObject))
+        {
+            Contract.Requires(ctx != null);
+            Contract.Requires(domain != null);
+            Contract.Requires(range != null);
+        }
         #endregion
     };
 

src/api/dotnet/Context.cs

@@ -274,6 +274,20 @@ namespace Microsoft.Z3
             return new ArraySort(this, domain, range);
         }
 
+        /// <summary>
+        /// Create a new n-ary array sort.
+        /// </summary>
+        public ArraySort MkArraySort(Sort[] domain, Sort range)
+        {
+            Contract.Requires(domain != null);
+            Contract.Requires(range != null);
+            Contract.Ensures(Contract.Result<ArraySort>() != null);
+
+            CheckContextMatch<Sort>(domain);
+            CheckContextMatch(range);
+            return new ArraySort(this, domain, range);
+        }
+
         /// <summary>
         /// Create a new tuple sort.
         /// </summary>
@@ -2113,6 +2127,7 @@ namespace Microsoft.Z3
             return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
         }
 
+
         /// <summary>
         /// Array read.
         /// </summary>
@@ -2123,8 +2138,8 @@ namespace Microsoft.Z3
         /// The node <c>a</c> must have an array sort <c>[domain -> range]</c>,
         /// and <c>i</c> must have the sort <c>domain</c>.
         /// The sort of the result is <c>range</c>.
-        /// <seealso cref="MkArraySort"/>
+        /// <seealso cref="MkArraySort(Sort, Sort)"/>
-        /// <seealso cref="MkStore"/>
+        /// <seealso cref="MkStore(ArrayExpr, Expr, Expr)"/>
         /// </remarks>
         public Expr MkSelect(ArrayExpr a, Expr i)
         {
@@ -2137,6 +2152,30 @@ namespace Microsoft.Z3
             return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
         }
 
+        /// <summary>
+        /// Array read.
+        /// </summary>
+        /// <remarks>
+        /// The argument <c>a</c> is the array and <c>args</c> are the indices
+        /// of the array that gets read.
+        ///
+        /// The node <c>a</c> must have an array sort <c>[domain1,..,domaink -> range]</c>,
+        /// and <c>args</c> must have the sort <c>domain1,..,domaink</c>.
+        /// The sort of the result is <c>range</c>.
+        /// <seealso cref="MkArraySort(Sort, Sort)"/>
+        /// <seealso cref="MkStore(ArrayExpr, Expr, Expr)"/>
+        /// </remarks>
+        public Expr MkSelect(ArrayExpr a, params Expr[] args)
+        {
+            Contract.Requires(a != null);
+            Contract.Requires(args != null && Contract.ForAll(args, n => n != null));
+            Contract.Ensures(Contract.Result<Expr>() != null);
+
+            CheckContextMatch(a);
+            CheckContextMatch<Expr>(args);
+            return Expr.Create(this, Native.Z3_mk_select_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
+        }
+
         /// <summary>
         /// Array update.
         /// </summary>
@@ -2151,8 +2190,9 @@ namespace Microsoft.Z3
         /// on all indices except for <c>i</c>, where it maps to <c>v</c>
         /// (and the <c>select</c> of <c>a</c> with
         /// respect to <c>i</c> may be a different value).
-        /// <seealso cref="MkArraySort"/>
+        /// <seealso cref="MkArraySort(Sort, Sort)"/>
-        /// <seealso cref="MkSelect"/>
+        /// <seealso cref="MkSelect(ArrayExpr, Expr)"/>
+        /// <seealso cref="MkSelect(ArrayExpr, Expr[])"/>
         /// </remarks>
         public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
         {
@@ -2167,14 +2207,45 @@ namespace Microsoft.Z3
             return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
         }
 
+        /// <summary>
+        /// Array update.
+        /// </summary>
+        /// <remarks>
+        /// The node <c>a</c> must have an array sort <c>[domain1,..,domaink -> range]</c>,
+        /// <c>args</c> must have sort <c>domain1,..,domaink</c>,
+        /// <c>v</c> must have sort range. The sort of the result is <c>[domain -> range]</c>.
+        /// The semantics of this function is given by the theory of arrays described in the SMT-LIB
+        /// standard. See http://smtlib.org for more details.
+        /// The result of this function is an array that is equal to <c>a</c>
+        /// (with respect to <c>select</c>)
+        /// on all indices except for <c>args</c>, where it maps to <c>v</c>
+        /// (and the <c>select</c> of <c>a</c> with
+        /// respect to <c>args</c> may be a different value).
+        /// <seealso cref="MkArraySort(Sort, Sort)"/>
+        /// <seealso cref="MkSelect(ArrayExpr, Expr)"/>
+        /// <seealso cref="MkSelect(ArrayExpr, Expr[])"/>
+        /// </remarks>
+        public ArrayExpr MkStore(ArrayExpr a, Expr[] args, Expr v)
+        {
+            Contract.Requires(a != null);
+            Contract.Requires(args != null);
+            Contract.Requires(v != null);
+            Contract.Ensures(Contract.Result<ArrayExpr>() != null);
+
+            CheckContextMatch<Expr>(args);
+            CheckContextMatch(a);
+            CheckContextMatch(v);
+            return new ArrayExpr(this, Native.Z3_mk_store_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args), v.NativeObject));
+        }
+
         /// <summary>
         /// Create a constant array.
         /// </summary>
         /// <remarks>
         /// The resulting term is an array, such that a <c>select</c>on an arbitrary index
         /// produces the value <c>v</c>.
-        /// <seealso cref="MkArraySort"/>
+        /// <seealso cref="MkArraySort(Sort, Sort)"/>
-        /// <seealso cref="MkSelect"/>
+        /// <seealso cref="MkSelect(ArrayExpr, Expr)"/>
         /// </remarks>
         public ArrayExpr MkConstArray(Sort domain, Expr v)
         {
@@ -2194,9 +2265,9 @@ namespace Microsoft.Z3
         /// Eeach element of <c>args</c> must be of an array sort <c>[domain_i -> range_i]</c>.
         /// The function declaration <c>f</c> must have type <c> range_1 .. range_n -> range</c>.
         /// <c>v</c> must have sort range. The sort of the result is <c>[domain_i -> range]</c>.
-        /// <seealso cref="MkArraySort"/>
+        /// <seealso cref="MkArraySort(Sort, Sort)"/>
-        /// <seealso cref="MkSelect"/>
+        /// <seealso cref="MkSelect(ArrayExpr, Expr)"/>
-        /// <seealso cref="MkStore"/>
+        /// <seealso cref="MkStore(ArrayExpr, Expr, Expr)"/>
         /// </remarks>
         public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
         {

src/api/java/ArraySort.java

@@ -56,4 +56,10 @@ public class ArraySort extends Sort
         super(ctx, Native.mkArraySort(ctx.nCtx(), domain.getNativeObject(),
                 range.getNativeObject()));
     }
+
+    ArraySort(Context ctx, Sort[] domains, Sort range)
+    {
+        super(ctx, Native.mkArraySortN(ctx.nCtx(), domains.length, AST.arrayToNative(domains),
+                range.getNativeObject()));
+    }
 };

src/api/java/Context.java

@@ -224,6 +224,17 @@ public class Context implements AutoCloseable {
         return new ArraySort(this, domain, range);
     }
 
+
+    /**
+     * Create a new array sort.
+     **/
+    public ArraySort mkArraySort(Sort[] domains, Sort range)
+    {
+        checkContextMatch(domains);
+        checkContextMatch(range);
+        return new ArraySort(this, domains, range);
+    }
+
     /**
      * Create a new string sort
      **/
@@ -414,7 +425,7 @@ public class Context implements AutoCloseable {
      * that is passed in as argument is updated with value v,
      * the remaining fields of t are unchanged.
      **/
-    public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) 
+    public Expr mkUpdateField(FuncDecl field, Expr t, Expr v) 
         throws Z3Exception
     {
         return Expr.create (this, 
@@ -706,7 +717,7 @@ public class Context implements AutoCloseable {
     }
 
     /**
-     * Mk an expression representing {@code not(a)}.
+     * Create an expression representing {@code not(a)}.
      **/
     public BoolExpr mkNot(BoolExpr a)
     {
@@ -1679,6 +1690,28 @@ public class Context implements AutoCloseable {
                         i.getNativeObject()));
     }
 
+    /**
+     * Array read.
+     * Remarks:  The argument {@code a} is the array and
+     * {@code args} are the indices of the array that gets read.
+     * 
+     * The node {@code a} must have an array sort
+     * {@code [domains -> range]}, and {@code args} must have the sorts
+     * {@code domains}. The sort of the result is {@code range}.
+     * 
+     * @see #mkArraySort
+     * @see #mkStore
+
+     **/
+    public Expr mkSelect(ArrayExpr a, Expr[] args)
+    {
+        checkContextMatch(a);
+        checkContextMatch(args);
+        return Expr.create(
+                this,
+                Native.mkSelectN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args)));
+    }
+
     /**
      * Array update.
      * Remarks:  The node {@code a} must have an array sort
@@ -1704,6 +1737,31 @@ public class Context implements AutoCloseable {
                 i.getNativeObject(), v.getNativeObject()));
     }
 
+    /**
+     * Array update.
+     * Remarks:  The node {@code a} must have an array sort
+     * {@code [domains -> range]}, {@code i} must have sort
+     * {@code domain}, {@code v} must have sort range. The sort of the
+     * result is {@code [domains -> range]}. The semantics of this function
+     * is given by the theory of arrays described in the SMT-LIB standard. See
+     * http://smtlib.org for more details. The result of this function is an
+     * array that is equal to {@code a} (with respect to
+     * {@code select}) on all indices except for {@code args}, where it
+     * maps to {@code v} (and the {@code select} of {@code a}
+     * with respect to {@code args} may be a different value). 
+     * @see #mkArraySort
+     * @see #mkSelect
+
+     **/
+    public ArrayExpr mkStore(ArrayExpr a, Expr[] args, Expr v)
+    {
+        checkContextMatch(a);
+        checkContextMatch(args);
+        checkContextMatch(v);
+        return new ArrayExpr(this, Native.mkStoreN(nCtx(), a.getNativeObject(),
+                             args.length, AST.arrayToNative(args), v.getNativeObject()));
+    }
+
     /**
      * Create a constant array.
      * Remarks:  The resulting term is an array, such
@@ -2104,7 +2162,7 @@ public class Context implements AutoCloseable {
     /**
      * Create a range expression.
      */
-    public ReExpr MkRange(SeqExpr lo, SeqExpr hi) 
+    public ReExpr mkRange(SeqExpr lo, SeqExpr hi) 
     {
         checkContextMatch(lo, hi);
         return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));

src/api/z3_api.h

@@ -1881,6 +1881,17 @@ extern "C" {
     */
     Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range);
 
+    /**
+       \brief Create an array type with N arguments
+
+       \sa Z3_mk_select_n
+       \sa Z3_mk_store_n
+
+       def_API('Z3_mk_array_sort_n', SORT, (_in(CONTEXT), _in(UINT), _in_array(1, SORT), _in(SORT)))
+    */
+    Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const * domain, Z3_sort range);
+
+
     /**
        \brief Create a tuple type.
 
@@ -2973,6 +2984,15 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i);
 
+    /**
+       \brief n-ary Array read.
+       The argument \c a is the array and \c idxs are the indices of the array that gets read.
+
+       def_API('Z3_mk_select_n', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
+
+    */
+    Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs);
+
     /**
        \brief Array update.
 
@@ -2991,6 +3011,14 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v);
 
+    /**
+       \brief n-ary Array update.
+
+       def_API('Z3_mk_store_n', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST), _in(AST)))
+
+    */
+    Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs, Z3_ast v);
+
     /**
         \brief Create the constant array.
 
@@ -3031,6 +3059,15 @@ extern "C" {
         def_API('Z3_mk_array_default', AST, (_in(CONTEXT), _in(AST)))
     */
     Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array);
+
+    /**
+       \brief Create array with the same interpretation as a function.
+       The array satisfies the property (f x) = (select (_ as-array f) x) 
+       for every argument x.
+
+       def_API('Z3_mk_as_array', AST, (_in(CONTEXT), _in(FUNC_DECL)))
+     */
+    Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f);
     /*@}*/
 
     /** @name Sets */
@@ -3854,6 +3891,7 @@ extern "C" {
 
     /**
        \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.
 
        \pre Z3_get_sort_kind(c, t) == Z3_ARRAY_SORT
 

src/ast/array_decl_plugin.cpp

@@ -242,7 +242,9 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
     parameter const* parameters = s->get_parameters();
  
     if (num_parameters != arity) {
-        m_manager->raise_exception("select requires as many arguments as the size of the domain");
+        std::stringstream strm;
+        strm << "select requires " << num_parameters << " arguments, but was provided with " << arity << " arguments";
+        m_manager->raise_exception(strm.str().c_str());
         return 0;
     }
     ptr_buffer<sort> new_domain; // we need this because of coercions.
@@ -314,7 +316,7 @@ func_decl * array_decl_plugin::mk_array_ext(unsigned arity, sort * const * domai
         return 0;
     }
     sort * r = to_sort(s->get_parameter(i).get_ast());
-    parameter param(s);
+    parameter param(i);
     return m_manager->mk_func_decl(m_array_ext_sym, arity, domain, r, func_decl_info(m_family_id, OP_ARRAY_EXT, 1, &param));
 }
 
@@ -592,3 +594,9 @@ sort * array_util::mk_array_sort(unsigned arity, sort* const* domain, sort* rang
     params.push_back(parameter(range));
     return m_manager.mk_sort(m_fid, ARRAY_SORT, params.size(), params.c_ptr());
 }
+
+func_decl* array_util::mk_array_ext(sort *domain, unsigned i) {    
+    sort * domains[2] = { domain, domain };
+    parameter p(i);
+    return m_manager.mk_func_decl(m_fid, OP_ARRAY_EXT, 1, &p, 2, domains);
+}

src/ast/array_decl_plugin.h

@@ -143,6 +143,7 @@ public:
     bool is_const(expr* n) const { return is_app_of(n, m_fid, OP_CONST_ARRAY); }
     bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); }
     bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
+    bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); }
     bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); }
     bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); }
     bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
@@ -182,12 +183,15 @@ public:
         return mk_const_array(s, m_manager.mk_true());
     }
 
+    func_decl * mk_array_ext(sort* domain, unsigned i);
+
     sort * mk_array_sort(sort* dom, sort* range) { return mk_array_sort(1, &dom, range); }
 
     sort * mk_array_sort(unsigned arity, sort* const* domain, sort* range);
 
-    app * mk_as_array(sort * s, func_decl * f) {
+    app * mk_as_array(func_decl * f) {
         parameter param(f);
+        sort * s = f->get_range();
         return m_manager.mk_app(m_fid, OP_AS_ARRAY, 1, &param, 0, 0, s);
     }
 };

src/ast/fpa/bv2fpa_converter.cpp

@@ -250,7 +250,7 @@ bv2fpa_converter::array_model bv2fpa_converter::convert_array_func_interp(model_
     am.new_float_fd = m.mk_fresh_func_decl(arity, array_domain.c_ptr(), rng);
     am.new_float_fi = convert_func_interp(mc, am.new_float_fd, bv_f);
     am.bv_fd = bv_f;
-    am.result = arr_util.mk_as_array(f->get_range(), am.new_float_fd);
+    am.result = arr_util.mk_as_array(am.new_float_fd);
     return am;
 }
 

src/smt/theory_array.cpp

@@ -53,18 +53,12 @@ namespace smt {
         var_data * d2 = m_var_data[v2];
         if (!d1->m_prop_upward && d2->m_prop_upward)
             set_prop_upward(v1);
-        ptr_vector<enode>::iterator it   = d2->m_stores.begin();
+        for (enode* n : d2->m_stores) 
-        ptr_vector<enode>::iterator end  = d2->m_stores.end();
+            add_store(v1, n);
-        for (; it != end; ++it) 
+        for (enode* n : d2->m_parent_stores) 
-            add_store(v1, *it);
+            add_parent_store(v1, n);
-        it  = d2->m_parent_stores.begin();
+        for (enode* n : d2->m_parent_selects) 
-        end = d2->m_parent_stores.end();
+            add_parent_select(v1, n);
-        for (; it != end; ++it)
-            add_parent_store(v1, *it);
-        it  = d2->m_parent_selects.begin();
-        end = d2->m_parent_selects.end();
-        for (; it != end; ++it)
-            add_parent_select(v1, *it);
         TRACE("array", tout << "after merge\n"; display_var(tout, v1););
     }
 
@@ -103,16 +97,11 @@ namespace smt {
         d->m_parent_selects.push_back(s);
         TRACE("array", tout << mk_pp(s->get_owner(), get_manager()) << " " << mk_pp(get_enode(v)->get_owner(), get_manager()) << "\n";);
         m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_selects));
-        ptr_vector<enode>::iterator it  = d->m_stores.begin();
+        for (enode* n : d->m_stores) {
-        ptr_vector<enode>::iterator end = d->m_stores.end();
+            instantiate_axiom2a(s, n);
-        for (; it != end; ++it) {
-            instantiate_axiom2a(s, *it);
         }
         if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
-            it  = d->m_parent_stores.begin();
+            for (enode* store : d->m_parent_stores) {
-            end = d->m_parent_stores.end();
-            for (; it != end; ++it) {
-                enode * store = *it;
                 SASSERT(is_store(store));
                 if (!m_params.m_array_cg || store->is_cgr()) {
                     instantiate_axiom2b(s, store);
@@ -129,27 +118,19 @@ namespace smt {
         var_data * d     = m_var_data[v];
         d->m_parent_stores.push_back(s);
         m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_stores));
-        if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
+        if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) 
-            ptr_vector<enode>::iterator it  = d->m_parent_selects.begin();
+            for (enode* n : d->m_parent_selects) 
-            ptr_vector<enode>::iterator end = d->m_parent_selects.end();
+                if (!m_params.m_array_cg || n->is_cgr())
-            for (; it != end; ++it) 
+                    instantiate_axiom2b(n, s);
-                if (!m_params.m_array_cg || (*it)->is_cgr())
-                    instantiate_axiom2b(*it, s);
-        }
     }
 
     bool theory_array::instantiate_axiom2b_for(theory_var v) {
         bool result = false;
         var_data * d = m_var_data[v];
-        ptr_vector<enode>::iterator it  = d->m_parent_stores.begin();
+        for (enode* n1 : d->m_parent_stores) 
-        ptr_vector<enode>::iterator end = d->m_parent_stores.end();
+            for (enode * n2 : d->m_parent_selects) 
-        for (; it != end; ++it) {
+                if (instantiate_axiom2b(n2, n1))
-            ptr_vector<enode>::iterator it2  = d->m_parent_selects.begin();
-            ptr_vector<enode>::iterator end2 = d->m_parent_selects.end();
-            for (; it2 != end2; ++it2) 
-                if (instantiate_axiom2b(*it2, *it))
                     result = true;
-        }
         return result;
     }
 
@@ -167,10 +148,8 @@ namespace smt {
             d->m_prop_upward = true;
             if (!m_params.m_array_delay_exp_axiom)
                 instantiate_axiom2b_for(v);
-            ptr_vector<enode>::iterator it  = d->m_stores.begin();
+            for (enode * n : d->m_stores) 
-            ptr_vector<enode>::iterator end = d->m_stores.end();
+                set_prop_upward(n);
-            for (; it != end; ++it)
-                set_prop_upward(*it);
         }
     }
 
@@ -209,11 +188,9 @@ namespace smt {
         }
         d->m_stores.push_back(s);
         m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_stores));
-        ptr_vector<enode>::iterator it  = d->m_parent_selects.begin();
+        for (enode * n : d->m_parent_selects) {
-        ptr_vector<enode>::iterator end = d->m_parent_selects.end();
+            SASSERT(is_select(n));
-        for (; it != end; ++it) {
+            instantiate_axiom2a(n, s);
-            SASSERT(is_select(*it));
-            instantiate_axiom2a(*it, s);
         }
         if (m_params.m_array_always_prop_upward || lambda_equiv_class_size >= 1) 
             set_prop_upward(s);
@@ -374,7 +351,7 @@ namespace smt {
     
     final_check_status theory_array::final_check_eh() {
         m_final_check_idx++;
-        final_check_status r;
+        final_check_status r = FC_DONE;
         if (m_params.m_array_lazy_ieq) {
             // Delay the creation of interface equalities...  The
             // motivation is too give other theories and quantifier

src/smt/theory_array_base.cpp

@@ -210,17 +210,16 @@ namespace smt {
 
 
 
-
     func_decl_ref_vector * theory_array_base::register_sort(sort * s_array) {
         unsigned dimension = get_dimension(s_array);
         func_decl_ref_vector * ext_skolems = 0;
         if (!m_sort2skolem.find(s_array, ext_skolems)) {       
+            array_util util(get_manager());
             ast_manager & m = get_manager();
             ext_skolems = alloc(func_decl_ref_vector, m);
             for (unsigned i = 0; i < dimension; ++i) {
                 sort * ext_sk_domain[2] = { s_array, s_array };
-                parameter p(i);
+                func_decl * ext_sk_decl = util.mk_array_ext(s_array, i);
-                func_decl * ext_sk_decl = m.mk_func_decl(get_id(), OP_ARRAY_EXT, 1, &p, 2, ext_sk_domain);
                 ext_skolems->push_back(ext_sk_decl);
             }
             m_sort2skolem.insert(s_array, ext_skolems);

src/tactic/bv/bvarray2uf_rewriter.cpp

@@ -117,7 +117,7 @@ func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) {
             if (is_uninterp_const(e)) {
                 if (m_emc)
                     m_emc->insert(to_app(e)->get_decl(),
-                                  m_array_util.mk_as_array(m_manager.get_sort(e), bv_f));
+                                  m_array_util.mk_as_array(bv_f));
             }
             else if (m_fmc)
                 m_fmc->insert(bv_f);
@@ -193,7 +193,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
             if (is_uninterp_const(e)) {
                 if (m_emc)
                     m_emc->insert(e->get_decl(),
-                        m_array_util.mk_as_array(m_manager.get_sort(e), bv_f));
+                        m_array_util.mk_as_array(bv_f));
             }
             else if (m_fmc)
                 m_fmc->insert(bv_f);
@@ -207,7 +207,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
         q = m_manager.mk_forall(1, sorts, names, body);
         extra_assertions.push_back(q);
 
-        result = m_array_util.mk_as_array(f->get_range(), bv_f);
+        result = m_array_util.mk_as_array(bv_f);
 
         TRACE("bvarray2uf_rw", tout << "result: " << mk_ismt2_pp(result, m_manager) << ")" << std::endl;);
         res = BR_DONE;
@@ -234,7 +234,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
         if (is_bv_array(t)) {
             // From [1]: For every array term t we create a fresh uninterpreted function f_t.
             f_t = mk_uf_for_array(t);
-            result = m_array_util.mk_as_array(m_manager.get_sort(t), f_t);
+            result = m_array_util.mk_as_array(f_t);
             res = BR_DONE;
         }
         else if (has_bv_arrays) {
@@ -274,7 +274,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
                     expr * v = args[0];
                     func_decl_ref f_t(mk_uf_for_array(t), m_manager);
 
-                    result = m_array_util.mk_as_array(f->get_range(), f_t);
+                    result = m_array_util.mk_as_array(f_t);
                     res = BR_DONE;
 
                     // Add \forall x . f_t(x) = v
@@ -321,7 +321,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
                     expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager);
                     extra_assertions.push_back(frllx);
 
-                    result = m_array_util.mk_as_array(f->get_range(), f_t);
+                    result = m_array_util.mk_as_array(f_t);
                     res = BR_DONE;
                 }
                 else if (m_array_util.is_store(f)) {
@@ -342,7 +342,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
                         func_decl_ref f_s(mk_uf_for_array(s), m_manager);
                         func_decl_ref f_t(mk_uf_for_array(t), m_manager);
 
-                        result = m_array_util.mk_as_array(f->get_range(), f_t);
+                        result = m_array_util.mk_as_array(f_t);
                         res = BR_DONE;
 
                         sort * sorts[1] = { get_index_sort(f->get_range()) };