如何在Z3Py中将任意维度列表转换为Array类型？

问题本质 #

Python原生列表是静态结构，只能用整数索引，而Z3量词里的变量是ArithRef类型的符号值，直接用它索引列表会抛出TypeError。要支持符号索引，必须把列表转换成Z3的嵌套Array类型——Z3没有原生多维Array，而是用“元素为Array的Array”实现多维结构。

通用递归转换函数 #

写一个递归函数，自动识别列表的维度和各维度长度，把Python列表逐层转换成Z3嵌套Array：

from z3 import *

def list_to_z3_array(data, sort=IntSort()):
    # 基础情况：当前元素是数值，返回Z3常量
    if not isinstance(data, list):
        return sort(data)
    
    # 递归处理内层，得到内层的Array类型
    inner_array = list_to_z3_array(data[0], sort)
    inner_sort = inner_array.sort()
    
    # 外层Array的索引类型是IntSort()，元素类型是内层Array的类型
    outer_sort = ArraySort(IntSort(), inner_sort)
    result = K(outer_sort, inner_array)  # 初始化外层Array，默认值为第一个内层元素的结构
    
    # 遍历每个内层元素，用Store更新外层Array
    for idx, item in enumerate(data):
        converted_item = list_to_z3_array(item, sort)
        result = Store(result, idx, converted_item)
    
    return result

二维列表示例（对应用户场景） #

比如定义二维列表VG，转成Z3 Array后添加量词约束：

# 示例二维列表：9行3列
VG = [
    [1, 2, 3],
    [4, 5, 6],
    [7, 8, 9],
    [0, -1, 2],
    [3, 4, -5],
    [6, 7, 8],
    [9, 0, 1],
    [2, 3, 4],
    [5, 6, 7]
]

# 转换为Z3嵌套Array
A = list_to_z3_array(VG)

# 创建求解器和量词变量
s = Solver()
i, j = Ints('i j')

# 添加约束：所有合法索引位置的元素>=0
s.add(ForAll([i, j], 
             Implies(And(i >= 0, i < 9, j >= 0, j < 3), 
                     Select(Select(A, i), j) >= 0)))

# 检查约束是否可满足
print(s.check())  # 输出unsat，因为VG里有-1、-5
print(s.model())

注意：Z3中访问多维Array需要嵌套使用Select，比如Select(Select(A, i), j)等价于Python里的A[i][j]。

三维列表示例（验证通用性） #

再用三维列表测试，函数会自动处理嵌套结构：

# 三维列表：2x2x2
three_d_list = [
    [[1, 2], [3, 4]],
    [[5, 6], [7, 8]]
]

three_d_array = list_to_z3_array(three_d_list)
x, y, z = Ints('x y z')

# 添加约束：所有元素>0
s = Solver()
s.add(ForAll([x, y, z],
             Implies(And(x >=0, x<2, y>=0, y<2, z>=0, z<2),
                     Select(Select(Select(three_d_array, x), y), z) > 0)))
print(s.check())  # 输出sat

关键细节说明 #

• 函数自动推导维度：递归判断每个元素是否为列表，直到遇到基础数值，逐层构建嵌套Array。
• 默认用IntSort()，如果需要实数可以传入sort=RealSort()。
• 初始化用K函数创建默认值的Array，再用Store逐个替换索引位置的元素，保证所有索引都被正确赋值。

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