2

この論文(セクション 3.2) では、z3 が他のステップを実行する前に式の書き換え/簡略化を適用すると述べています。

に、複数のステートメントQF_UFで構成される式があるとします。assert異なる assert ステートメント間の何らかの形で「障壁を破る」書き換えルールはありますか? または、逆に、1 つの assert ステートメントの "内" で、書き換えルールがローカルにのみ適用されることを確認できますか?

たとえば、次の式を考えてみましょう。

(set-logic QF_UF)
(set-option :auto-config false)
(set-option :PROOF_MODE  2)

(declare-fun a () Bool)
(assert a)
(assert (not a))

(check-sat)
(get-proof)

証明には を証明するための解決ステップが含まれていると確信できますか、それとも書き直し/単純化ステップによって結論付けられるFalse可能性はありますか?False

私が質問している理由は、私のアプリケーションでは、すべてのassertステートメントに特別なセマンティクスがあるからです。いくつかのステートメントにまたがる書き直し/単純化assertは、結果として得られる不満足性の証明を使用できない (または少なくとも: 使用するのが非常に難しい) ものにするでしょう。

4

1 に答える 1

1

Z3 3.2 は、いくつかの前処理ステップを適用します。を使用(set-option :auto-config false)すると、それらのほとんどが無効になります。次の 2 つのオプションも含める必要があります。

(set-option :propagate-booleans false)

(set-option :propagate-values false)

于 2012-04-25T18:12:27.973 に答える