1

Z3Pythonで、バイトの配列を宣言したいと思います（つまり、配列の各メンバーは8ビットの整数です）。次のコードで試しましたが、Int（8）が不正な型であると報告されているようです。

問題を解決する方法について何かアイデアはありますか？ありがとう！

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

1 に答える 1

2

Int（）関数の引数として数値を指定することはできません。文字列（実際には整数の名前）を想定しており、整数のサイズ（ビット単位）は想定していません。代わりにビットベクトルの使用を検討することをお勧めします。

Byte = BitVecSort(8)
i8 = BitVec('i8', Byte)
A = Array('A', IntSort(), Byte)
于 2013-03-11T12:45:55.923 に答える