Как представить константу с плавающей запятой (например, 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

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