z3 - Z3：我应该使用 Arrays、IntVectors 还是其他东西？

Question

我想知道我应该为我的 z3 应用程序使用什么数据类型。我的理解是，类似整数数组的数据结构的唯一选择是 Array(IntSort()、IntSort()) 和 IntVector()。

我认为数组过于矫枉过正的原因：每个数组元素只写一次，我没有做任何类似Store((Store(X, y, z1)), y, z2). 此外，每个数组的预定义长度为 <= 256（并且数组中的每个整数都在 0 到 63 之间）。

我认为 BitVectors 不起作用的原因：我想使用 Int 变量来索引数组。例如，我可能有z = Int('z')，一些约束 z 的子句，然后Or(arr[z] == 2, arr[z + 1] == 2)。在玩弄 z3 并阅读之后，我的理解是向量不支持这一点。

有没有一种方法可以让我获得变量索引的强大功能，而无需使用昂贵的数组操作？

标签： z3smtz3py

Answer 1

如果您有固定长度的小型数组而没有符号索引访问，那么我强烈建议您使用IntVector（参见https://z3prover.github.io/api/html/namespacez3py.html#a7e166f891df8f17fd23290bec963b03c）

请注意，这里重要的是您是否需要使用符号索引进行访问。（也就是说，您是否总是使用已知的常量索引来寻址您的数组，或者您是否需要读取/写入符号寻址位置的能力。）根据您的描述，您似乎总是静态地知道地址，所以IntVector是您的最佳选择. 如果地址可以是符号的，那么您必须使用旧的 SMTLib 数组，这更昂贵。