3

z3を使用して式を削除しようとしています

not ((not x) add y)

これはに等しい

x sub y

このコードによって：

(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))
(assert (= (bvnot (bvadd (bvnot x) y)) (bvsub x y)))
(check-sat)
(simplify (bvnot (bvadd (bvnot x) y)))

次のような結果を取得したい：

sat
(bvsub x y)

ただし、結果は次のとおりです。

sat
(bvnot (bvadd (bvnot x) y))

誰かが私を助けてくれませんか？

4

1 に答える 1

3

これは、次のスクリプト(bvnot (bvadd (bvnot x) y))を使用するのと同等であることを証明できます。(bvsub x y)

(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))
(assert (not (= (bvnot (bvadd (bvnot x) y)) (bvsub x y))))
(check-sat)

このスクリプトでは、Z3を使用して、それ(not (= (bvnot (bvadd (bvnot x) y)) (bvsub x y)))が不十分であることを示しました。つまり、の値がの値と異なるような値を見つけることはxできませyん。(bvnot (bvadd (bvnot x) y))(bvsub x y)

Z3では、simplifyコマンドは書き換えルールを適用するだけで、アサートされた式のセットを無視します。このsimplifyコマンドは、を使用して充足可能性をチェックするよりもはるかに高速ですcheck-sat。さらに、2つの同等の式Fとが与えられた場合、の結果がに等しくなるGという保証はありません。たとえば、Z3 v4.3.1では、simplifyコマンドは、とに対して異なる結果を生成しますが、これらは同等の式です。一方、とについては同じ結果が得られます。(simplify F)(simplify G)(= (bvnot (bvadd (bvnot x) y)(bvsub x y)(= (bvneg (bvadd (bvneg x) y)(bvsub x y)

(simplify (bvnot (bvadd (bvnot x) y)))
(simplify (bvneg (bvadd (bvneg x) y)))
(simplify (bvsub x y))

上記の例の完全なスクリプトは次のとおりです。

ところで、これらの例は、 Z3Pythonインターフェースを使用するとはるかに読みやすくなります。

x, y = BitVecs('x y', 32)
prove(~(~x + y) == x - y)
print simplify(x - y)
print simplify(~(~x + y))
print simplify(-(-x + y))

最後に、Z3にはより複雑な簡略化手順があります。それらは戦術として利用可能です。PythonおよびSMT2.0形式のチュートリアルは、追加情報を提供します。

もう1つの可能性は、Z3シンプリエ/リライターを変更することです。ご指摘のとおり、はとnot x同等-x -1です。この書き換えルールnot x --> -x - 1をZ3書き換えに簡単に追加できます。例として、このコミットでは、このルールを有効にする「bvnot2arith」という新しいオプションを追加しました。実際の実装は非常に小さいです（5行のコード）。

于 2012-12-27T16:35:42.307 に答える