fp.min/fp.max does not work correctly for -0/+0

[LeventErkok]

For inputs +0/-0, fp.min and fp.max seem to be doing the "wrong" thing currently.

For the following benchmark:

; Automatically generated by SBV. Do not edit.
(set-option :produce-models true)
(set-logic QF_FP)
; --- uninterpreted sorts ---
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
; --- skolem constants ---
(declare-fun s0 () (_ FloatingPoint 11 53)) ; tracks user variable "r"
(declare-fun s1 () (_ FloatingPoint 11 53)) ; tracks user variable "a"
(declare-fun s2 () (_ FloatingPoint 11 53)) ; tracks user variable "b"
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(assert ; no quantifiers
   (let ((s3 (fp.isZero s1)))
   (let ((s4 (fp.isNegative s1)))
   (let ((s5 (and s3 s4)))
   (let ((s6 (fp.isZero s2)))
   (let ((s7 (fp.isPositive s2)))
   (let ((s8 (and s6 s7)))
   (let ((s9 (fp.min s1 s2)))
   (let ((s10 (= s0 s9)))
   (and s5 s8 s10))))))))))
(check-sat)
(get-value (s0))
(get-value (s1))
(get-value (s2))

Z3 responds:

sat
((s0 (_ +zero 11 53)))
((s1 (_ -zero 11 53)))
((s2 (_ +zero 11 53)))

Which suggests +0, -0, +0 are solutions; but the result should actually be -0, -0, +0

A parallel benchmark for fp.max exhibits the same problem:

; Automatically generated by SBV. Do not edit.
(set-option :produce-models true)
(set-logic QF_FP)
; --- uninterpreted sorts ---
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
; --- skolem constants ---
(declare-fun s0 () (_ FloatingPoint 11 53)) ; tracks user variable "r"
(declare-fun s1 () (_ FloatingPoint 11 53)) ; tracks user variable "a"
(declare-fun s2 () (_ FloatingPoint 11 53)) ; tracks user variable "b"
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(assert ; no quantifiers
   (let ((s3 (fp.isZero s2)))
   (let ((s4 (fp.isNegative s2)))
   (let ((s5 (and s3 s4)))
   (let ((s6 (fp.isZero s1)))
   (let ((s7 (fp.isPositive s1)))
   (let ((s8 (and s6 s7)))
   (let ((s9 (fp.max s1 s2)))
   (let ((s10 (= s0 s9)))
   (and s5 s8 s10))))))))))
(check-sat)
(get-value (s0))
(get-value (s1))
(get-value (s2))

Z3 responds:

sat
((s0 (_ -zero 11 53)))
((s1 (_ +zero 11 53)))
((s2 (_ -zero 11 53)))

Which suggests the solution is -0, +0, -0; which should actually be +0, +0, -0.

[wintersteiger]

This one's actually quite tricky, because there is no clear definition of the semantics of min/max for zeros. The CPUs I tested the implementation against implements min(+0, -0) = +0 and min(-0, +0) = -0, i.e., the return value is the first argument. Neither the IEEE standard, nor the SMT theory definition gives a clear answer, but I think min(-0, +0) = min(+0, -0) = +0 will ultimately be the conclusion, so as to stay in line with a couple of other upcoming changes/clarifications to the FP theory, so I think I can make those changes now.

[wintersteiger]

Closing as fixed, feel free to reopen if there are further problems.

[LeventErkok]

Thanks for the fixes @wintersteiger; I'll test them later today.

Did you have a typo in your comment? You said:

"but I think min(-0, +0) = min(+0, -0) = +0"

You either meant max, or the result to be -0, I'm guessing?

In any case, I think the SMTLib is quite clear on min/max. The theory document is rather sparse on it, but the "reference" paper at http://www.philipp.ruemmer.org/publications/smt-fpa.pdf
clearly states the semantics of min/max in Section 3.3.9. My reading of that section is that:

  min(-0, +0) = min(+0, -0) = -0
  max(-0, +0) = max(+0, -0) = +0

