如何在 z3 c++ 界面中启用证明？答案

【问题标题】：How do I enable proofs in the z3 c++ interface?如何在 z3 c++ 界面中启用证明？
【发布时间】：2017-02-11 00:33:50
【问题描述】：

如何在 Z3 中通过 C++ 接口启用校样？我尝试了以下方法将 :produce-proofs 设置为 true，但如果我取消注释该行，稍后当我尝试将 !conjecture 添加到解决方案时，我会崩溃，甚至在取消注释调用证明（）的行之前。基于示例 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";
}

【问题讨论】：

标签： c++ z3

【解决方案1】：

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

设置全局默认参数

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

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

【讨论】：

看起来这样可行，但我必须记住在获得证明后的某个时间再次关闭证明参数，否则它会导致后续单元测试崩溃（这不是在全部）。
如果您有一个（小而易读的）测试用例要分享，我们很高兴看到这些崩溃！
嗨，克里斯托弗。崩溃的单元测试，基于分发中的 example.cpp 文件，是非线性示例 1，当我从先前的测试（demorgan，我在 unsat 案例中转储证明）中保留了证明参数时。我转换的其他似乎没问题（到目前为止通过 bitvector_example2），如果我关闭参数，崩溃就会消失。所以我猜这是与非线性示例1中的自动配置内容的特定冲突，您可以在该示例文件上尝试。我们已经在我们的构建系统下得到了这个，或者我会在原始发行版上自己尝试一下。
另外，我们拥有的 z3 版本已经有几年历史了，如果这有什么不同的话。我们可能会在下一次发布后的某个时间对其进行更新。
看起来我们还有另一个单元测试，我们的一个，它不使用 autoconfig，但如果 proof 参数保持打开，则在 ast.cpp 中断言。不过，你需要做更多的工作。