Ответ, который вы ищете:
0 011 110001
Вы можете перестать читать, если это все, что вас заботит; но если вы хотите узнать, как я нашел его и как SMT-решатели могут помочь ответить на такие вопросы о числах с плавающей запятой (среди многих других!), читайте дальше.
Если у вас есть 3 экспонентных бита, 6 значащих бит и 1 знаковый бит; тогда у вас есть всего 10 бит. Эрик уже объяснил общую схему того, как выполнить преобразование, но он использовал 16-битный так называемый формат half-precision
. Поскольку у вас есть этот нестандартный формат, он не дает прямого ответа на ваш вопрос. Вы можете следовать его рассуждениям и делать то же самое для своего формата (вам придется выяснить правильное смещение и т. Д.), Или использовать инструмент, чтобы сделать все это за вас.
Современные преобразователи SMT могут быть легко использованы для таких преобразований. Решатель SMT - это своего рода автоматическое средство проверки теорем, которое может иметь дело с различными интересующими теориями, в том числе с плавающей точкой. И они поддерживают числа с плавающей точкой самым общим способом: с указанными пользователем значениями ширины для показателя степени и значения и.
Сказав все это, все, что нам нужно сделать, это спросить решателя, что будет преобразование в ваш конкретный формат, учитывая число 1.76
. Вот как эта проблема написана на языке SMT-Lib:
(set-option :produce-models true)
(define-fun x () (_ FloatingPoint 3 7)
((_ to_fp 3 7) roundNearestTiesToEven (/ 176.0 100.0)))
(check-sat)
(get-value (x))
Это язык, похожий на шутки, как вы можете видеть. Тип с плавающей точкой, о котором вы говорите, (несколько странно) записан как (_ FloatingPoint 3 7)
. Это означает, что у нас есть 3-битные экспоненты и 7-битные для значащих, , включая скрытый бит. Дополнительный 1-бит для знака всегда есть, поэтому он явно не упоминается.
Преобразование выполняется с помощью функции (_ to_fp 3 7)
, которая преобразует данный натуральный в соответствующий формат. Обратите внимание, что он, как обычно, использует режим округления, и я выбрал общий режим roundNearestTiesToEven
; но вы можете выбрать любой из пяти режимов округления IEEE754. См. Описание логики с плавающей точкой для деталей. Наконец, рациональное число 1.76
записывается как (/ 176.0 100.0)
.
Мы сказали, что решатель должен производить модели в самой первой строке. Вызов (check-sat)
говорит: «Иди и найди модель для всех моих ограничений». И в последней строке мы запрашиваем значение нашего числа с плавающей точкой x
.
Теперь, если вы поместите эту программу в файл, скажем a.smt2
, загрузите z3 на свой компьютер и запустите его, вы получите:
$ z3 a.smt2
sat
((x (fp #b0 #b011 #b110001)))
Что говорит нам z3, так это то, что действительно есть решение. (Помните, что вы можете наложить произвольные ограничения, чтобы система могла вообще не иметь решения; в этом случае вы получили бы ответ unsat
.) Чем он говорит нам, каково значение x
. И вы можете щуриться и посмотреть формат, как вы просили:
0 011 110001
Итак, вот так, вы представляете число 1.76 в вашем конкретном формате с плавающей запятой.
Решатели SMT довольно удивительны, и они могут делать волшебные вещи; включая бесплатное преобразование в любой конкретный формат с плавающей запятой, который у вас может быть!