2
this paper（セクション3.2）では、z3は他のステップを実行する前に式の書き換え/簡略化を適用すると言います。式の書き換え
の式があり、それが複数の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ステートメントの書き換え/簡略化は、結果として不満の証拠を使用できなくなります（少なくとも使用するのは非常に難しい）。
あなたは何をしている記述することができます。また、次の2つのオプションを含める必要がありますやろうとしている？なぜ複数のアサートにまたがって書き直し/簡略化を行うと結果が使えなくなるのでしょうか？検索中、Z3はいくつかのアサーションにわたって推論ステップを実行することに注意してください。証明書を使用できないようにするでしょうか？ –
私は「純粋な」解像度の証明に証明を書き直そうとしています。アプリケーション固有の理由から、1つのassert文の内部で発生する単純化と書き換えは、私には興味がありません。つまり、私は、assertステートメントには既に単純化された式のバージョンが含まれていると仮定します。アサーションステートメントのすべての推論のステップは私にとって興味深いもので、何とかそれらを処理しなければなりません。アサーション全体で単純化が行われないことを確信できれば、私は書き直しをする間に対処するのが難しい（困難な）ケースが1つあります。これでもう少し明確になることを願っています。 – Georg