Substitute function body (using z3py)

[rainoftime]

Consider a simple program below:

    assume int i = 0;
    while (i < 10) {
        i = i + 1;
    }
    assert i == 10;

To verify the Hoare trip, a convenient way is to use the CHC engine of Z3, e.g.,

    s = SolverFor("HORN")
    inv = Function('inv', IntSort(), BoolSort())
    i, ip = Ints('i ip')
    s.add(ForAll([i], Implies(i == 0, inv(i))))
    s.add(ForAll([i, ip], Implies(And(inv(i), i < 10, ip == i + 1), inv(IP))))
    s.add(ForAll([i], Implies(And(inv(i), i >= 10),  i == 10)))

Another possible strategy is to use template-based invariant generation (or CEGIS-style invariant learning, etc)
Suppose that we use i <= a as the template, and replace inv in the above formula.
After replacing the function body of inv, we obtain the following formula

    s = Solver()
    i, ip, a = Ints('i ip a')
    s.add(ForAll([i], Implies(i == 0,  i <= a)))
    s.add(ForAll([i, ip], Implies(And(i <= a, i < 10, ip == i + 1), ip <= a)))
    s.add(ForAll([i], Implies(And(i <= a, i >= 10), i == 10)))

For more general cases, is there any suggestion for substituting the function body using some templates?
For example, we may have the following templates for a candidate invariant inv = Function('inv', IntSort(), IntSort(), BoolSort())

    a0 + a1*x + a2*y  >= 0
    b0 + b1*x + b2*y  >= 0

Thanks!

[NikolajBjorner]

You would have to use the API and a visitor pattern on expressions.

[NikolajBjorner]

See a5d588c