我想知道我应该为我的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和阅读之后，我的理解是向量不支持这一点。
有没有办法可以获得变量索引的功能，而无需使用昂贵的数组操作？
如果你有一个固定长度的小数组，没有符号索引访问，那么我强烈建议使用IntVector（参见https://z3prover.github.io/api/html/namespacez3py.html#a7e166f891df8f17fd23290bec963b03c）
请注意，重要的是您是否需要使用符号索引进行访问。 （也就是说，你总是使用已知的常量索引来处理你的数组，或者你是否需要能够读取/写入符号寻址的位置。）从你的描述中，你似乎总是静态地知道地址，所以IntVector是你最好的选择。如果地址可以是符号，那么你必须使用更好的旧SMTLib数组。