[SMT-COMP] QF_FP, min and zeros

[Martin Nyx Brain]

On Thu, 2017-04-20 at 17:45 +0200, François Bobot wrote:
> Hi everyone,
> 
> 	We wonder what is the semantic of fp.min and fp.max:
> 
> [RW10] Philipp Ruemmer and Thomas Wahl.
>           An SMT-LIB Theory of Binary Floating-Point Arithmetic.
> 
> 
> and
> 
> [BTRW15] Martin Brain, Cesare Tinelli, Philipp Ruemmer, and Thomas Wahl.
>             An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic
>             Technical Report, 2015.
> 
> 
> disagree on min(-0,+0), the first gives -0 the second is uninterpreted.

The second is partially interpreted to give one of the two inputs.

This was an issues with the draft that was fixed in the final version.

[ Lengthy tedious justification : IEEE-754 2008 allows both because
min / max weren't in IEEE-754 1985 but were implemented by most vendors
so the standardisation was retroactive and they wanted to be inclusive.
IIRC the two "obvious" implementations:

((x <  y) || (isnan(x))) ? y : x;
((x <= y) || (isnan(x))) ? y : x;

have different behaviours.  Worse, there is actual variation between
common architectures, even between different FPUs on the same chip (x87
vs. SSE on x86) so compiler flags can change the behaviour of the code.
Thus fixing one behaviour in the SMT-LIB semantics would be fixing one
reference implementation and conflict with the idea of being a
formalisation of the IEEE standard rather than particular
implementations. ]

>  Moreover 
> min-has-no-other-solution-13472.smt2 from Wintersteiger's benchmark says that min(-0,+0) is +0.

I suspect this is an artefact of the hardware Wintersteiger used.  IIRC
his benchmarks were produced as this was being finalised.

> We prefer the one of BTRW15 which correspond to IEEE, but in that case SMTCOMP should be fixed.

Yes.


> As a side note, Wintersteiger is great and invaluable as a set of unit tests, but it should not be 
> used for the competition. But perhaps it will not since it is crafted.

IMHO It rather depends on what you want the competition to assess.


Cheers,
 - Martin