2

我想使用 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 很陌生，无法弄清楚要采取什么方法或如何实现它。

4

1 回答 1

4

是的，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)
于 2013-06-23T16:23:21.317 回答