目前我正在对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中表示十进制浮点常数?
1 回答
有关浮点理论的官方语法和语义,请参阅Theory FP . FP数字的主要构造函数是
即,FP号由3个位向量构成 . 在文档中还有一些转换函数可以将其他数字转换为浮点数(全部称为
to_fp
) .除了那里描述的那些,Z3还支持另一个转换,如下所示:
但请注意,
307
这里是2的幂,而不是10的幂,即,这是1.0 *(2 ^ 307),有些工具可能会将其打印为1p307
.