From 4685a5f8bac97dcb600761fc2844fd4fc6fb2221 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Nov 2015 16:42:13 -0800 Subject: [PATCH] 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 --- src/api/api_array.cpp | 3 ++- src/api/api_ast.cpp | 1 + src/api/dotnet/Context.cs | 16 ++++++++++++++++ src/api/java/Context.java | 11 +++++++++++ src/api/python/z3.py | 7 +++++++ src/api/python/z3printer.py | 2 +- src/api/z3_api.h | 15 +++++++++++++++ src/ast/array_decl_plugin.cpp | 13 ++++++++----- src/ast/array_decl_plugin.h | 4 ++-- src/smt/theory_array_base.cpp | 7 ++----- src/smt/theory_array_base.h | 2 +- src/smt/theory_array_full.cpp | 6 +++++- 12 files changed, 71 insertions(+), 16 deletions(-) diff --git a/src/api/api_array.cpp b/src/api/api_array.cpp index de4d6f4e6..d3dda5d9d 100644 --- a/src/api/api_array.cpp +++ b/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); } diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 15a9f5bae..200b483cf 100644 --- a/src/api/api_ast.cpp +++ b/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; diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index b179d44a5..25c399d68 100644 --- a/src/api/dotnet/Context.cs +++ b/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)); } + + /// + /// 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) + { + Contract.Requires(arg1 != null); + Contract.Requires(arg2 != null); + Contract.Ensures(Contract.Result() != 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 diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 4497e6970..0f9a85799 100644 --- a/src/api/java/Context.java +++ b/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. **/ diff --git a/src/api/python/z3.py b/src/api/python/z3.py index acee87f54..837443e07 100644 --- a/src/api/python/z3.py +++ b/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. diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py index e8a6b992f..5116046dd 100644 --- a/src/api/python/z3printer.py +++ b/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' } diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9887cd7f0..927aad930 100644 --- a/src/api/z3_api.h +++ b/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 */ diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 0e315c38d..49b1b18c5 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/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, ¶m)); + return m_manager->mk_func_decl(m_array_ext_sym, arity, domain, r, func_decl_info(m_family_id, OP_ARRAY_EXT, 1, ¶m)); } @@ -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& 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)); } } diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 98fd563f0..778b94c33 100644 --- a/src/ast/array_decl_plugin.h +++ b/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); diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 663816a7d..29e4438c4 100644 --- a/src/smt/theory_array_base.cpp +++ b/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)) { - UNREACHABLE(); - return; - } + VERIFY(m_sort2skolem.find(s, funcs)); unsigned dimension = funcs->size(); diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index 03d180f8c..46cd60fd6 100644 --- a/src/smt/theory_array_base.h +++ b/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)); } diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 013c3c188..a9dc657dd 100644 --- a/src/smt/theory_array_full.cpp +++ b/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; }