2

なぜZ3は、結合法則と可換性（AC）の公理を適用することによって、いくつかの些細な平等を示すことができるのか、そうでない場合もあるのだろうか。例えば、

(simplify (= (bvadd x (bvadd y z)) (bvadd z (bvadd y x))))

真になりますが、

(simplify (= (bvxor x (bvxor y z)) (bvxor z (bvxor y x))))

そうではありません（Z3はbvxorアプリケーションをフラット化するだけです）。

ソースコード（src / ast / bv_decl_plugin.cpp）を調べたところ、bvaddとbvxorの両方がACシンボルとして宣言されています。それらの各シンボルに適用される書き換えルールと関係がありますか？特に、mk_bv_add（src / ast / rewriter / bv_rewriter.cpp）は、単項式の合計としてbvadd項を処理するmk_add_core（src / ast / simpleifier / poly_simplifier_plugin.cpp）を呼び出します。

4

1 に答える 1

4

はい、それはシンボルに適用される書き換えルールに関連しています。Z3には、2つの式の簡略化子があります：src/ast/rewriterとsrc/ast/simplifier。これsrc/ast/simplifierはレガシーであり、新しいコードでは使用されません。SMT-LIBフロントエンドのsimplifyコマンドはに基づいていsrc/ast/rewriterます。はmk_bv_add実際にで使用mk_add_coreしていsrc/ast/rewriter/poly_rewriter.hます。

コードを変更して、Z3にbvxor質問の式を単純化するように強制することは難しくありませんtrue。に次のコード行を追加するだけsrc/ast/rewriter/bv_rewriter.hです。新しい行は単にbvxor引数をソートしています。これは、ACオペレーターにとって正しい書き直しです。

br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & result) {
    SASSERT(num > 0);
    ...
    default:
        // NEW LINE
        std::sort(new_args.begin(), new_args.end(), ast_to_lt());
        //
        result = m_util.mk_bv_xor(new_args.size(), new_args.c_ptr());
        return BR_DONE;
    }
}

そうは言っても、Z3リライターは、考えられるすべての単純化を適用したり、正規の正規形を生成したりすることは想定されていません。彼らの主な目標は、おそらくソルバーがより簡単な式を作成することです。ルールは、要求に基づいて（たとえば、例XではZ3が遅すぎ、新しい前処理ルールを適用することでパフォーマンスの問題を「修正」できます）、またはユーザーの要求に基づいて大きくなります。したがって、これが便利な機能であると思われる場合は、すべてのAC演算子の引数を並べ替えるオプションを追加できます。

編集

訂正：次のステートメントも変更する必要があります

if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (rational::power_of_two(sz) - numeral(1))))
    return BR_FAILED;

mk_bv_xorこのステートメントは、既存の書き換えルールのいずれも適用できない場合に、の実行を中断します。また、それを変更する必要があります。ここでこれらの変更を実装しました。新しいオプションを使用してそれらをアクティブ化できます:bv-sort-ac。このオプションはデフォルトでは有効になっていません。新しいオプションは、unstable（進行中の）ブランチで使用できます。trueに設定すると、ビットベクトルAC演算子がソートされます。unstableブランチは、次の公式リリースで利用可能になる新しいパラメータ設定フレームワークを使用する ことに注意してください。ブランチを構築する方法については、次の手順を参照してください。unstableこれらの変更は、今週、ナイトリービルドでも利用できるようになります。

新しいオプションを使用するいくつかの例を次に示します。

(declare-const a (_ BitVec 8))
(declare-const b (_ BitVec 8))
(declare-const c (_ BitVec 8))
(declare-const d (_ BitVec 8))

(simplify (= (bvxor a b c) (bvxor b a c)))
(simplify (= (bvxor a b c) (bvxor b a c)) :bv-sort-ac true)
(simplify (= (bvxor a (bvxor b c)) (bvxor b a c)) :bv-sort-ac true)

(simplify (= (bvor a b c) (bvor b a c)))
(simplify (= (bvor a b c) (bvor b a c)) :bv-sort-ac true)
(simplify (= (bvor a (bvor b c)) (bvor b a c)) :bv-sort-ac true)


(simplify (= (bvand a b c) (bvand b a c)))
(simplify (= (bvand a b c) (bvand b a c)) :bv-sort-ac true)
(simplify (= (bvand a (bvand b c)) (bvand b a c)) :bv-sort-ac true)

; In the new parameter setting framework, each module has its own parameters.
; The bv-sort-ac is a parameter of the "rewriter" framework.
(set-option :rewriter.bv-sort-ac true)

; Now, Z3 will rewrite the following formula to true even when we do not provide
; the option :bv-sort-ac true
(simplify (= (bvand a b c) (bvand b a c)))

; It will also simplify the following assertion.
(assert (= (bvand a b c) (bvand b a c)))

(check-sat)

編集終了

于 2013-03-24T16:30:37.030 に答える