python - (Z3Py) 连接、量词和位向量

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__'

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

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

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

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

输出正确的:已证明

Answer 1

您的示例将值 b 定义为串联的简写。它作为绑定(bind)变量传递给量词 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)))