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

【问题标题】：Z3: Should I use Arrays, IntVectors, or something else?Z3：我应该使用 Arrays、IntVectors 还是其他东西？
【发布时间】：2018-09-24 19:40:12
【问题描述】：

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

我认为数组过于矫枉过正的原因：每个数组元素只写一次，我没有像Store((Store(X, y, z1)), y, z2) 那样做任何事情。此外，每个数组的预定义长度为

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

有没有一种方法可以在不必使用昂贵的数组操作的情况下获得变量索引的强大功能？

【问题讨论】：

标签： z3 smt z3py

【解决方案1】：

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

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

【讨论】：