Floating point exponent saturates rather than becoming infinite

[mpdn]

It seems like if the exponent of a floating point overflows, it just saturates instead of becoming (positive or negative) infinite.

Example:

import numpy as np
from z3 import *

# This does not find a solution
x = FP('x', Float32())
solve(x > 0, (x * 2) * 0.5 > x)

# But this *is* a solution and prints `True`
x = np.finfo(np.float32).max
print((x * np.float32(2)) * np.float32(0.5) > x)

[LeventErkok]

It seems the Python interface is using the default rounding mode of round-towards-zero, which causes the problem to be unsat. If you set the regular defaulting mode of nearest-ties-to-even, you get a model:

from z3 import *

print(get_default_rounding_mode())
set_default_rounding_mode(Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN)
print(get_default_rounding_mode())

x = FP('x', Float32())
solve(x > 0, (x * 2) * 0.5 > x)

This prints:

RTZ()
RNE()
[x = 1.00000095367431640625*(2**127)]

This is set in:

z3/src/api/python/z3/z3.py

Line 8679 in daf7e9e

_dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO

So, it does the "right" thing per this definition, but I do agree that the default rounding mode should be set to Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN

[mpdn]

Ah, thanks a lot. Although I don't quite get how round-to-zero causes it to not become infinite, but maybe this is me misunderstanding IEEE-754.

[LeventErkok]

@mpdn When you multiply max with 2 in RTZ, the value remains max and does not become Infinity. The easiest way to see this is to consider where the infinitely precise value remains: It's clearly between max and infinity, and RTZ says go towards zero, i.e., the result remains max. (It's funny to talk about a value being "close" to max than infinity, but the definition of overflow is very precisely defined in IEEE-754.)

You can double-check this with a C program:

#include <stdio.h>
#include <fenv.h>

int main()
{
    float f = 3.4028235e38;

    float g1 = f*2;
    printf("f = %g, g1 = %g\n", f, g1);

    fesetround(FE_TOWARDZERO);
    float g2 = f*2;
    printf("f = %g, g2 = %g\n", f, g2);
}

When I run this, I get:

f = 3.40282e+38, g1 = inf
f = 3.40282e+38, g2 = 3.40282e+38

The first one is the multiplication with the default round-to-nearest-even mode, and the second one is done in RTZ.

[wintersteiger]

Thanks @LeventErkok for the detailed explanation! The "hidden" default rounding mode can be confusing if users don't already know and expect it.

[LeventErkok]

@wintersteiger Is there a reason why the "default" mode is RTZ? I'd have expected RNE, given that's the default in pretty much everywhere else.

[wintersteiger]

I have no recollection of what I thought about it at the time I added that. It's likely that it was simply the first in the list/enum. Is the default in the other Z3 APIs RNE too?

[wintersteiger]

Apparently it's RNA in C++. shakeshead

[wintersteiger]

I will now change the default rounding mode in Python to RNE as well, see #6073. Someone else has already changed the default in the C++ API and I don't think we have another API the overloads operators.