[SMT-LIB] FP demo track at SMT-COMP

[Martin Brain]

On Wed, 2015-06-10 at 17:26 +0200, Alberto Griggio wrote:
> Hello all,
> 
> >> So far, none of the submissions to SMT-COMP 2015 have select QF_FP or
> >> QF_BVFP as categories they would like to take part in:
> >>
> >> http://smtcomp.sourceforge.net/2015/participants.shtml
> >>
> >> We would like to run the floating-point demo track alongside the other
> >> competition track, i.e., starting June 14. So, if you would like to
> >> participate, please let us know as soon as possible. As Tjark said, if
> >> we don’t hear from you, your solver(s) will not take part.
> >>
> >> If you want to take a look at the latest benchmarks before committing to
> >> it, they are available on starexec in root/SMT/SMT-LIB
> >> benchmarks/2015-06-01/non-incremental/QF_FP and …/QF_BVFP.
> >
> > I was planning to submit. As I told Tjark, I did not understand that the
> > general SMTCOMP deadline was meant also for the FP demo tracks. If I'm
> > still on time, I'll try to submit mathsat by june 14.
> 
> I have a follow-up question about this. If I understand correctly,
> fp.min and fp.max are underspecified in the current standard, in the
> case the inputs are +0 and -0.

Yes.  This is only the cases min(+0,-0) and min(-0,+0) (and the
corresponding max cases).

>  The reference paper [BTRW15] argues that
> this is necessary to be fully compliant with IEEE.

The specific clause is:

<quote>
minNum(x, y) is the canonicalized number x if x < y, y if y < x, the
canonicalized number if one operand is a number and the other a quiet
NaN. Otherwise it is either x or y, canonicalized (this means results
might differ among implementations).
</quote>

Canonicalisation only applies in the case of decimal floating-point
which SMT-LIB doesn't (currently) support.

My understanding of this is that max and min were not included in the
1985 version of IEEE-754 and that different implementators made
different assumptions about what they should do.  IIRC the x87 and SSE
units on Intel chips have different behaviour, likewise:

!(x < y) ? x : y;
!(x > y) ? y : x;

have different behaviour around +0/-0.

>  To me, this seems
> like an unnecessary complication (for the same reason, I think
> bit-vector division by 0 should be specified). Regardless of this,
> however, I found at least one benchmark that seems to be misclassified
> (there might be more):
> 
>     wintersteiger/min/2066309/min-has-no-other-solution-13472.smt2
> 
> Is it too late to ask for a change in the FP standard? Fixing one return
> value for e.g. (fp.min -0 +0) would make life simpler without losing
> much IMHO, given that the underspecified semantics can still be encoded
> if someone really wants that. What do people think?

I, personally, think that we should keep the underspecified semantics as
something similar will be needed for converting from float to signed and
unsigned integers so it's not as if changing max/min will remove the
need to support these.

Benchmarks that use this aspect ... should probably be treated like
bit-vector divide by 0.

Cheers,
 - Martin