Z3py: массив определенного целочисленного типа?

Question

В Z3Python я хочу объявить массив байтов (что означает, что каждый член массива имеет целое число из 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)