CODEWITHSUNDEEP
z3
MattKay
MattKay

Reputation: 115

Counterexample output of Z3

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?

Cheers, Matt

Upvotes: 6

Views: 2172

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

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 proofs are reconstructed inside of Isabelle using a trusted core. You can find several papers describing this work and the Z3 proof format at Sascha Bohme's homepage

  2. Generation of interpolants

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

Upvotes: 8

Related Questions