私は配列理論でメモリアクセスをモデル化しようとしています。以下のような簡単なコードがあります(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' を返すように上記のスクリプトを修正するにはどうすればよいですか?
本当にありがとう。