(Z3Py) Concat、量词和位向量答案

【问题标题】：(Z3Py) Concat, quantifiers and bit-vectors(Z3Py) Concat、量词和位向量
【发布时间】：2013-04-27 16:40:35
【问题描述】：

是否可以使用带有位向量和连接的量词？为了说明，在最新的 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)))

输出正确：proved

【问题讨论】：

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

【讨论】：