Horn clauses in Z3

问题:

Z3 now supports solving for inductive invariants (implying a desired property) if the semantics of the program to analyze is given as Horn clauses.

The version in the master branch of the Z3 source code on z3.codeplex.com however does not support this feature. Since Z3 solves these Horn clauses problems by the PDR algorithm, which uses interpolation, I compiled instead the interp branch (d8b31773b809), which supports (set-logic HORN).

As far as I understood, a Horn-clause problem is to be specified with unknown predicates representing invariants, and a predicate over X×Y is just a function from X×Y to Bool. So far so good.

The first example I tried is just a problem of inferring an inductive invariant for a for(int i=0; i<=10; i++) loop.

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (forall ((I Int)) (or (> I 10) (not (inv I)) (inv (+ I 1)))))
(check-sat)

So far so good, got sat. Now just added (assert (not (inv 15)) and I got unsat. I then tried

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (not (inv 15)))
(check-sat)

and got unsat.

What am I doing wrong?

回答1:

Use the "unstable" branch. The "interp" branch is for internal development and the state of this branch can fluctuate. I get the answer "sat" on your second problem.

A slightly more interesting version of the first problem is:

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (forall ((I Int)) (or (> I 10) (not (inv I)) (inv (+ I 1))))) 
(assert (forall ((I Int)) (=> (inv I) (<= I 11))))
(check-sat)
(get-model)

It produces the obvious inductive invariant. If you replace the last assertion by

(assert (forall ((I Int)) (=> (inv I) (<= I 10)))) 

Instead you get a (hard to read) proof.