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 实现的“启发”，但这已经被时间的迷雾迷失了。

数学SAT

来源不可用，实施受到 CBMC 的“启发”，因此大小相似，等等。

CVC4

我的 CVC4 分支之一：

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

有一个位爆破浮点引擎。它被编写为一个“独立”库（请参阅 src/symfpu - 我会提供完整链接，但 github 会阻止每个帖子超过两个链接......），它将单独发布......很快。它在“后端”中被参数化，因此它可以用作任意精度的浮点库，为不同的求解器生成位向量表达式等。它大约 3.5KLoC 的代码，但确实包含一些的多个实现操作。它是从头开始编写的（尽管我已经阅读了浮点手册）。

声纳

源代码不可用，我相信它是用 C++ 实现的，并且感觉有人告诉我它是基于 Mueller 和 Paul 的书。

请注意，已经进行了多次、认真、独立的努力来（交叉）验证和验证这些实现。我不会声称一切都是完美的（我们仍在努力对剩余和 FMA 充满信心），但您应该会发现它们没有明显的错误。

您可以使用 VHDL 或 Verilog 设计，但是......制作好的可合成 FPU 并不是（必然）制作好的编码。我知道有些人使用 SoftFloat 作为实现的来源，但也有类似的评论。

Answer 2

SMT 求解器中还没有“很多”实现，但 Z3 是实现所有东西的实现之一。代码在fpa2bv_converter.cpp中，它相当不言自明。对于大部分代码，我从 Mueller 和 Paul 的“计算机体系结构”一书中获得灵感，其中有一章是关于浮点电路的。“Handbook of Floating-Point Arithmetic”（Muller 等人）也提供了大量信息/程序/电路。