[SMT-COMP] QF_FP, min and zeros
cwinter at microsoft.com
Thu Apr 20 12:58:31 EDT 2017
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).
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
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
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.
[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,
More information about the SMT-COMP