Rounding of to_fp from signed bit-vectors

[Christoph Wintersteiger]

The definiton of the conversion function from signed bit-vectors to floats is this:

```

  o ((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb))

    Let b in [[(_ BitVec m)]] and let n be the signed integer represented by b
    (in 2's complement format).
    [[(_ to_fp eb sb)]](r, b) = +/-infinity if n is too large/too small to be
    represented as a finite number of [[(_ FloatingPoint eb sb)]];
    [[(_ to_fp eb sb)]](r, x) = y otherwise, where y is the finite number
    such that [[fp.to_real]](y) is closest to n according to rounding mode r.

```

And `QF_FP/schanda/spark/zeros_consistent_4.smt2` is thusly:

```

(set-logic QF_FP)
(set-info :source |SPARK inspired floating point problems by Florian Schanda|)
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun rm1 () RoundingMode)
(define-fun a () Float32 ((_ to_fp 8 24) rm1 (_ bv0 32)))
(assert (not (fp.isPositive a)))
(check-sat)
(exit)

```

This benchmark is tagged as unsat, but if the rounding mode is to-negative, shouldn't the float conversion return a -zero? 

Z3 has been saying +zero for all rounding modes for a long time, so I'm sure there was a reason, I just can't remember it :-)

Thanks,

Christoph

[Levent Erkok]

When the conversion is exact (which in this case it is), the rounding-mode doesn’t come into play, right? So, +zero would be the correct answer, since there’s no rounding necessary.

-Levent.

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/9816e658-0a5a-4280-beb1-f2b50b731383n%40googlegroups.com.

[Mak Andrlon]

That's not why. According to section 6.3 "The sign bit" of IEEE 754-2019, if the rounding mode is roundTowardNegative (round towards negative infinity), then 1.0 - 1.0 = -0.0, despite the difference being exact.

This behavior of int-to-float conversion is correct, however. The description of "formatOf-convertInt" in section 5.4 states that "The signs of integer zeros are preserved. Integer zeros without signs are converted to +0."

Mak

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/04D6B5F3-985F-418C-8D65-2332FD581D97%40gmail.com.

[Christoph Wintersteiger]

Thanks for the pointer, Mak! I had forgotten that this exception is right there in '754. 

Christoph