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

Question

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

我想要这样的东西：

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

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

有人能帮我正确的语法吗？在

Answer 1

下面的示例说明如何创建Z3位向量的“vector”（Python列表）。 该示例也可以在rise4fun在线获得。在

^{1}$