[SMT-COMP] QF_FP, min and zeros

[Christoph Wintersteiger]

That's not exactly right; min-has-no-other-solution-13472.smt2 asserts this:

(assert (= r (fp.min x y)))
(assert (and (not (= r (_ +zero 11 53))) (not (= r (_ -zero 11 53)))))

I.e., we have x/y are zeros and the result r is not +0 && not -0. The whole problem is unsatisfiable, i.e., r must be one of the zeros, but it's not known which one. I understand that this is the SMT-LIB semantics at least per BTRW15 (and that's also what's implemented in Z3). 

Cheers,
Christoph

Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | https://www.microsoft.com/en-us/research/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: smt-comp-bounces at cs.nyu.edu [mailto:smt-comp-bounces at cs.nyu.edu] On Behalf Of François Bobot
Sent: 20 April 2017 16:45
To: smt-comp at cs.nyu.edu
Cc: Bruno Marre <bruno.marre at cea.fr>
Subject: [SMT-COMP] QF_FP, min and zeros

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

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



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.


PS: starexec seems down so I have not been able to check if I have the last version of the benchmark

Thank you for the precisions,

Best,

-- 
François Bobot