Z3條件語句

Question

如何在Z3中編寫條件語句。

eg: 
if (a%2==0){ 
value=1 
} 

我想微軟研究院來實現這Z3求解，但到目前爲止沒有運氣

Answer 1

查找SSA形式：https://en.wikipedia.org/wiki/Static_single_assignment_form

本質上講，你必須改變你的程序看如：

value_0 = 0 
value_1 = (a%2 == 0) ? 1 : value_0 

一旦它在這個所謂的靜態單一賦值形式，你現在可以直接或多或少地直接翻譯每一行;最後的作業爲value_N，最終值爲value。

循環將會產生問題：通常的策略是將它們展開到一定數量（有界模型檢查），並希望這樣做足夠。如果您檢測到最後一次展開不夠用，那麼您可以在該點生成一個未解釋的值;這可能會導致你的證據以虛假的反例失敗;但如果沒有涉及適當處理歸納法和循環不變式的方案，這是最好的。

請注意，這個研究領域被稱爲「象徵性執行」，並有着悠久的歷史，目前正在進行積極的研究。您可能需要閱讀以下內容：https://en.wikipedia.org/wiki/Symbolic_execution