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)