Z3は浮動小数点制約のNaN値を返します

Question

以下の浮動小数点制約があると、Z3はzがNaNの異常なモデルを生成します。明らかに、それは正しい解決策ではありません。バグですか？ BTW。 Z3のバージョンは、これらは、（SMT-LIBによれば、同様にIEEE-754による）関係演算子の正しいセマンティクスであり、これはバグではありません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

あります。私が手のモデルはこれです：

(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))が満たされて、何も未満NaN（すべての述語がNaN入力に対して偽である）ではないので、すなわち、x + yは、NaN以上です。

この動作が望ましくない場合、我々はもちろんzがNaNではないことを確認するために別の制約を追加することができます。

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

とZ3は、その後y（したがってx+y）がNaNあるモデルを見つけるだろう。