如何在 Z3py 中定义二维数组变量

Question

我想在 Z3py 中定义一个二维布尔数组。实际上，我想使用其他整数变量访问数组索引，例如 A[x][3]，其中 x 是一个整数变量，其值由运行时的 SMT 求解器决定。

如果我按如下方式定义二维数组： A = [ [ Bool("a_%s_%s" % (i， j(( 对于范围(5( 中的 j ] 对于范围(5( 中的 i ] 然后，我在添加约束时得到"类型错误：对象不能被解释为索引"，例如 (A[x][3]==True(。

我检查了定义为 A = Array('A'，IntSort((，IntSort(((的 z3 数组，我可以使用其他整数变量(例如 A[x](访问数组索引。现在，我想要二维数组也是如此。

请在这方面帮助我。 提前谢谢。

Answer 1

您可以像这样对嵌套数组进行建模：

A  = Array('A', IntSort(), ArraySort(IntSort(), BoolSort()))

也就是说，第一个索引是一个整数，它索引到另一个从整数到布尔值的数组中。