parsing - Z3 C++，如何解析smt-competition unsat核心实例

我试图将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)”)

意外错误:解析器错误

有人知道如何克服这个错误吗？

最佳答案

Z3_parse_smtlib*函数仅用于解析公式；因此，许多选项将不适用于它们。

您可以简单地删除输入文件中的(set-option :produce-unsat-cores true)行，并在初始化context时设置该选项。您可以使用Z3_solver_get_unsat_core检索未饱和的岩心。

如果您不想修改输入文件，则应改用Z3二进制文件。这些选项将使用Z3二进制文件成功解析。