floating-point - Z3 验证器中的浮点溢出指示

Question

是否可以使用 Z3 验证器检查浮点运算中的溢出和下溢？如果是，Z3 如何指示这些异常？

标签： floating-pointoverflowz3

Answer 1

SMTLib 的浮点逻辑（此处描述：http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml ，基于论文：http ://smtlib.cs.uiowa.edu/papers/BTRW15.pdf ）确实没有任何浮点异常的概念，例如精度、下溢、溢出、除零、非正规和无效。该论文第 VIII.B 节的直接引述说：

我们的形式化不涵盖 IEEE-754 的异常或标志概念（执行的默认处理）。这仅仅是因为逻辑公式中没有执行顺序的概念，因此在理论上没有直接表达这些概念的有意义的方式。

因此，逻辑中不支持浮点标志，z3 也不支持它们。

注意：我个人不同意该论文中给出的推理。例如，Z3 可以检查位向量指令的上溢/下溢，请参阅https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf。类似的方法也可以适用于浮点，使用新的 SMTLib 命令来检测 PUOZDI 标志。然而，这还没有正式化，据我所知，没有求解器为 FPA 实现了这个想法。