如何在z3的Python API中实现bitvectors数组

Question

我是z3py的新手,正在使用Python中的Z3 API,但无法弄清楚如何定义一个bitvectors数组.

我想要的东西:

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)