Search code examples
z3isabelle

How does a z3 certificate look like?

In Extending Sledgehammer with SMT solvers I find this quote:

Certificates make it possible to store Z3 proofs alongside Isabelle formalizations, allowing SMT proof replay without Z3. Only if the formalizations cahnge must the certificates be regenerated.

How does a Z3 certificate look like? Is it just some sort of balanced tree where the inference steps obtained in Z3 are stored?

Solution

  • A certificate is simply the proof produced by Z3. Here is an example (taken from the file SMT_Examples.certs you can find in the Isabelle distribution):

    23f5eb3b530a4577da2f8947333286ff70ed557f 11 0
unsat
((set-logic AUFLIA)
(proof
(let (($x29 (exists ((?v0 A$) )(! (g$ ?v0) :qid k!7))
))
(let (($x30 (f$ $x29)))
(let (($x31 (=> $x30 true)))
(let (($x32 (not $x31)))
(let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false))))
(mp (asserted $x32) @x42 false))))))))

    A Z3 proof is, in essence, a proof tree with false as a conclusion, not a balanced tree. The reconstruction and the proof format is described in a paper by Sascha Böhme.

    Remark that Sledgehammer has nothing to do with certificates. Whenever you have an smt call (whether you have written it by hand or used Sledgehammer to produce it), you can use certificates. However, I don't know anyone doing it.