solving quantifier-free VC using z3

Question

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]) )))

Function('P', B, Z) is a function from B to Z; the declaration is missing the second argument or the return type. — Christoph Wintersteiger
True! I've missed the return type. As per the research paper I referenced in the question, it's an invariant that is to be inferred. I'm not exactly sure how will it be inferred by the solver, as it is mentioned in the paper, and what's the return type of invariant. — user8616916

alias alias · Accepted Answer · 2020-10-20T17:15:13

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.

solving quantifier-free VC using z3

1 Answers