Внедрение дробеструйной обработки для арифметики с плавающей точкой в SMT
Мне было интересно, как люди реализуют дробеструйные арифметические конструкции с плавающей точкой в решателях SMT. Существуют ли какие-либо библиотеки или средства для этого (VHDL, ...) или они реализованы с нуля? Это представляет сколько строк кода (C? C++?)?
Заранее спасибо.
2 ответа
Насколько мне известно, существует следующая реализация:
CBMC (не строго и SMT решатель, но содержит необходимые биты)
https://github.com/diffblue/cbmc/blob/master/src/solvers/floatbv/float_utils.cpp
Примерно 2KLoC в C++ (но построенный поверх служебных функций для всех операций с бит-вектором, что является еще одним 2KLoC). Я полагаю, что это было первоначально написано из книги Мюллера и Пола. ESBMC содержит форк более ранней версии этого кода.
Z3
Смотрите ответ Кристофа выше. В Z3 была более ранняя реализация прототипа, которая была "вдохновлена" реализацией CBMC, но она потеряна для глубины веков.
MathSAT
Источник недоступен, реализация "вдохновлена" CBMC и, таким образом, похожа по размеру и т. Д.
CVC4
Одна из моих веток CVC4:
https://github.com/martin-cs/CVC4/tree/floating-point-symfpu
имеет взрывной двигатель с плавающей запятой. Он написан как "автономная" библиотека (см. Src/symfpu - я бы дал полную ссылку, но github предотвращает более двух ссылок на пост...), которая будет выпущена отдельно... в ближайшее время. Он параметризован в 'back-end', так что его можно использовать в качестве библиотеки с плавающей запятой произвольной точности, генерировать выражения битовых векторов для различных решателей и т. Д. Он составляет около 3,5 КБ кода, но содержит несколько реализаций некоторых операции. Он был написан с нуля (хотя я прочитал "Руководство с плавающей точкой").
SONOLAR
Источник недоступен, я считаю, что он реализован на C++, и у меня есть ощущение, что кто-то сказал мне, что он основан на книге Мюллера и Пола.
Обратите внимание, что было предпринято множество серьезных независимых попыток (перекрестной) проверки и проверки этих реализаций. Я не буду утверждать, что все идеально (мы все еще пытаемся получить полную уверенность в отношении остатка и FMA), но вы должны обнаружить, что там нет очевидных ошибок.
Вы могли бы использовать проекты VHDL или Verilog, но... то, что делает хороший синтезируемый FPU, не является (обязательно) чем-то, что делает хорошее кодирование. Я знаю, что некоторые использовали SoftFloat в качестве источника реализаций, но подобные комментарии остаются в силе.
В решателях SMT пока не существует "многих" реализаций, но Z3 - одна из тех, которая реализует все. Код находится в fpa2bv_converter.cpp, и он довольно понятен. Для большей части кода я черпал вдохновение из книги Мюллера и Пола "Компьютерная архитектура", в которой есть глава о схемах с плавающей запятой. "Справочник по арифметике с плавающей точкой" (Мюллер и др.) Также содержит много информации / программ / схем.