在 Z3 python 中构建一个元组列表答案

【问题标题】：Build in Z3 python a list of tuples在 Z3 python 中构建一个元组列表
【发布时间】：2021-06-26 03:45:57
【问题描述】：

我正在尝试在 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', ('head', IntPair), ('tail', List))

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

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

上面将运行没有错误。

谢谢。

【问题讨论】：

IntPair的定义是什么？
@ChristophWintersteiger 道歉，IntPairSort 应该是 IntPair

标签： python z3 smt z3py

【解决方案1】：

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

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

与：

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

现在IntPair 是您想要的类型的名称；并且您的程序的其余部分将不会出现任何错误。

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

【讨论】：