Z3:为什么这个数组理论用法返回Unsat？

Question

我试图用数组理论来模拟内存访问。我有一个如下的简单代码（z3python）

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中读出，然后给它写不同的值。这真的是我被拒绝的原因吗？在

如果是这样，我如何使用数组理论来建模内存访问？如何修复上面的脚本，使其返回“Sat”？在

非常感谢。在

Answer 1

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

您的查询可以归结为要求Z3查找Mem和t的值，这样Mem[t] = Mem[t] - 1，这显然不是你能想到的任何{}和{}的值；因此Z3响应Unsat。在

如果你能告诉我们你想要满足什么性质，我们可以帮助你正确地表述它。在