SMT-LIB标准中如何表示一个浮点常量（如1e307）？

【问题标题】：How to represent a floating point constant (such as 1e307) in SMT-LIB standard?SMT-LIB标准中如何表示一个浮点常量（如1e307）？
【发布时间】：2015-10-12 08:58:42
【问题描述】：

目前我正在Z3上做一些实验，我不知道在SMT中表示一个浮点常量字面量（例如1e307）：

(declare-const a Real)
(assert (= a 1e+307))
(check-sat)

FPA 理论也出现了同样的问题：

(declare-const a (_ FloatingPoint 11 53))
(assert (= a 1e+307))
(check-sat)

所有这些 SMT 代码都收到错误消息：

(error "line 2 column 14: unknown constant e+307")

那么有什么想法可以在 Z3 或 SMT-LIB 中表示十进制浮点常量吗？

【问题讨论】：

标签： floating-point constants z3 smt

【解决方案1】：

有关浮点理论的官方语法和语义，请参阅Theory FP。 FP 数字的主要构造函数是

(fp (_ BitVec 1) (_ BitVec eb) (_ BitVec i) (_ FloatingPoint eb sb))

即，FP 数由 3 个位向量构成。在文档的更下方，还有可以将其他数字转换为浮点数的转换函数（都称为to_fp）。

除了上面描述的之外，Z3 还支持另一种转换，如下所示：

((_ to_fp 11 53) RNE 1.0 307)

但是请注意，这里的 307 是 2 的幂，而不是 10 的幂，即这是 1.0*(2^307)，某些工具可能会将其打印为 1p307。

【讨论】：

非常感谢您非常有帮助的回答！