z3 z3py quantifiers first-order-logic hoare-logic

solving quantifier-free VC using z3

I was reading this research paper: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.9467&rep=rep1&type=pdf

So, in summary, they are transforming the quantified horn clauses to quantifier-free horn clauses by instantiation (via E-matching), and the resulting Verification Conditions (VCs) are given in Fig. 6 of the paper.

As per my understanding, the paper suggests to pass the resulting VCs in Fig. 6 to any SMT solver, since the VCs are now quantifier-free and can be solved by any SMT solver. (Please correct me, if I'm wrong in this.)

So, going ahead with this understanding, I tried coding Fig. 6 VCs with z3py.

Edit: My goal is to find the solution to the VCs in Fig. 6. What should I add as the return type of invariant P that is to be inferred by z3? Is there a better way to do this using z3? Thank you for your time!

Here's the code:

    from z3 import *
    Z = IntSort()
    B = BoolSort()

    k0, k1, k2, N1, N2 = Ints('k0, k1, k2, N1, N2')
    i0, i1, i2 = Ints('i0, i1, i2')

    P = Function('P', B, Z)

    a0 = Array('a0', Z, B)
    a1 = Array('a1', Z, B)
    a2 = Array('a2', Z, B)


    prove(And(Implies(i0 == 0, P( Select(a0,k0), i0) ), 
          Implies(And(P(Select(a1, k1),i1), i1<N1), P(Select(Store(a1, i1, 0)), i1+1) ),
          Implies(And(P(Select(a2,k2), i2), not(i2<N2)), Implies(0<=k2<=N2, a2[k2]) )))

Solution

You've a number of coding issues in your z3Py code. Here's a recoding of it, that at least goes through z3 without any errors:

from z3 import *

Z = IntSort()
B = BoolSort()

k0, k1, k2, N1, N2 = Ints("k0 k1 k2 N1 N2")
i0, i1, i2 = Ints("i0 i1 i2")

P = Function('P', B, Z, B)

a0 = Array('a0', Z, B)
a1 = Array('a1', Z, B)
a2 = Array('a2', Z, B)

s = Solver()
s.add(Implies(i0 == 0, P(Select(a0, k0), i0)))

s.add(Implies(And(P(Select(a1,k1),i1), i1<N1), P(Select(Store(a1, i1, False), k1), i1+1)))

s.add(Implies(And(P(Select(a2,k2),i2), Not(i2<N2)), Implies(And(0<=k2, k2<=N2), a2[k2])))

print(s.sexpr())
print(s.check())

Some fixes I put into your code:

The function P is a predicate and hence its final type is bool. Fix that by saying P = Function('P', B, Z, B)
The notation A <= B <= C, while you can write it in z3Py doesn't mean what you think it means. You need to split it into two parts and use conjunction.
It's a better idea to split constraints to multiple lines, easier to debug
Boolean negation is Not, it isn't not

etc. While z3 produces sat on this; but I'm not quite sure if this is the correct translation from the paper. (In particular, the notation a1[i1 ← 0][k1] or the sequence of implications A -> B -> C needs to be both correctly translated. You seem to be completely missing the C part of that sequence of implications. I haven't studied the paper, so I'm not sure what these are supposed to mean.)

So, the encoding I gave above, while goes through z3, is definitely not what the conditions in the paper actually are. But hopefully this'll get you started.