Z3條件語句

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

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

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

2017-06-01 ha93

首先請注意，Z3表達式不會直接對程序進行編碼。在表達中沒有直接的副作用概念。您可以從任何由Z3公開的API中構建「if-then-else」表達式。 –

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

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

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

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

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

2017-06-02 16:09:09

回答