Contractor pin Z3

When the formula in Z3 is unsat and (get-proof) is specified, there is a way out that I can not find any information about what it is. Where can I find documentation about this?

It seems that I am not reading, is it possible any tool that accepts this as input?

Cheers, Matt

+6
source share
1 answer

The "evidence" produced by Z3 is not intended for human consumption. An outdated version of the format is described in the document: Evidence and Disclaimer and Z3 . The z3_api.h file has a long description of each of the evidence. Verification rule identifiers begin with Z3_OP_PR . I know about two applications that use Z3 proof objects. The following documents contain many examples and describe how evidence objects can be used.

1- Isabella Interactive Theoretical Theorem: Z3 proofs are reconstructed inside Isabelle using a trusted kernel. You can find several works describing this work, and the Z3 proof format on the Sascha Bohme Home page

2- Interpolation Generation

As the pack says, unsat-cores much easier to use.

+7
source

Source: https://habr.com/ru/post/907472/


All Articles