QF_FPA？ Z3是否支持IEEE-754算法？

瀏覽Z3源代碼，我遇到了一堆涉及QF_FPA的文件，這似乎代表無量化的浮點算術。但是，我似乎無法找到任何關於其狀態的文檔，或者如何通過各種前端（特別是SMT-Lib2）來使用它。這是IEEE-754 FP的編碼嗎？如果有，支持哪些精度/操作？任何文檔都是最有幫助的。QF_FPA？ Z3是否支持IEEE-754算法？

來源

2013-03-03 Levent Erkok

是的，Z3支持Ruemmer和Wahl在最近的SMT研討會paper中提出的浮點運算。在現階段，沒有正式的FPA理論，Z3的支持是非常基本的（只有一點點衝擊波）。我們現在還沒有積極投放廣告，但它可以完全按照Ruemmer/Wahl（設置邏輯QF_FPA和QF_FPABV）的文章中提出的方式使用。目前，我們正在爲FPA制定一個新的決策程序，但這需要一段時間才能獲得。

這裏是什麼的FPA SMT2公式可能看起來像一個簡單的例子：

(set-logic QF_FPA)  

(declare-const x (_ FP 11 53)) 
(declare-const y (_ FP 11 53)) 
(declare-const r (_ FP 11 53)) 

(assert (and 
    (= x ((_ asFloat 11 53) roundTowardZero 0.5 0)) 
    (= y ((_ asFloat 11 53) roundTowardZero 0.5 0)) 
    (= r (+ roundTowardZero x y)) 
)) 

(check-sat)

來源

2013-03-04 11:11:45

是否已將此浮點運算支持合併到z3的最新穩定版本4.3.2中？另外，浮點理論支持是否已經與其他理論（例如線性整數算法）結合起來，可以是穩定版本還是不穩定版本？ – user1779685 2015-06-29 17:41:20

4.3.2只有部分支持，目前版本爲4.4.0，其中包括理論組合在內的全面支持。請注意，從浮點數到實數/有理數的轉換引入了非線性約束，因此與線性算術的組合也變爲非線性。 – 2015-06-30 10:17:46

感謝有關轉換和理論組合的知識。我檢查了github：4月底的z3版本更廣泛的支持是好消息。將很快嘗試。 – user1779685 2015-06-30 14:36:17

浮點邏輯被命名爲QF_FP和QF_FPBV在v4.4.2。 RELEASE_NOTES中理論描述的鏈接被破壞。正確的頁面是http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml。上面的建議示例應該是

(set-logic QF_FP) 

(declare-const x (_ FloatingPoint 11 53)) 
(declare-const y (_ FloatingPoint 11 53)) 
(declare-const r (_ FloatingPoint 11 53)) 

(assert (and 
    (= x (fp #b0 #b00000000010 #b0000000000000000000000000000000000000000000000000010)) 
    (= y (fp #b0 #b00000000010 #b0000000000000000000000000000000000000000000000000010)) 
    (= r (fp.add roundTowardZero x y)) 
)) 

(check-sat)

來源

2015-10-30 15:46:57

感謝Daniel更新示例！ SMT FP標準已經更新，這確實是新的語法。我們已經從Z3中刪除了所有舊符號，並且我們只支持最終的標準。 – 2015-10-31 13:34:04

QF_FPA？ Z3是否支持IEEE-754算法？

回答

相關問題