Z3的反例输出 [英] Counterexample output of Z3

问题描述

当 Z3 中的公式未满足并且指定了 (get-proof) 时，会出现一个输出，但我找不到任何关于它是什么的信息.我在哪里可以找到任何相关文档?

When a formula in Z3 is unsat and (get-proof) is specified there is an output which I don't find any information about what it is. Where can I find any documentation about that?

在我看来很不可读，是否有任何工具可以将其作为输入?

Seems to me quite unreadable, is there possibly any tool that takes this as an input?

干杯，马特

推荐答案

The proofs"Z3 生产的产品不供人类食用.论文中描述了该格式的过时版本:证明和反驳，和Z3.z3_api.h 文件 对每一个证明规则都有很长的描述.证明规则标识符以 Z3_OP_PR 开头.我知道有两个应用程序使用 Z3 证明对象.下面的论文包含了大量的例子，并描述了如何使用证明对象.

The "proofs" produced by Z3 are not for human consumption. An outdated version of the format is described in the paper: Proofs and Refutations, and Z3. The z3_api.h file has a long description of each one of the proof rules. The proof rule identifiers start with Z3_OP_PR. I am aware of two applications that use the Z3 proof objects. The following papers contain a lot of examples, and describe how the proof objects can be used.

1. Isabelle Interactive Theorem Prover:Z3 证明是在 Isabelle 内部使用可信核心重建的.您可以在 Sascha Bohme 的主页

插值的生成

正如 pad 所说，unsat-cores 使用起来要简单得多.

As pad said, unsat-cores are much simpler to use.

这篇关于Z3的反例输出的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！