Python中使用Z3构造元组类型列表触发访问器校验错误的问题排查

• 核心问题是对Z3 Python API中TupleSort的返回值结构存在误解：调用TupleSort("IntPair", [IntSort(), IntSort()])时，返回值并非单独的二元组类型Sort对象，而是由(二元组Sort实例, 左分量访问函数, 右分量访问函数)组成的三元组。
• 声明列表构造子的head访问器时，你直接将整个三元组IntPair传入参数位。Z3校验访问器时要求该位置必须是Sort或Datatype类型，收到非预期的普通元组后，就会抛出“访问器格式不合法”的异常。
• 整数元素列表可正常运行的原因很简单：IntSort()本身就是独立的Sort实例，不存在返回多值元组的行为，作为访问器参数时可通过类型校验。

• 首先解构TupleSort的返回值，提取真正的二元组Sort实例，作为列表head字段的合法类型。
• 列表的递归定义流程保持原有写法即可，无需调整Datatype的构建逻辑。

可直接运行的修正代码：

from z3 import *

# 解构TupleSort返回的三元组，提取合法的二元组类型Sort
IntPairSort, get_edge_src, get_edge_dst = TupleSort("IntPair", [IntSort(), IntSort()])

List = Datatype('List')
# head字段使用解构得到的Sort实例
List.declare('list', ('head', IntPairSort), ('tail', List))
List.declare('empty')
List = List.create()

基于修正后的类型，即可实现图合法路径判定的path谓词：通过递归约束相邻列表元素的关系，即前一个二元组的终点与后一个二元组的起点一致、所有二元组代表的边属于给定图G的边集，就能完成合法性校验。

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