在 Z3 python 中构建元组列表

问题描述

我试图在 python 中使用 Z3 求解器来创建一个谓词 path(list)，如果 list 是给定图 G 上的有效路径，它返回 true

我想使用 Z3 来构建一个元组列表来表示图中存在的所有边，这是我的第一次尝试：

from z3 import *

IntPair = TupleSort("IntPair",[IntSort(),IntSort()])

List = Datatype('List')
List.declare('list',('head',IntPair),('tail',List))
List.declare('empty')
List = List.create()

但是我收到一个错误：

Z3Exception：预期访问者的有效列表。访问器是一对形式 (String,Datatype|Sort)

从这一行：

List.declare('list',List))

我不确定哪个访问器违反并导致此错误。如果我们考虑一个整数列表：

List.declare('list',IntSort()),List))

上面的代码运行不会出错。

谢谢。

解决方法

当您调用 TupleSort 时，它返回一个三元组。排序、构造函数和访问器。您需要进行模式匹配并给每个单独的名称。也就是说，替换您的行：

IntPair = TupleSort("IntPair",[IntSort(),IntSort()])

与：

IntPair,mkIntPair,(first,second) = TupleSort("IntPair",IntSort()])

现在 IntPair 是您想要的排序的名称；程序的其余部分将不会出错。

随着您进一步开发程序，您需要使用 mkIntPair、first 和 second 来访问和构建列表中的这些对。

python smt z3 z3py