mirror of
https://git.freebsd.org/ports.git
synced 2025-05-08 03:40:46 -04:00
8 lines
560 B
Text
8 lines
560 B
Text
SymFPU is an implementation of the SMT-LIB / IEEE-754 operations in terms of
|
|
bit-vector operations. It is templated in terms of the bit-vectors,
|
|
propositions, floating-point formats and rounding mode types used. This allow
|
|
the same code to be executed as an arbitrary precision "SoftFloat" library
|
|
(although it's performance would not be good) or to be used to build symbolic
|
|
representation of floating-point operations suitable for use in "bit-blasting"
|
|
SMT solvers (you could also generate circuits from them but again, performance
|
|
will likely not be good).
|