c++ - 如何在 z3 c++ 界面中启用校样？

Question

如何通过 Z3 中的 C++ 接口(interface)启用校样？我尝试了以下方法将 :produce-proofs 设置为 true，但如果我取消注释该行，稍后当我尝试将 !conjecture 添加到解决方案时，即使在取消注释调用 proof() 的行之前，我也会崩溃。基于示例 C++ 文件中的函数:

        void prove_example2(std::ostream& os) {
        os << "prove_example2\n";

        context c;
        solver s(c);
        params p(c);
        //p.set(":produce-proofs", true);
        s.set(p);

        expr x = c.int_const("x");
        expr y = c.int_const("y");
        expr z = c.int_const("z");
        sort I = c.int_sort();
        func_decl g = function("g", I, I);

        expr conjecture1 = implies(g(g(x) - g(y)) != g(z) && x + z <= y && y <= x,
            z < 0);


        s.add(!conjecture1);
        os << "conjecture 1:\n" << conjecture1 << "\n";
        if (s.check() == unsat) {
            os << "proved" << "\n";
            // Needs setup before calling
            //os << s.proof() << "\n";
        }
        else
            os << "failed to prove" << "\n";
}

Answer 1

参见 test_capi.c 中的 mk_proof_context .必须在上下文和求解器中启用证明。在 C++ 中，最简单的方法可能是通过

设置全局默认参数

z3::set_param("proof", "true");

在创建任何上下文或求解器之前。