1

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

バージョン 4 の想定を行わずにコアを取得する方法はありますか? もちろん、長期的な解決策は最新バージョンに移行することですが、混乱の少ない解決策があればそれでよいでしょう。たとえば、unsat の証明 (Z3.solver_get_proof によって返される) から unsat コアを抽出する方法はありますか?

ありがとう！

4

1 に答える 1

1

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

于 2016-08-09T00:50:50.627 に答える