更新z3可變或線性解決方案

Question

我是Z3的新手，所以這可能是一個愚蠢的問題。我試圖模擬一個程序的執行流程。現在通過手動z3執行此操作。也就是說，我最終試圖建模如下：

x = 1 
x += 1 

執行以下命令給我不滿意，我明白爲什麼。

x = z3.Int('x') 
s.add(x == 1) 
s.add(x == x + 1) 

規模小，它可能是合理的手動更改X == 1到x == 2，我的問題是，有沒有辦法在Z3要做到這一點，我沒有回去並嘗試修改我放入解算器的變量？這些方程顯然會比+1更難以操作，並且嘗試手動完成該邏輯看起來很容易出錯並且馬虎。

編輯：調整我的程序使用SSA建議後，它現在很容易工作。我確實選擇保留多個版本的變量，但這並沒有變成太多的額外工作。

Answer 1

您可以重命名變量，使它們處於SSA格式（https://en.wikipedia.org/wiki/Static_single_assignment_form）。 另外，您可能不需要爲中間表達式引入名稱。唯一的Z3變量應該是程序輸入或類似的東西。