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)