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

【问题标题】：Z3 - How to set a byte constraint on a BitVecZ3 - 如何在 BitVec 上设置字节约束
【发布时间】：2016-10-26 10:09:38
【问题描述】：

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

例如：

让我们有一个名为bv 的32 位BV 和一个名为s 的Solver()：

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

我希望每个字节可以是0x2 或0x34 或0xFF 所以我使用Extract()：

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的正确方式。我是否以正确的方式编写了约束，还是我的思维过程完全错误？

【问题讨论】：

标签： python z3 bitvector

【解决方案1】：

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

【讨论】：

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

【讨论】：