How to implement array of bitvectors in z3's Python APIs

Question

I am new to z3py and was going through the Z3 API in Python, but couldn't figure out how to define an array of bitvectors.

I want something like:

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

but this syntax didn't work, even on the practice panel in the tutorial.

Can someone help with the correct syntax?

Answer 1

The following examples illustrate how to create a "vector" (Python list) of Z3 Bit-Vectors. The example is also available online at 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)