floating-point - 如何在 SMT-LIB 标准中表示浮点常量(如 1e307)？

Question

目前我正在 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 中表示十进制浮点常数有什么想法吗？

Answer 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 .