HORN Clause Z3 Documentation

Question

I am trying to encode some imperative program using HORN logic of Z3 (set-logic HORN) but getting some difficulties of defining clause (using SMT2). Could anyone tell me where can I find a good source of documentations for this feature of Z3?

Answer 1

Well, there's more to it when it comes to "encoding" a program in horn clauses. First you need to check an appropriate proof rule: does the program has recursive functions, should you do function summarization? and so on.

There are a few papers on the subject, but I don't think there's any tutorial on VC gen. You may also want to take a look to some benchmarks in Horn SMT format to draw inspiration: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/clauses/

Feel free to ask if you have a specific question.