充分利用μZ3（喇叭解算器）

Question

一个反例使用Z3的号角条款求解：

如果答案是SAT，可以得到一个满意的分配未知谓词（在大多数应用中，对应的电感不变某种过渡系统或程序调用系统）。

如果答案是unsat，那么这意味着存在于霍恩子句的展开和一个赋值于霍恩子句普遍量化变量，使得安全条件中的至少一个（具有false头的条款）被违反。这构成了一个具体的目击者为什么系统没有解决方案。

我怀疑，如果Z3可以得出结论unsat，那么它在内部具有某种形式的此类见证（如果我记得的话，无论如何PDR就是这种情况）。有没有办法打印出来？

也许我严重阅读文档，但我找不到方法。 (get-proof)打印某些不可读的内容，此外，(set-option :produce-proofs true)会造成一些棘手的问题。

Answer 1

Z3针对HORN逻辑问题产生的驳斥是以单位分辨率步骤树的形式出现的。你正在寻找的反例隐藏在单位解决步骤的结论中。这些结论（规则的最后一个论点）是与反例中的程序状态（或过程总结或其他）相对应的基本事实。产生这些事实的变量绑定可以在“quant-inst”规则中找到。

显然，这不是人类可读的，实际上很难被机器读取。对于Boogie，我实现了一个更常规的格式，但它目前仅适用于双重引擎，并且仅适用于使用“规则”和“查询”的定点格式。你可以使用下面的命令获得它。

（查询：engine duality：print-certificate true）