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

Question

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

如果我将二维数组定义如下： A = [ [ Bool("a_%s_%s" % (i, j)) for j in range(5) ] for i in range(5) ] 那么，我在添加诸如 (A[x][3]==True) 之类的约束时得到“TypeError：对象不能被解释为索引”。

我检查了对于定义为 A = Array('A',IntSort(),IntSort()) 的 z3 数组，我可以使用其他整数变量（例如 A[x]）访问数组索引。现在，我希望二维数组也一样。

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

标签： pythonarraysz3py

Answer 1

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

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

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