FloatingPointNumber returns a floating-point number as represented in a bitvector. We switched to this, as some solvers do not return real numbers for floating-point numbers.
However, it is often still possible to provide the real representation for a FloatingPointNumber, which can help tools that can't translate them back on their own.
Also, the main solver that caused the switch back then, Bitwuzla, added support for fp-numbers to their real representations a while back due to our request.
FloatingPointNumberreturns a floating-point number as represented in a bitvector. We switched to this, as some solvers do not return real numbers for floating-point numbers.However, it is often still possible to provide the real representation for a
FloatingPointNumber, which can help tools that can't translate them back on their own.Also, the main solver that caused the switch back then, Bitwuzla, added support for fp-numbers to their real representations a while back due to our request.