z3 - 浮点文字

Question

我有两个关于编写 Z3 的 FPA 逻辑所接受的 IEEE 浮点常量的问题:

一、在this question ，克里斯托夫举了个例子:

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

我想知道最后是什么 0表示？我试过:

 ((_ asFloat 11 53) roundTowardZero 0.5))

这似乎也有效。拉默 paper似乎也不需要最后的 0；所以我很好奇它扮演什么角色。

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

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

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

谢谢..

Answer 1

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

最后0在示例中表示(二进制)指数，即 (... 0.5 1) == 1.0 .我们添加这个只是因为如果不能单独指定指数，数字有时会需要大量空间。这样，我们通常可以非常简洁地指定它们。
p1输出中的后缀表示二进制指数，即，其中 e8意味着 10^8 ，后缀p8将意味着 2^8 . Z3 目前只使用二进制指数，所以这里总会有一个 p 后缀，但这在 future 可能会改变。数字的其余部分被赋予足够的十进制数字来表示精确的结果。

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