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

[Christoph Wintersteiger]

Regarding fp.min/fp,max in the benchmarks and what's implemented in Z3, please see also this discussion:
https://github.com/Z3Prover/z3/issues/68

I agree that we have to fix those to some value, or maybe the second argument. Users can always wrap them in ITEs that select whatever they want for those cases (and internally most of us would do the same kind of wrapping inside our solvers anyways).

For the demo track, I think it would be fair to simply exclude that benchmark, so we don't have to find a community consensus right away. 

Cheers,
Christoph

Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter


Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB 

-----Original Message-----
From: Alberto Griggio [mailto:griggio at fbk.eu] 
Sent: 10 June 2015 16:27
To: Christoph Wintersteiger; smtcomp-discussion at lists.sourceforge.net; smt-lib (smt-lib at cs.nyu.edu)
Cc: Martin Brain; Schanda Florian; Florian Lapschies; Pascal.Fontaine at inria.fr; Philipp Ruemmer (philipp.ruemmer at it.uu.se); wahl at ccs.neu.edu
Subject: Re: FP demo track at SMT-COMP

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.