3

Z3 を c++ API (バージョン Z3 4.1.0.0) で使用しようとしています。つまり、smt-competition unsat コア トラックからインスタンスを解析しようとしています。私は（例に基づいて）次のコードを書きました：

context c;
Z3_ast f;
f = Z3_parse_smtlib2_file(c, "smtlib_uc/QF_IDL/queens_bench/n_queen/queen3-1.smt2.uc.smt2", 0, 0, 0, 0, 0, 0);
expr r = to_expr(c, f);
solver s(c);
s.add(r);
std::cout << s << "\n";

しかし、私は次のエラーが発生します:

(エラー "行 1 列 34: エラー設定 ':produce-unsat-cores'、オプション値は初期化後に変更できません")

(エラー "行 220 列 15: unsat コアの構築が有効になっていません。コマンドを使用してください (set-option :produce-unsat-cores true)")

予期しないエラー: パーサー エラー

このエラーを克服する方法を知っている人はいますか?

4

1 に答える 1

2

Z3_parse_smtlib*関数は数式の解析専用です。したがって、多くのオプションはそれらでは機能しません。

(set-option :produce-unsat-cores true)入力ファイルの の行を削除するだけで、 の初期化時にそのオプションを設定できますcontext。Z3_solver_get_unsat_core を使用してunsatコアを取得できます。

入力ファイルを変更したくない場合は、代わりに Z3 バイナリを使用する必要があります。これらのオプションは、Z3 バイナリで正常に解析されます。

于 2012-10-16T13:47:48.620 に答える