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

[Alberto Griggio]

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. The reference paper [BTRW15] argues that
this is necessary to be fully compliant with IEEE. 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?

Alberto



[BTRW15] Martin Brain, Cesare Tinelli, Philipp Ruemmer, and Thomas Wahl.
          An Automatable Formal Semantics for IEEE-754 Floating-Point 
Arithmetic
          Technical Report, 2015.