I do agree, however, that the IEEE-spec itself and fmin/fmax in the C-library seem to be returning the second argument actually. (You said the "first" argument.) I tested with the following program:

#include <stdio.h>
#include <math.h>

int main()
{
     double nz = -0.0;
     double pz =  0.0;
     printf("nz sign: %d\n", signbit(nz));
     printf("pz sign: %d\n", signbit(pz));
     printf("min(-0,+0) = %8.2f, neg: %d\n", fmin(nz,pz), signbit(fmin(nz,pz)));
     printf("min(+0,-0) = %8.2f, neg: %d\n", fmin(pz,nz), signbit(fmin(pz,nz)));
     printf("min(-0,-0) = %8.2f, neg: %d\n", fmin(nz,nz), signbit(fmin(nz,nz)));
     printf("max(-0,+0) = %8.2f, neg: %d\n", fmax(nz,pz), signbit(fmax(nz,pz)));
     printf("max(+0,-0) = %8.2f, neg: %d\n", fmax(pz,nz), signbit(fmax(pz,nz)));
     printf("max(-0,-0) = %8.2f, neg: %d\n", fmax(nz,nz), signbit(fmax(nz,nz)));
     return 0;
}

[wintersteiger]

No, that was not a typo, min(-0,+0) == +0, with the justification that -0 is not smaller than +0 after conversion to reals. I had the same intuition about this as you, and implemented min/max as well as Real and FP conversions to floating-point numbers the same way, e.g.., when converting Real numbers to FP numbers and rounding towards negative, I would select -0 instead of +0, but I was outvoted and it will now always be +0.

