Z3（バージョン4）のUnsatコア

Question

私は、1年ほど前からZ3バージョン4.0のOcaml APIを使用していました。主にビットベクトル理論です。今私はZ3.solver_checkを実行した後にunsatコアを抽出する必要があります。残念ながらバージョン4にはこの機能がありません。私は数式の各ビットベクトル方程式を立てて、unsatコアを得るために仮定を使用するよう書き直すことができますが、これはコードの重要な部分ですが、全体的なパフォーマンスに影響する可能性があります。

バージョン4の前提を踏まないと、unsatコアを取得する方法はありますか？長期的な解決策はもちろん、最新のバージョンに移行することですが、障害の少ないソリューションがあれば良いでしょう。例えば、unsatの証明からunsatコアを抽出する方法がありますか（Z3.solver_get_proofによって返されます）？

ありがとうございます！

Answer 1

ソルバーモジュールのassert_and_track関数を使用すると、ソルバーモジュールのget_unsat_coreも、トラッキングされたアサーションに対応するトラッキングリテラルのセットを返します。メソッドUnsatCoreAndProofExample2のC＃APIとJava（https://github.com/Z3Prover/z3/blob/master/examples/java/JavaExample.java）にassert_and_trackを使用する例があります。 MLサンプルには対応する例はありませんが、OCamlへの変換はそれほど複雑ではありません。