2

z3pyを使用して、アクションと事後条件が与えられたときに最も弱い前提条件を見つけたいです。

アクションN = N + 1と事後条件を考えるとN == 5、最も弱い前提条件は N == 4 になります。

Tactic を使用すると、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平等を排除するために使用できます。問題は、どの平等が排除されるかを制御できないことです。もう 1 つのオプションは、使用することです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結果から除外するには 2 回目のパスを実行する必要があります。

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 に答える