floating-point - Z3: 浮動小数点 FMA セマンティクス

Question

Z3 は、このベンチマークに対して満足のいくモデルを返します: http://rise4fun.com/Z3/Bnv5m

a*b+0ただし、クエリは基本的に、FMA 命令を使用するのと同等であると主張していますa*b。これは、IEEE 浮動小数点数にも当てはまると思います。ベンチマークは、どちらaでもないことを明示的に確認することに注意してください。bNaN

FMA のエンコードに問題はありますか?

Answer 1

はい、FMA には現在バグがあります。私は先週の金曜日に他の指示に対していくつかの修正をコミットしましたが、FMA の修正にはまだ取りかかっていません。レポート、特にテスト ケースに感謝します。特に FMA の場合、これは非常に役立ちます。