z3 - SMT での浮動小数点演算のビットブラストの実装

Question

SMT ソルバーで浮動小数点演算構造のビットブラストをどのように実装しているのか疑問に思っていました。それを行うための既存のライブラリや機能 (VHDL など) はありますか、それとも最初から実装されていますか? これは、(C ? C++ ?) コードの行数を表します。

前もって感謝します。

Answer 1

私の知る限り、次の実装が存在します。

CBMC (厳密にはSMTソルバーではありませんが、必要なビットが含まれています)

https://github.com/diffblue/cbmc/blob/master/src/solvers/floatbv/float_utils.cpp

C++ でおよそ 2KLoC (ただし、別の 2KLoC であるすべてのビットベクトル操作のユーティリティ関数の上に構築されています)。もともとミューラーとポールの本から書かれたと思います。ESBMC には、このコードの以前のバージョンのフォークが含まれています。

Z3

上記のクリストフの回答を参照してください。Z3 には、CBMC 実装に「触発された」初期のプロトタイプ実装がありましたが、これは時の霧の中で失われました。

MathSAT

ソースは利用できません。実装はCBMCのものに「触発された」ため、サイズなどは似ています.

CVC4

私の CVC4 ブランチの 1 つ:

https://github.com/martin-cs/CVC4/tree/floating-point-symfpu

ビットブラスト浮動小数点エンジンを搭載。これは「スタンドアロン」ライブラリ (src/symfpu を参照 - 完全なリンクを提供しますが、github は投稿ごとに 2 つ以上のリンクを禁止しています...) として作成されており、個別にリリースされる予定です ... 間もなく。「バックエンド」でパラメータ化されているため、任意精度の浮動小数点ライブラリとして使用したり、さまざまなソルバーのビットベクトル式を生成したりできます。約 3.5KLoC のコードですが、いくつかの複数の実装が含まれています。オペレーション。これはゼロから書かれたものです (ただし、Handbook of Floating-Point は読んだことがあります)。

ソノラー

ソースがありません。C++ で実装されていると思います。Mueller と Paul の本に基づいていると誰かが言ったような気がします。

これらの実装を (クロス) 検証および検証するために、複数の真剣で独立した取り組みが行われていることに注意してください。すべてが完璧であるとは言いませんが (残りの部分と FMA についてはまだ完全な信頼を得ようとしています)、明らかなバグがないことがわかるはずです。

VHDL または Verilog デザインを使用することもできますが、... 合成可能な FPU を良好にするものは、(必然的に) エンコーディングを良好にするものではありません。実装のソースとして SoftFloat を使用している人もいますが、同様のコメントがあります。

Answer 2

SMT ソルバーにはまだ「多く」の実装はありませんが、Z3 はすべてを実装するものの 1 つです。コードはfpa2bv_converter.cppにあり、一目瞭然です。コードの大部分は、Mueller と Paul の「Computer Architecture」という本から着想を得ました。この本には、浮動小数点回路に関する章が含まれています。「Handbook of Floating-Point Arithmetic」(Muller et al.) にも、多くの情報/プログラム/回路が記載されています。