The document you cite is a very old document and there were numerous changes to the theory since then. The current theory definition is not that clear anymore. I hear that there is a paper in the works which will assign precise semantics, but that is still in the works (and I'm not involved).

Yes, it could well have been the second argument instead of the first one. Note that your demo program does not select a particular floating-point unit, so depending on the system that you compile this on, it will either use the x87 (when in 32-bit mode) or the SSE2 unit (when in 64 bit mode), and they do not agree on some results (and I think min/max was such a discrepancy, but I can't remember exactly). On Windows, by default, it may decide to further approximate unless /fp:precise is added.

[LeventErkok]

Ah good point. Indeed http://smt-lib.org/papers/BTRW14.pdf specifically says that min/max are underspecified for +0/-0:

The two functions above are underspecified in case the input
values f, g satisfy eqε,σ (which is only when one is −0 and
the other is +0). This means that we consider as acceptable
models any structures with function families maxε,σ and
minε,σ that satisfy the specifications above, regardless of
whether they return −0 or +0 for (−0, +0), and for (+0, −0).
Although underspecification is inconvenient for implementors,
it is necessary as IEEE-754 itself allows either value to be
returned and compliant implementations do vary. For example,
on some Intel processors the result returned by the x87 and
SSE units is different.

So, just to clarify what you've implemented and for the record, can you tell me what Z3 will produce for the following calls:

 min(-0,+0)
 min(+0,-0)
 max(-0,+0)
 max(+0,-0)

We can then refer to this ticket later on in case of confusion again.

[wintersteiger]

In the current implementation (as of earlier today, unstable, see commit above), they all return +0.

[LeventErkok]

Thank you!

Let me just point out that this is in "disagreement" with the current Intel PRM for MAXPS, MAXPD, MINPS, MINPD and other floating-point instructions; which all return the "second" argument for these cases. This creates a sticking point that one has to watch out for. I wish the IEEE754 were just clear on this, alas that ship has sailed long time ago.

[wintersteiger]

Indeed, I feel much the same about this. This would have been trivial to sort out at the time IEEE754 was compiled, now it's a bit of a pain.

There aren't too many operations that suffer from this problem though. Add/sub/muk/div are almost unaffected by this (except when rounding to negative). So, we can always wrap our min/max's in if-then-elses that check for double zeros and return our preferred result, otherwise do the default. This way all different implementations can be handled soundly and it's not more expensive, as internally we'd do exactly the same.

[LeventErkok]

@wintersteiger I was surprised to see the problem remained after I did a pull; but then noticed that you fixed it in your own branch.. Would it be possible to pull the fix in to z3/unstable?

[wintersteiger]

Indeed, I just forgot to push that, it's there now.

[LeventErkok]

@wintersteiger It appears you've changed the code for this and now +0/-0 cases actually return the second argument?

In an earlier comment, you said '+0' was the chosen result in the mixed-zero cases, but it does appear you're now just returning the second argument. Wanted to double-check on that.

[wintersteiger]

Hmm, apparently I changed the code to return the second argument, but in my comments I said all cases would be +0.0. I probably mixed up this one with an fp.rem bug report at the time. In any case, I've added yet more special case handling, so this should really be +0.0 everywhere now.

[kyledewey]

This has come up during differential testing. Consider the following input:

(set-logic QF_FP)
(declare-fun x0 () Float32)
(assert (= (fp.abs x0) (fp.min (_ +zero 8 24) (_ -zero 8 24))))
(check-sat)

Z3 reports unsat here, whereas MathSAT5 reports sat, with a model that corresponds to +0.0. Z3 returns -0.0 for the fp.min operation, and since the absolute value of a value cannot be negative, Z3 ultimately reports unsat.

Based on the comment from @LeventErkok above with the snippet from the standard, I'm leaning towards Z3 being incorrect here. From the standard, it's clear that -0.0 and +0.0 are possible results for the fp.min use above. However, my interpretation is that the correct behavior is to nondeterministically pick one of the inputs, as opposed to deterministically picking a particular input, which would lead to implementation-defined behavior in the solver. The standard mentions different hardware platforms that have chosen different strategies, and so the lowest common denominator to me seems to be nondeterministic choice.

[wintersteiger]

"From the standard, it's clear..."

No it's not, that's exactly the point, regardless of which of the 3 involved standards you refer to.

Part of the SMT FP standard is to avoid as many unspecified results as possible - those create big problems for solver developers and only tiny benefits for the users. Unspecifiedness can always be recovered on the application level by guarding unspecified functions, e.g., fp.min, with an if-then-else that catches those special cases, so when we push that onto the end-user, they are responsible for picking a solver that supports uninterpreted functions; if for some reason they can't choose such a solver, then they can't have general unspecifiedness.

I had brought the min/max +-0.0 case up with them before, but so far they haven't delivered a clear solution yet, and they may well have forgotten about it. Before the current SMT FP standard was released we used a google group to discuss all these issues, it's been quiet recently but I think it's the best place to bring this one up again, The group is called smt-fp and it might require getting permissions from the owners (should be quick though).

I've taken a quick glance at BTRW14 again, and it seems like they did update the min/max paragraph to what appears like unspecifiedness, I'll confirm with them that this is indeed their intent.

[wintersteiger]

Update: There is now also BTRW15. Not sure that's the latest version though.

[wintersteiger]

Meanwhile I received confirmation, those disputed cases will indeed stay unspecified alongside the conversions to other theories, so that's what I'll implement now.

[wintersteiger]

fp.min/fp.max should now behave as defined in BTRW15. I'd be grateful if you could run your own tests and then report any new problems back to us.

[kyledewey]

Just to be absolutely sure I'm understanding what the semantics are, if we have the same test case from before (duplicated below for convenience):

(set-logic QF_FP)
(declare-fun x0 () Float32)
(assert (= (fp.abs x0) (fp.min (_ +zero 8 24) (_ -zero 8 24))))
(check-sat)

Then this should be sat, correct? As in, fp.min(+0.0, -0.0) is nondeterministically both +0.0 and -0.0?

[wintersteiger]

Yes to both, the test case is sat and it's non-deterministic.

[LeventErkok]

@wintersteiger All my tests confirm the nondeterministic behavior as you predicted. As unfortunate as that is, I do agree that this is the behavior required by the standard.