Finding the weakest precondition using z3py

Question

I want to find the weakest precondition given an action and post condition using z3py.

Given the action N = N + 1 and the post condition N == 5 the weakest precondition would be N == 4.

Using the Tactic solve-eqs this approach works for some post conditions but not others. When using the post condition N < 5 I get [[Not(4 <= N)]].

But when using N == 5 I get [[]], when I would like N == 4.

N2 = Int('N2') # N after the action
N = Int('N') # N before the action

weakestPreconditionGoal = Goal()

# 'N2 == n + 1' action
# 'N2 == 5' post condition. 
weakestPreconditionGoal.add(N2 == N + 1,  N2 == 5)

t = Tactic('solve-eqs')
wp = t(weakestPreconditionGoal)
print(wp)

Is this the best approach find the weakest precondition?

I have tried a several methods but am new to Z3 and can not figure out what approach to take or how to implement it.

Leonardo de Moura Leonardo de Moura · Accepted Answer · 2013-06-23T16:23:21

Yes, solve-eqs can be used to eliminate equalities. The problem is that we have no control over which equalities will be eliminated. Another option is to use qe (quantifier elimination). The example is also available here.

N2 = Int('N2') # N after the action
N = Int('N') # N before the action

weakestPreconditionGoal = Goal()

# 'N2 == n + 1' action
# 'N2 == 5' post condition. 
weakestPreconditionGoal.add(Exists([N2], And(N2 == N + 1,  N2 == 5)))

t = Tactic('qe')
wp = t(weakestPreconditionGoal)
print(wp)

Another option is to use solve-eqs, but "guard" equations that we don't want to eliminate. We can guard the equations by using an auxiliary predicate guard. Here is an example (also available online here). Of course, we will have to perform a second pass to eliminate guard from the result.

N2 = Int('N2') # N after the action
N = Int('N') # N before the action
guard = Function('guard', BoolSort(), BoolSort())

weakestPreconditionGoal = Goal()

# 'N2 == n + 1' action
# 'N2 == 5' post condition. 
weakestPreconditionGoal.add(N2 == N + 1,  guard(N2 == 5))

t = Tactic('solve-eqs')
wp = t(weakestPreconditionGoal)
print(wp)

Finding the weakest precondition using z3py

1 Answers