[Question]: How to calculate upper and lower bound of floating points?

[hagozaebii]

hello

I have recently been doing floating point-related calculations in z3. While performing calculations, I learned that floating points have upper and lower limits, and when they exceed the bound, they are displayed as inf.
It seems that these upper and lower bounds are determined by ebits and sbits of the sort, but I would like to know how the upper and lower bounds are determined given the ebits and sbits. I tried to check the information on Wikipedia, but I couldn't figure it out. To be more specific,

>>> FPVal(-3.75, FPSort(2,3))
-oo
>>> FPVal(-3.74, FPSort(2,3))
-1.75*(2**1)
>>> FPVal(3.75, FPSort(2,3))
+oo
>>> FPVal(3.74, FPSort(2,3))
1.75*(2**1)

Likewise, when ebits is 2 and sbits is 3, the upper and lower limits appear to be 3.75 and -3.75, respectively. How can these be calculated with formulas?

Thanks for reading.

[LeventErkok]

Perhaps https://www.h-schmidt.net/FloatConverter/IEEE754.html will help? In any case, this really has nothing to do with z3. Perhaps try the relevant stack-overflow forum: https://stackoverflow.com/questions/tagged/floating-point

[wintersteiger]

The number of ebits/sbits just fixes the precision of the numbers. If a result is outside the numbers that can be represented, they are rounded to a representable one (according to one of five rounding modes). No upper/lower bounds are computed. Z3 implements floating point numbers as defined by the SMT standard, which is equivalent to IEEE754 for the combinations of ebits/sbits defined there, so functions on floats, rounding modes, and representable numbers have equivalent semantics. Thus, almost all tutorials on floating point numbers found on the internet also apply here :-)