6

私はZ3が初めてで、オンラインのpythonチュートリアルをチェックしていました。

次に、BitVecs でオーバーフローの動作を確認できると考えました。

私はこのコードを書きました：

x = BitVec('x', 3)
y = Int('y')

solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))

そして、私は [y = 7, x = 7] を期待していました (つまり、値が等しいが、x + 1 が 0 になり、y + 1 が 8 になるため、後続の値が等しくない場合)

しかし、Z3 は [y = 0, x = 0] と答えます。

私は何を間違っていますか？

4

2 に答える 2

5

あなたが何か間違ったことをしているとは思いませんが、 BV2Intバグがあるようです:

 x = BitVec('x', 3)
 prove(x <= 3)
 prove(BV2Int(x) <= 3)

Z3py は最初のものを証明しますが、2 番目の反例を示しx=0ます。それは正しく聞こえません。(唯一の説明は奇妙な Python のことかもしれませんが、その方法がわかりません。)

+また、得られるモデルは、ビットベクトルを Python バインディングで符号付きの数値として扱うかどうかに依存することに注意してください。これは事実だと思います。ただし、BV2Int符号なしの値として扱うため、そうしない場合があります。これは事態をさらに複雑にするだろう。

いずれにせよ、BV2Intコーシャではないようです。Z3関係者から公式の回答があるまで、私はそれを避けます.

于 2013-07-24T01:46:36.140 に答える