（Z3Py）Concat、量词和位向量

Question

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

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

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

产生以下错误：

^{pr2}$

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

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

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

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

输出正确的：proved

Answer 1

您的示例将值b定义为串联的速记。 它被传递给量词的绑定变量存在（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)))