[SMT-COMP] QF_FP, min and zeros

[François Bobot]

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
-------------- next part --------------
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :source |Christoph M. Wintersteiger (cwinter at microsoft.com). Randomly generated floating-point testcases.|)
; Rounding mode: to zero
; Precision: double (11/53)
; X = -zero {- 0 -1023 (-0)}
; Y = +zero {+ 0 -1023 (0)}
; -zero m +zero == +zero
; [HW: +zero] 

; mpf : + 0 -1023
; mpfd: + 0 -1023 (0) class: +0
; hwf : + 0 -1023 (0) class: +0

(set-logic QF_FP)
(set-info :status unsat)
(define-sort FPN () (_ FloatingPoint 11 53))
(declare-fun x () FPN)
(declare-fun y () FPN)
(declare-fun r () FPN)
(assert (= x (fp #b1 #b00000000000 #b0000000000000000000000000000000000000000000000000000)))
(assert (= y (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000)))
(assert (= r (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000)))
(assert  (not (= (fp.min x y) r)))
(check-sat)