add array-ext to externally exposed functions to enable interpolants with arrays to be usable in feedback loops with Z3. Addresses one issue raised in #292

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

src/api/api_array.cpp

@@ -187,7 +187,8 @@ extern "C" {
     MK_BINARY(Z3_mk_set_difference, mk_c(c)->get_array_fid(), OP_SET_DIFFERENCE, SKIP);
     MK_UNARY(Z3_mk_set_complement, mk_c(c)->get_array_fid(), OP_SET_COMPLEMENT, SKIP);
     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_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set) {
         return Z3_mk_select(c, set, elem);
     }

src/api/api_ast.cpp

@@ -1012,6 +1012,7 @@ extern "C" {
             case OP_SET_COMPLEMENT: return Z3_OP_SET_COMPLEMENT;
             case OP_SET_SUBSET: return Z3_OP_SET_SUBSET;
             case OP_AS_ARRAY: return Z3_OP_AS_ARRAY;
+            case OP_ARRAY_EXT: return Z3_OP_ARRAY_EXT;
             default:
                 UNREACHABLE();
                 return Z3_OP_UNINTERPRETED;

src/api/dotnet/Context.cs

@@ -2122,6 +2122,21 @@ namespace Microsoft.Z3
             CheckContextMatch(array);
             return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
         }
+
+        /// <summary>
+        /// Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.
+        /// </summary>
+        public Expr MkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
+        {
+            Contract.Requires(arg1 != null);
+            Contract.Requires(arg2 != null);
+            Contract.Ensures(Contract.Result<Expr>() != null);
+
+            CheckContextMatch(arg1);
+            CheckContextMatch(arg2);
+            return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
+        }
+
         #endregion
 
         #region Sets
@@ -2268,6 +2283,7 @@ namespace Microsoft.Z3
             CheckContextMatch(arg2);
             return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
         }
+
         #endregion
 
         #region Pseudo-Boolean constraints

src/api/java/Context.java

@@ -1717,6 +1717,17 @@ public class Context extends IDisposable
                 Native.mkArrayDefault(nCtx(), array.getNativeObject()));
     }
 
+    /**
+     * Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.
+     **/
+    public Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
+    {
+	checkContextMatch(arg1);
+	checkContextMatch(arg2);
+	return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
+    }
+
+
     /**
      * Create a set type.
      **/

src/api/python/z3.py

@@ -4143,6 +4143,13 @@ def K(dom, v):
         v = _py2expr(v, ctx)
     return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
 
