如何在 z3 的 Python API 中实现位向量数组答案

【问题标题】：How to implement array of bitvectors in z3's Python APIs如何在 z3 的 Python API 中实现位向量数组
【发布时间】：2013-02-01 14:32:18
【问题描述】：

我是 z3py 的新手，正在使用 the Z3 API in Python，但不知道如何定义位向量数组。

我想要类似的东西：

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

但这种语法不起作用，即使在教程中的练习面板上也是如此。

有人可以帮忙看看正确的语法吗？

【问题讨论】：

标签： python arrays z3 bitvector

【解决方案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)

【讨论】：

我们能否创建一个以integer/bitvecotr 作为参数并返回“BitVecVector”的函数？我们需要为“BitVecVector”使用什么sort？谢谢