Z3py : 특정 정수 유형의 배열?

Question

Z3 파이썬에서 바이트의 배열을 선언하고자합니다. 배열의 각 구성원은 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)