如何使用列表值作为 Z3py 中的字典索引答案

【问题标题】：How to use list value as the dictionary indices in Z3py如何使用列表值作为 Z3py 中的字典索引
【发布时间】：2020-12-22 08:37:24
【问题描述】：

我有一个带有 j 个整数元素的 python 数组 (Arr)、一个值为 z3 Int 变量的 Z3 列表 (X) 和一个值为 Z3 Bool 变量的 Z3 字典 (D)。

例如：

X = [ [ x_0_0, x_0_1, ..., x_0_j], [ x_1_0, x_1_1, ..., x_1_j], … [ x_i_0, x_i_1, ..., x_i_j] ] X[0] = Arr /* Arr 是 python 整数数组 */ D = { (x, i, j): D_x_i_j } 对于所有 i 和 j，其中 x 是 X[i][j] 位置的值。

X[i₁][j] 的剩余值由求解器根据 D 值决定，即真/假，其中 11子>

现在这些解出的 X 值是 D 字典的键值。

因此，我想将这些值用作字典的键索引。

我的问题是如何使用 Z3 列表值作为 Z3 字典的键值或作为另一个 z3 列表的索引？

【问题讨论】：

您需要展示更多代码。本质上，您想查询求解器以获取 X 的值（使用 s.model()），然后将其转换为索引（很可能使用 .as_long()），然后将其用作常规索引。但是如果没有看到更多的代码，就很难说更具体的了。如果您可以发布一个人们可以运行的最小示例来展示您遇到的问题，那么 Stack-overflow 效果最好。

标签： python arrays list dictionary z3

【解决方案1】：

您可以将列表转换为tuple。 Tuples 是可散列的，因此是有效的字典键。

d = {(x, i, j): D_x_i_j}
X[0] = Arr                # [x, i, j]
key = tuple(X[0])
print(d[key])             # yields D_x_i_j

【讨论】：