浮點文字

我已經寫關於IEEE浮點常數的兩個問題，通過Z3的FPA邏輯所接受：浮點文字

首先，在this question，克里斯托夫使用的例子：

((_ asFloat 11 53) roundTowardZero 0.5 0))

我想知道最後的0意味着什麼？我試過了：

((_ asFloat 11 53) roundTowardZero 0.5))

而且這似乎也適用。 Rummer的paper似乎也不需要最終的0;所以我很好奇它扮演着什麼角色。

其次，當我從Z3得到一個模型，它打印浮點文字就像這樣：

(as +1.0000000000000002220446049250313080847263336181640625p1 (_ FP 11 53))

如何解釋p1後綴？還有哪些後綴是可能的？

謝謝..

來源

2013-03-31 Levent Erkok

感謝您指出這些問題。這兩者都是因爲在輸入或輸出中還沒有關於浮點文字的商定標準。

該例子中的最終0代表（二進制）指數，即(... 0.5 1) == 1.0。我們增加了這一點，因爲如果指數不能單獨指定，數字有時會需要大量的空間。這樣，我們經常可以很簡潔地指定它們。

p1的後綴在所述輸出表示二進制指數，即，其中e8裝置10^8，後綴p8將意味着2^8。 Z3目前只使用二進制指數，所以在這裏總會有一個p後綴，但這可能會在將來改變。數字的其餘部分提供足夠的小數位數來表示精確的結果。

請注意，輸出格式尚未由SMT社區同意。這可能在未來發生變化。例如，關於這是應該用IEEE位矢量格式還是介於實數和非IEEE位矢量之間的中間格式進行討論。

來源

2013-04-02 11:48:17

謝謝Christoph，這很有道理。然而，讀Rummer的論文後，我仍然認識到FP數字應該使用有理數寫成，如下：'（/ 2 3）'。這可以用作模型中的輸入和輸入。我喜歡這種方法，因爲它是明確的，並且每個FP編號可以相對容易地轉換爲理性。也許我們可以有一個'pp.print_fpa_as_rational'或類似的選項來指定這個功能，以便爲構建在Z3之上的工具提供一致性？ –

是的，Z3在這裏也接受有理數，例如（（__float11535）roundTowardZero（/ 2 3））。就個人而言，我更喜歡尾數+指數符號，因爲它通常更簡潔，但其他人當然可以有其他偏好。在爲輸出實現不同的選項之前，我想等一會兒看看SMT社區做出了什麼決定（例如，我們也在輸出中請求了IEEE位向量格式）。 –

對於所有對SMT中的FPA感興趣的人的說明：有一個名爲smt-fp的谷歌組[請參閱http://groups.google.com/forum/#!forum/smt-fp]，它用於討論這個話題當然包括輸出格式。反饋和請求是最受歡迎的！ –

回答

相關問題