python - (Z3Py) Concat、量词和位向量

Question

是否可以使用带有位向量和连接的量词？为了说明，在最新的 Z3 中运行以下代码：

a = BitVec('a', 8)
b = Concat(BitVec('b', 4), BitVec('c', 4))

prove(ForAll(a, Exists(b, a == b)))

产生以下错误：

BitVecRef instance has no attribute '__len__'

我尝试在其中添加一个简单的__len__方法，BitVecRef但出现了更多问题。

如果没有Concat，代码将按预期工作。例如：

a = BitVec('a', 8)
b = BitVec('b', 8)

prove(ForAll(a, Exists(b, a == b)))

输出正确：proved

Answer 1

您的示例将值 b 定义为串联的简写。它作为绑定变量传递给量词 Exists(b, a == b)。量词需要一个基本常量的列表，例如下面的 a、b、c，但不是复合表达式，例如 d。以下是您处理的拼图版本：

a = BitVec('a', 8)
b = BitVec('b', 4)
c = BitVec('c', 4)
d = Concat(b, c)

prove(ForAll(a, Exists(b, a == d)))