python - z3中一定大小的数组

Question

我正在将 z3py 库用于程序验证项目，并希望对 z3 中数组的访问进行编码。有没有一种简单的方法可以使 Array z3type 具有一定的大小，例如 112 个条目？我在想类似的东西： A = Array('A', IntSort(), size)

谢谢，

Answer 1

如果你想要一个包含 112 个整数元素的数组，你应该将它声明为

A = IntVector('A', 112)