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

Question

我正在尝试将 Z3 与 c++ api（版本 Z3 4.1.0.0）一起使用，即我正在尝试解析来自 smt-competition unsat core track 的实例。我（基于示例）编写了以下代码：

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 列：未启用未饱和核心构造，使用命令（set-option :produce-unsat-cores true）”）

意外错误：解析器错误

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

Answer 1

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

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

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