python - Z3 - 如何在 BitVec 上设置字节约束

Question

我正在尝试在 BitVec 中设置可能允许的字节列表，但我不确定我实际上是否以正确的方式设置了约束。

例如：

让我们调用一个 32 位 BVbv和一个Solver()被调用s：

s = Solver()
bv = BitVec(8 * 4)

我希望每个字节都可以是我使用的一个0x2或0x34多个：0xFFExtract()

i = 0
while (i < 8 * 4):
    s.add(Extract(i + 7, i, bv) == 0x2)
    s.add(Extract(i + 7, i, bv) == 0x34)
    s.add(Extract(i + 7, i, bv) == 0xFF) 
    i += 8

可悲的是，s.check()回报unsat。

我认为这不是表达这些字节可能是0x2 OR 0x34 OR 0xFF的正确方法。我是否以正确的方式编写了约束，或者我的思维过程完全错误？

Answer 1

求解器中的约束是隐含的合取，即，您必须先构建析取，然后再构建析s.add(...)取。

Answer 2

i = 0
while (i < 8 * 4):
   s.add(Or(Extract(i + 7, i, bv) == 0x2), 
            Extract(i + 7, i, bv) == 0x34),
            Extract(i + 7, i, bv) == 0xFF)) 
i += 8