Z3py：特定整数类型的数组？

Question

在Z3Bython中，我要声明一个字节数组（这意味着数组的每个成员都是8位的整数）。我尝试了以下代码，但很明显它报告Int（8）是非法类型。

你知道如何解决这个问题吗？谢谢！

I = IntSort()
I8 = Int(8)
A = Array('A', I, I8)

Answer 1

不能提供数字作为Int（）函数的参数。它需要一个字符串（实际上是整数的名称），而不是整数的大小（以位为单位）。您可能需要考虑改用位向量：

Byte = BitVecSort(8)
i8 = BitVec('i8', Byte)
A = Array('A', IntSort(), Byte)