使用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（消除量詞）。該示例也可用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) 

另一種選擇是使用solve-eqs，但我們不想消除的「保護」方程。 我們可以通過使用輔助謂詞guard來保護方程。這裏是一個例子（也可在線here）。當然，我們將不得不執行第二次通過以從結果中消除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)