在 Z3 中构建 python 元组列表

Question

我正在尝试在 python 中使用 Z3 求解器来创建谓词 path(list) 如果 list 是给定图上的有效路径，则 returns 为真 G

我想使用 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: Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)

来自这一行：

List.declare('list', ('head', IntPair), ('tail', List))

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

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

以上将运行没有错误。

谢谢。

Answer 1

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

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

与：

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

现在IntPair就是你想要的那种的名字；你的程序的其余部分将不会出现任何错误。

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

在 Z3 中构建 python 元组列表

Build in Z3 python a list of tuples

python

z3

smt

z3py