z3 - 浮点字面量

Question

我有两个关于编写 IEEE 浮点常量的问题，正如 Z3 的 FPA 逻辑所接受的那样：

首先，在这个问题中，Christoph 使用了这个例子：

 ((_ asFloat 11 53) roundTowardZero 0.5 0))

我想知道最后的意义0是什么？我试过了：

 ((_ asFloat 11 53) roundTowardZero 0.5))

这似乎也有效。Rummer 的论文似乎也不需要最后的 0。所以我很好奇它扮演什么角色。

其次，当我从 Z3 获取模型时，它会打印浮点文字，如下所示：

 (as +1.0000000000000002220446049250313080847263336181640625p1 (_ FP 11 53))

我如何解释p1后缀？还有哪些可能的后缀？

谢谢..

Answer 1

感谢您指出这些问题。两者都是因为还没有就输入或输出中的浮点文字达成一致的标准。

示例中的 final0表示（二进制）指数，即(... 0.5 1) == 1.0。我们添加这个只是因为如果不能单独指定指数，数字有时会需要很多空间。这样，我们通常可以非常简洁地指定它们。

输出中的p1后缀表示二进制指数，即，其中e8表示10^8，后缀p8表示2^8。Z3 目前只使用二进制指数，所以这里总会有一个 p 后缀，但将来可能会改变。数字的其余部分有足够的十进制数字来表示精确的结果。

请注意，SMT 社区尚未就输出格式达成一致。这在未来可能会改变。例如，有关于是否应该以 IEEE 位向量格式或位于实数和非 IEEE 位向量之间的中间格式进行讨论的讨论。