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

Question

我正在尝试将 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 列:':product-unsat-cores' 设置错误，选项值初始化后无法修改”)

(错误“第 220 行第 15 列:未启用 unsat 核心构建，使用命令 (set-option :product-unsat-cores true)”)

意外错误:解析器错误

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

Answer 1

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

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

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