Z3：为什么这个数组理论使用返回 Unsat？

Question

我正在尝试使用数组理论对内存访问进行建模。我有一个像下面这样的简单代码（Z3 python）

Mem = Array('Mem', BitVecSort(32), BitVecSort(32))

F = True
tmp = BitVec('tmp', 32)
tmp3 = BitVec('tmp3', 32)
F = And(F, tmp3 == Select(Mem, tmp))
tmp4 = BitVec('tmp4', 32)
F = And(F, tmp4 == (tmp3 - 1))
F = And(F, Mem == Store(Mem, tmp, tmp4))

s = Solver()
s.add(F)
print s.check() 

我想要 'Sat' 结果，但此脚本返回 'Unsat'。

我认为这是因为我从 Mem 中读出，然后向它写入不同的值。这真的是我得到“Unsat”的原因吗？

如果是这样，我如何使用数组理论对内存访问进行建模？如何修复上述脚本，使其返回 'Sat'？

非常感谢。

Answer 1

您为什么希望此查询返回 Sat？

您的查询归结为要求 Z3 查找 Mem 和 t 的值，例如 Mem[t] = Mem[t] - 1，这显然不是您能想到的 Mem 和 t 的任何值；所以Z3回复Unsat。

如果您能告诉我们您想要满足什么属性，我们可以帮助您正确地制定它。