Z3(Py)数组技术疑问：模型解读、函数实现及与序列差异

背景 #

我在Z3Py中实现了公式：Exists i::Integer s.t. (0<=i<|arr|) & (avg(arr)+t<arr[i])，用于判断数组中是否存在索引i（满足0<=i<|arr|），使得arr[i]大于数组平均值avg(arr)加阈值t。对应的Z3Py代码如下：

t = Int('t')
avg_arr = Int('avg_arr')
len_arr = Int('len_arr')

arr = Array('arr', IntSort(), IntSort())

phi_1 = And(0 <= i, i< len_arr)
phi_2 = (t+avg_arr<arr[i])

phi = Exists(i, And(phi_1, phi_2))

s = Solver()
s.add(phi)
print(s.check())
print(s.model())

该公式可满足，但每次执行会得到不同模型，例如：[avg_a = 0, t = 7718, len_arr = 1, arr = K(Int, 7719)]。

疑问解答 #

1. arr = K(Int, 7719)的含义 #

K(Int, 7719)表示常量数组：即这个数组的所有索引位置对应的取值都是7719。这里因为模型中len_arr=1，有效索引只有0，看起来像是单个元素的数组，但本质上Z3的数组是无限定义域的映射，不管索引取什么值，返回的都是7719。其中K是Z3用来标记常量数组的符号，全称是"constant array"。

2. 关联数组的avg和len函数 #

原代码中avg_arr、len_arr是独立的整数变量，和数组arr没有约束关联，因此求解器可以随意赋值。要实现真正关联数组的长度和平均值，有两种方案：

方案1：改用序列（推荐）

Z3的序列（Sequence）是有限元素集合，内置长度、求和等函数，更贴合日常对"数组"的认知：

from z3 import *

t = Int('t')
seq = Seq('seq', IntSort())
len_seq = Length(seq)
sum_seq = Sum(seq)
# 用实数类型避免整数除法精度问题
avg_seq = ToReal(sum_seq) / ToReal(len_seq)

s = Solver()
# 约束序列长度至少为1，避免除以0
s.add(len_seq >= 1)
# 断言存在符合条件的索引
s.add(Exists(i, And(0 <= i, i < len_seq, seq[i] > avg_seq + ToReal(t))))

print(s.check())
print(s.model())

方案2：用数组显式约束

Z3的数组是无限映射，需要手动约束有效索引范围和总和：

from z3 import *

t = Int('t')
len_arr = Int('len_arr')
arr = Array('arr', IntSort(), IntSort())
sum_arr = Int('sum_arr')
avg_arr = ToReal(sum_arr) / ToReal(len_arr)

s = Solver()
# 约束长度至少为1
s.add(len_arr >= 1)
# 用量化断言总和为有效索引元素的和
s.add(ForAll(k, Implies(And(0 <= k, k < len_arr), sum_arr == sum_arr + arr[k])))
# 断言存在符合条件的索引
s.add(Exists(i, And(0 <= i, i < len_arr, arr[i] > avg_arr + ToReal(t))))

print(s.check())
print(s.model())

这种方式较为繁琐，因为数组没有内置的长度和求和能力，需要手动通过量化约束模拟。

3. 模型中没有索引i的原因 #

i是被Exists（存在量词）绑定的局部变量，Z3的模型只会输出自由变量（即未被量词约束的变量，比如t、avg_arr、len_arr、arr）。求解器只需要证明存在这样的i即可，不需要在模型中给出具体的i值。如果需要获取具体的i，可以将Exists替换为引入自由变量i，再添加对应约束求解。

Z3Py数组与序列的差异 #

• 数组：属于无限定义域的映射（全函数），没有内置长度概念，所有索引（包括超出定义的"有效范围"）都有对应值。适合表示内存、寄存器这类无限或固定大小的映射场景。
• 序列：属于有限元素的有序集合，内置Length()、Sum()、Concat()等操作函数，索引访问仅对有效范围（0到长度-1）有效。更符合日常开发中对"数组/列表"的认知，适合处理有限元素的集合操作。

内容的提问来源于stack exchange，提问作者Theo Deep