How to represent a floating point constant (e.g. 1e307) in the SMT-LIB standard?

Question

I am currently doing some experiments on Z3, and I have no idea of ​​representing a floating-point constant literal in the literature (e.g. 1e307):

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

A similar problem arose in FPA theory:

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

All of these SMT codes received an error message:

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

So, any idea to represent a decimal floating point constant in Z3 or SMT-LIB?

Answer 1

For the official syntax and semantics of floating point theory, see FP Theory . The main constructor of FP numbers is

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

i., FP 3 -. , ( to_fp).

, Z3 , :

((_ to_fp 11 53) RNE 1.0 307)

, , 307 2, 10, .. 1.0 * (2 ^ 307), 1p307.