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

Question

我是z3py的新手，正在学习Python中的Z3 API，但我不知道如何定义一个位向量数组。

我想要的是：

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

但是这个语法在教程的实践面板上甚至都没有起作用。

有人能帮忙提供正确的语法吗？

- Sharad

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)

- Leonardo de Moura

---

我们能否创建一个以整数/位向量为参数并返回"BitVecVector"的函数？对于"BitVecVector"，我们需要使用什么sort？谢谢。 - Shafiul