Z3給出我的浮點約束的NaN值

Question

給定以下浮點約束，Z3產生一個異常模型，其中z是NaN。顯然，這不是一個正確的解決方案。這是一個錯誤嗎？ 順便說一句。 Z3的版本4.5.0

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


(assert 
(and 
    (not (fp.lt x (_ +zero 11 53))) 
    (not (fp.lt y (_ +zero 11 53))) 
    (not (fp.lt z (_ +zero 11 53))) 
    (not (fp.leq (fp.add roundNearestTiesToEven x y) z)) 
) 
) 

(check-sat) 
(get-model) 

Answer 1

這不是錯誤，這些都是用於涉及（根據SMT-LIB和根據IEEE-754以及）的運營商的正確語義。我得到的模型是這樣的：

(model 
    (define-fun z() (_ FloatingPoint 11 53) 
    (_ NaN 11 53)) 
    (define-fun y() (_ FloatingPoint 11 53) 
    (fp #b0 #b00000000000 #x0000000004000)) 
    (define-fun x() (_ FloatingPoint 11 53) 
    (_ +zero 11 53)) 
) 

確實(not (fp.leq (fp.add roundNearestTiesToEven x y) z))滿足，即x + y不低於NaN少，因爲沒有什麼是小於NaN（所有謂詞都是假的NaN輸入）。

如果這種行爲是不希望的，我們當然可以添加其他約束，以確保z不是NaN：

(assert (not (= z (_ NaN 11 53)))) 

然後Z3會發現一個模型，其中y（因此x+y）是NaN 。