Как представить константу с плавающей точкой (например, 1e307) в стандарте SMT-LIB?

Question

В настоящее время я провожу некоторые эксперименты на Z3 и не имею представления представлять константу с плавающей запятой (например, 1e307) в SMT:

(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

Официальный синтаксис и семантика теории с плавающей точкой см. В теории 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,