From 36cceee4547bf00fc56cf62c1a3b866a762afb85 Mon Sep 17 00:00:00 2001 From: Walden Yan Date: Sat, 31 Dec 2022 23:00:12 -0500 Subject: [PATCH 1/2] fix: making array select work for lambda expressions --- src/api/python/z3/z3.py | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 695bb939f0..390b2aacf8 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -4597,10 +4597,16 @@ def default(self): def _array_select(ar, arg): if isinstance(arg, tuple): - args = [ar.domain_n(i).cast(arg[i]) for i in range(len(arg))] + if isinstance(ar, QuantifierRef): + args = [ar.var_sort(i).cast(arg[i]) for i in range(len(arg))] + else: + args = [ar.domain_n(i).cast(arg[i]) for i in range(len(arg))] _args, sz = _to_ast_array(args) return _to_expr_ref(Z3_mk_select_n(ar.ctx_ref(), ar.as_ast(), sz, _args), ar.ctx) - arg = ar.domain().cast(arg) + if isinstance(ar, QuantifierRef): + arg = ar.var_sort(0).cast(arg) + else: + arg = ar.domain().cast(arg) return _to_expr_ref(Z3_mk_select(ar.ctx_ref(), ar.as_ast(), arg.as_ast()), ar.ctx) From e7c87cde5d990038bb9b42b87be19b4fb50fe956 Mon Sep 17 00:00:00 2001 From: Walden Yan Date: Sat, 31 Dec 2022 23:07:33 -0500 Subject: [PATCH 2/2] more elegant solution --- src/api/python/z3/z3.py | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 390b2aacf8..074570b035 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -4597,16 +4597,10 @@ def default(self): def _array_select(ar, arg): if isinstance(arg, tuple): - if isinstance(ar, QuantifierRef): - args = [ar.var_sort(i).cast(arg[i]) for i in range(len(arg))] - else: - args = [ar.domain_n(i).cast(arg[i]) for i in range(len(arg))] + args = [ar.sort().domain_n(i).cast(arg[i]) for i in range(len(arg))] _args, sz = _to_ast_array(args) return _to_expr_ref(Z3_mk_select_n(ar.ctx_ref(), ar.as_ast(), sz, _args), ar.ctx) - if isinstance(ar, QuantifierRef): - arg = ar.var_sort(0).cast(arg) - else: - arg = ar.domain().cast(arg) + arg = ar.sort().domain().cast(arg) return _to_expr_ref(Z3_mk_select(ar.ctx_ref(), ar.as_ast(), arg.as_ast()), ar.ctx)