从 µZ3（喇叭求解器）获取反例

Question

使用 Z3 的 Horn 子句求解器：

如果答案是SAT，则可以对未知谓词（在大多数应用程序中，对应于某种转换系统或过程调用系统的归纳不变量）进行令人满意的分配。

如果答案是unsat，那么这意味着存在一个展开的 Horn 子句和对 Horn 子句中普遍量化的变量的赋值，使得至少有一个安全条件（带有 @987654323 的子句@head) 被违反。这构成了系统没有解决方案的具体见证。

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

也许我没有仔细阅读文档，但我找不到方法。 (get-proof) 打印出一些不可读的东西，此外，(set-option :produce-proofs true) 使一些问题变得难以处理。

Answer 1

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

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

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