Нахождение самой слабой предпосылки с помощью z3py

Question

Я хочу найти самое слабое предварительное условие, заданное действием и последующим условием, используя z3py.

Учитывая действие N = N + 1 и почтовое условие N == 5 самым слабым предварительным условием было бы N == 4.

Используя Тактику solve-eqs этот подход работает для некоторых почтовых условий, но не для других. При использовании почтового условия N < 5 я получил [[Not(4 <= N)]],

Но при использовании N == 5 я получил [[]]когда я хотел бы 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)

Является ли это лучшим подходом найти самое слабое предварительное условие?

Я попробовал несколько методов, но я новичок в Z3 и не могу понять, какой подход выбрать или как его реализовать.

Answer 1

Да, solve-eqs может быть использован для устранения равенства. Проблема в том, что у нас нет контроля над тем, какие равенства будут устранены. Другой вариант заключается в использовании qe (устранение квантификатора). Пример также доступен здесь.

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)

Другой вариант заключается в использовании solve-eqs, но "охраняют" уравнения, которые мы не хотим исключать. Мы можем защитить уравнения с помощью вспомогательного предиката guard, Вот пример (также доступен онлайн здесь). Конечно, нам придется выполнить второй проход, чтобы устранить guard из результата.

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)