+def Ext(a, b):
+    """Return extensionality index for arrays.
+    """
+    if __debug__:
+	_z3_assert(is_array(a) and is_array(b))
+    return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()));
+
 def is_select(a):
     """Return `True` if `a` is a Z3 array select application.
     

src/api/python/z3printer.py

@@ -31,7 +31,7 @@ _z3_op_to_str = {
     Z3_OP_BASHR : '>>', Z3_OP_BSHL : '<<', Z3_OP_BLSHR : 'LShR', 
     Z3_OP_CONCAT : 'Concat', Z3_OP_EXTRACT : 'Extract', Z3_OP_BV2INT : 'BV2Int',
     Z3_OP_ARRAY_MAP : 'Map', Z3_OP_SELECT : 'Select', Z3_OP_STORE : 'Store', 
-    Z3_OP_CONST_ARRAY : 'K',
+    Z3_OP_CONST_ARRAY : 'K', Z3_OP_ARRAY_EXT : 'Ext', 
     Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe'
     }
 

src/api/z3_api.h

@@ -322,6 +322,9 @@ typedef enum
    - Z3_OP_AS_ARRAY An array value that behaves as the function graph of the
                     function passed as parameter.
 
+   - Z3_OP_ARRAY_EXT Array extensionality function. It takes two arrays as arguments and produces an index, such that the arrays
+                    are different if they are different on the index.
+
    - Z3_OP_BNUM Bit-vector numeral.
 
    - Z3_OP_BIT1 One bit bit-vector.
@@ -1033,6 +1036,7 @@ typedef enum {
     Z3_OP_SET_COMPLEMENT,
     Z3_OP_SET_SUBSET,
     Z3_OP_AS_ARRAY,
+    Z3_OP_ARRAY_EXT,
 
     // Bit-vectors
     Z3_OP_BNUM = 0x400,
@@ -3260,6 +3264,17 @@ END_MLAPI_EXCLUDE
     Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2);
     /*@}*/
 
+    /**
+       \brief Create array extensionality index given two arrays with the same sort. 
+              The meaning is given by the axiom:
+              (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B))
+
+       def_API('Z3_mk_array_ext', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+
+    Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2);
+    /*@}*/
+
     /**
        @name Numerals
     */

src/ast/array_decl_plugin.cpp

@@ -293,7 +293,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
                                    func_decl_info(m_family_id, OP_STORE));
 }
 
-func_decl * array_decl_plugin::mk_array_ext_skolem(unsigned arity, sort * const * domain, unsigned i) {
+func_decl * array_decl_plugin::mk_array_ext(unsigned arity, sort * const * domain, unsigned i) {
     if (arity != 2 || domain[0] != domain[1]) {
         UNREACHABLE();
         return 0;
@@ -306,7 +306,7 @@ func_decl * array_decl_plugin::mk_array_ext_skolem(unsigned arity, sort * const
     }
     sort * r = to_sort(s->get_parameter(i).get_ast());
     parameter param(s);
-    return m_manager->mk_func_decl(m_array_ext_sym, arity, domain, r, func_decl_info(m_family_id, OP_ARRAY_EXT_SKOLEM, 1, &param));
+    return m_manager->mk_func_decl(m_array_ext_sym, arity, domain, r, func_decl_info(m_family_id, OP_ARRAY_EXT, 1, &param));
 }
 
 
@@ -463,12 +463,15 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         func_decl * f = to_func_decl(parameters[0].get_ast());
         return mk_map(f, arity, domain);        
     }
-    case OP_ARRAY_EXT_SKOLEM:
+    case OP_ARRAY_EXT:
+        if (num_parameters == 0) {
+            return mk_array_ext(arity, domain, 0);
+        }
         if (num_parameters != 1 || !parameters[0].is_int()) {
             UNREACHABLE();
             return 0;
         }
-        return mk_array_ext_skolem(arity, domain, parameters[0].get_int());
+        return mk_array_ext(arity, domain, parameters[0].get_int());
     case OP_ARRAY_DEFAULT:
         return mk_default(arity, domain);
     case OP_SET_UNION:
@@ -519,7 +522,7 @@ void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
         op_names.push_back(builtin_name("complement",OP_SET_COMPLEMENT));
         op_names.push_back(builtin_name("subset",OP_SET_SUBSET));
         op_names.push_back(builtin_name("as-array", OP_AS_ARRAY));
-        //op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT_SKOLEM));
+        op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT));
     }
 }
 

src/ast/array_decl_plugin.h

@@ -42,7 +42,7 @@ enum array_op_kind {
     OP_STORE,
     OP_SELECT,
     OP_CONST_ARRAY,
-    OP_ARRAY_EXT_SKOLEM,
+    OP_ARRAY_EXT,
     OP_ARRAY_DEFAULT,
     OP_ARRAY_MAP,
     OP_SET_UNION,
@@ -80,7 +80,7 @@ class array_decl_plugin : public decl_plugin {
 
     func_decl * mk_store(unsigned arity, sort * const * domain);
 
-    func_decl * mk_array_ext_skolem(unsigned arity, sort * const * domain, unsigned i);
+    func_decl * mk_array_ext(unsigned arity, sort * const * domain, unsigned i);
 
     func_decl * mk_set_union(unsigned arity, sort * const * domain);
 

src/smt/theory_array_base.cpp

@@ -220,7 +220,7 @@ namespace smt {
             for (unsigned i = 0; i < dimension; ++i) {
                 sort * ext_sk_domain[2] = { s_array, s_array };
                 parameter p(i);
-                func_decl * ext_sk_decl = m.mk_func_decl(get_id(), OP_ARRAY_EXT_SKOLEM, 1, &p, 2, ext_sk_domain);
+                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);
@@ -310,10 +310,7 @@ namespace smt {
         func_decl_ref_vector * funcs = 0;
         sort *                     s = m.get_sort(e1);
 
-        if (!m_sort2skolem.find(s, funcs)) {
+        VERIFY(m_sort2skolem.find(s, funcs));
-            UNREACHABLE();
-            return;
-        }
 
         unsigned dimension = funcs->size();
 

src/smt/theory_array_base.h

@@ -36,7 +36,7 @@ namespace smt {
         bool is_select(app const* n) const { return n->is_app_of(get_id(), OP_SELECT); }
         bool is_default(app const* n) const { return n->is_app_of(get_id(), OP_ARRAY_DEFAULT); }
         bool is_const(app const* n) const { return n->is_app_of(get_id(), OP_CONST_ARRAY); }
-        bool is_array_ext(app const * n) const { return n->is_app_of(get_id(), OP_ARRAY_EXT_SKOLEM); }
+        bool is_array_ext(app const * n) const { return n->is_app_of(get_id(), OP_ARRAY_EXT); }
         bool is_as_array(app const * n) const { return n->is_app_of(get_id(), OP_AS_ARRAY); }
         bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); }
         bool is_array_sort(app const* n) const { return is_array_sort(get_manager().get_sort(n)); }

src/smt/theory_array_full.cpp

@@ -273,7 +273,7 @@ namespace smt {
         }
         context & ctx = get_context();
 
-        if (is_map(n)) {
+        if (is_map(n) || is_array_ext(n)) {
             for (unsigned i = 0; i < n->get_num_args(); ++i) {
                 enode* arg = ctx.get_enode(n->get_arg(i));
                 if (!is_attached_to_var(arg)) {
@@ -320,6 +320,10 @@ namespace smt {
             found_unsupported_op(n);
             instantiate_default_as_array_axiom(node);
         }
+        else if (is_array_ext(n)) {
+            SASSERT(n->get_num_args() == 2);
+            instantiate_extensionality(ctx.get_enode(n->get_arg(0)), ctx.get_enode(n->get_arg(1)));
+        }
         return true;
     }