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

Question

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

I need something like:

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

but this syntax did not work, even in the practice panel in the tutorial.

Can anyone help with the correct syntax?

Answer 1

The following examples show how to create a “vector” (Python list) of Z3 bit vectors. An 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)