python - z3 の Python API でビットベクトルの配列を実装する方法

Question

私は z3py を初めて使用し、Python で Z3 API を使用していましたが、ビットベクトルの配列を定義する方法がわかりませんでした。

私は次のようなものが欲しい：

DOT__mem[16] = BitVec('DOT__mem[16]', 8)

しかし、チュートリアルの演習パネルでも、この構文は機能しませんでした。

誰かが正しい構文を手伝ってくれますか?

Answer 1

次の例は、Z3 ビット ベクトルの「ベクトル」(Python リスト) を作成する方法を示しています。この例は、rise4funでオンラインでも入手できます。

# Create a Bitvector of size 8
a = BitVec('a', 8)

# Create a "vector" (list) with 16 Bit-vectors of size 8
DomVect = [ BitVec('DomVect_%s' % i, 8) for i in range(16) ]
print DomVect
print DomVect[15]

def BitVecVector(prefix, sz, N):
  """Create a vector with N Bit-Vectors of size sz"""
  return [ BitVec('%s__%s' % (prefix, i), sz) for i in range(N) ]

# The function BitVecVector is similar to the functions IntVector and RealVector in Z3Py.

# Create a vector with 32 Bit-vectors of size 8. 
print BitVecVector("A", 8, 32)