Z3 验证器中的浮点溢出指示
Floating point overflow indication in Z3 verifier
是否可以使用 Z3 验证程序检查浮点运算中的上溢和下溢？如果是，Z3 是如何指出这些异常的？
SMTLib 的浮点逻辑（此处描述：http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml, based on the paper: http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf）not 没有任何关于 floating-point 异常的概念，例如精度、下溢、溢出、 div-by-zero、非规范化和无效。该论文第 VIII.B 节的直接引述说：
Our formalization does not cover the IEEE-754 notion of exceptions or
flags (the default handling of executions). This is simply because
there is no notion of execution order in a logical formula, and so
there is no meaningful way of expressing those notions directly in
theory.
所以，逻辑上不支持floating-point-flags，z3也不支持。
注：我个人不同意那篇论文给出的推理。例如，Z3 可以检查 overflow/underflow 以获取 bit-vector 指令，请参阅 https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf。 floating-point 也可以采用类似的方法，使用新的 SMTLib 命令来检测 PUOZDI 标志。然而，这还没有正式化，据我所知，还没有求解器为 FPA 实现了这个想法。
是否可以使用 Z3 验证程序检查浮点运算中的上溢和下溢？如果是，Z3 是如何指出这些异常的？
SMTLib 的浮点逻辑（此处描述：http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml, based on the paper: http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf）not 没有任何关于 floating-point 异常的概念，例如精度、下溢、溢出、 div-by-zero、非规范化和无效。该论文第 VIII.B 节的直接引述说：
Our formalization does not cover the IEEE-754 notion of exceptions or flags (the default handling of executions). This is simply because there is no notion of execution order in a logical formula, and so there is no meaningful way of expressing those notions directly in theory.
所以，逻辑上不支持floating-point-flags，z3也不支持。
注：我个人不同意那篇论文给出的推理。例如，Z3 可以检查 overflow/underflow 以获取 bit-vector 指令，请参阅 https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf。 floating-point 也可以采用类似的方法，使用新的 SMTLib 命令来检测 PUOZDI 标志。然而，这还没有正式化，据我所知，还没有求解器为 FPA 实现了这个想法。