0

我正在尝试用数组理论对内存访问进行建模。我有一个像下面这样的简单代码（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”的原因吗？

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

非常感谢。

4

1 回答 1

1

Why do you expect this query to return Sat?

Your query comes down to asking Z3 to find values for Mem and t such that Mem[t] = Mem[t] - 1, which is clearly not true of any value of Mem and t you can think of; so Z3 responds Unsat.

If you can tell us what property you're trying to satisfy, we can help you formulate it correctly.

于 2013-04-20T07:15:57.567 回答