fp - float to Int8 conversion

[LeventErkok]

[I think this is similar to #114; but GitHub doesn't allow me to re-open issues.]

Another conversion benchmark. This time the SP value 5.8336496e-2, which is expressed as the rational 244681 / 4194304, converted to an 8-bit signed integer using RNE. Result should be 0; but Z3 is producing 1:

(set-option :produce-models true)
(set-logic QF_FPBV)
(define-fun s10 () (_ BitVec 8) #x00)
(define-fun s8 () RoundingMode roundNearestTiesToEven)
(define-fun s2 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 244681 4194304)))
(declare-fun s0 () (_ FloatingPoint  8 24))
(declare-fun s1 () (_ BitVec 8))
(assert ; no quantifiers
   (let ((s3 (fp.eq s0 s2)))
   (let ((s4 (fp.isNaN s0)))
   (let ((s5 (fp.isInfinite s0)))
   (let ((s6 (or s4 s5)))
   (let ((s7 (not s6)))
   (let ((s9 ((_ fp.to_sbv 8) s8 s0)))
   (let ((s11 (ite s7 s9 s10)))
   (let ((s12 (= (bvcomp s1 s11) #b1)))
   (let ((s13 (and s3 s12)))
   s13))))))))))
(check-sat)
(get-value (s1))

Z3 says:

sat
((s1 #x01))

The correct answer should be 0.

[wintersteiger]

This is now fixed in unstable. In case there are more similar bugs I'll keep the issue open for now.

[LeventErkok]

I'm still getting failures. The following one is pretty much the same as before, this time converting the single-precision value (/ 11459215 16777216), which is equivalent to 0.68302244; to a signed 8-bit integer. The result should be 1:

(set-option :produce-models true)
(set-logic QF_FPBV)
(define-fun s10 () (_ BitVec 8) #x00)
(define-fun s8 () RoundingMode roundNearestTiesToEven)
(define-fun s2 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 11459215 16777216)))
(declare-fun s0 () (_ FloatingPoint  8 24))
(declare-fun s1 () (_ BitVec 8))
(assert
   (let ((s3 (fp.eq s0 s2)))
   (let ((s4 (fp.isNaN s0)))
   (let ((s5 (fp.isInfinite s0)))
   (let ((s6 (or s4 s5)))
   (let ((s7 (not s6)))
   (let ((s9 ((_ fp.to_sbv 8) s8 s0)))
   (let ((s11 (ite s7 s9 s10)))
   (let ((s12 (= (bvcomp s1 s11) #b1)))
   (let ((s13 (and s3 s12)))
   s13))))))))))
(check-sat)
(get-value (s1))

Alas, Z3 says:

sat
((s1 #x00))

[wintersteiger]

I've given to_sbv and to_ubv a bit of a makeover. My regression tests pass, but that doesn't say much. I'll keep this issue open for now.

[LeventErkok]

I think it's getting there, but not quite! The following converts the single-precision float 0.5268265 to an unsigned-32 bit value:

(set-option :produce-models true)
(set-logic QF_FPBV)
(define-fun s10 () (_ BitVec 32) #x00000000)
(define-fun s8 () RoundingMode roundNearestTiesToEven)
(define-fun s2 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 4419341 8388608)))
(declare-fun s0 () (_ FloatingPoint  8 24))
(declare-fun s1 () (_ BitVec 32))
(assert
   (let ((s3 (fp.eq s0 s2)))
   (let ((s4 (fp.isNaN s0)))
   (let ((s5 (fp.isInfinite s0)))
   (let ((s6 (or s4 s5)))
   (let ((s7 (not s6)))
   (let ((s9 (ite (fp.isNegative s0) (bvneg ((_ fp.to_ubv 32) s8 (fp.abs s0))) ((_ fp.to_ubv 32) s8 s0))))
   (let ((s11 (ite s7 s9 s10)))
   (let ((s12 (= (bvcomp s1 s11) #b1)))
   (let ((s13 (and s3 s12)))
   s13))))))))))
(check-sat)
(get-value (s1))

The result should be 1. Alas, Z3 says:

sat
((s1 #x00000000))

[wintersteiger]

Your test cases seem to be randomly generated and you seem to be the only user for these conversions, could you perhaps generate more than one at a time? This way I loose a lot of time paging the to_*bv circuit in and out of my brain.

[wintersteiger]

The last problem is no fixed in unstable as well.

[LeventErkok]

Thanks @wintersteiger

It appears the conversions do produce correct results, but I do get a lot of "Unknown" results as well. Since my "tests" are essentially all constant folding, is that expected? For instance, the following benchmark converts the single-precision value 0.0 to a 32-bit signed-integer:

(set-option :produce-models true)
(set-logic QF_FPBV)
(define-fun s10 () (_ BitVec 32) #x00000000)
(define-fun s8 () RoundingMode roundNearestTiesToEven)
(define-fun s2 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 0 1)))
(declare-fun s0 () (_ FloatingPoint  8 24))
(declare-fun s1 () (_ BitVec 32))
(assert
   (let ((s3 (fp.eq s0 s2)))
   (let ((s4 (fp.isNaN s0)))
   (let ((s5 (fp.isInfinite s0)))
   (let ((s6 (or s4 s5)))
   (let ((s7 (not s6)))
   (let ((s9 ((_ fp.to_sbv 32) s8 s0)))
   (let ((s11 (ite s7 s9 s10)))
   (let ((s12 (= (bvcomp s1 s11) #b1)))
   (let ((s13 (and s3 s12)))
   s13))))))))))
(check-sat)

Z3 is responding Unknown for this input. Is that expected? Perhaps a constant-folding optimization is not happening for some reason?

[wintersteiger]

Unknowns are only expected when real numbers are involved or when a timeout expires. This looks like a bug in the FP to BV conversion where an illegal intermediate term is created somewhere.

[wintersteiger]

This is now fixed in unstable, there shouldn't be any unknowns anymore as long as fp.to_real is not present.

[wintersteiger]

Were there any other issues with to_*bv, or does it look stable enough to close this issue?

[LeventErkok]

@wintersteiger Yes, conversions seem to be working fine now. I think it'd be fine to close this ticket.

One current issue I have is regarding fp.rem: For DP inputs, z3 really takes a long time to reduce the results, with simple constant values. I'd be happy to provide a benchmark if you'd like to take a look. (I haven't seen any incorrect outputs, but some cases really run way too long.)

[wintersteiger]

That sounds good, thanks for checking!

fp.rem is one of those cases... if you have an actual application that uses this operation to achieve something meaningful, then I'd be happy to spend some time on it, but if it's randomly generated test cases then I'd rather spend my time on something else. If they appear somewhere along the line of an encoding of programs, but nothing really depends on them, you could try to replace them with just uninterpreted functions as a crude abstraction which will work if there's really nothing that depends on the output of fp.rem.

Z3 does propagate those values (see occurrences of mk_propagate_values_tactic in qffp_tactic.cpp), but by default it's limited to avoid blow-up on other problems. It might be worth checking why it doesn't propagate your values though.

If you do have more than 1 sharable benchmark with a meaningful purpose, please do consider collecting them so we can add them to SMT-LIB!

[LeventErkok]

I do have a bunch of benchmarks for fp.rem; alas I think they all fail the "meaningful" test. They are part of a regression suite, and largely synthetic; making sure that what Z3 produces on constants is the same on what we internally compute via constant-folding.

I'll ping if I have a real use case for it in the future. Most likely that use case will have true symbolic floats instead of constants, so I'm not sure if it'll help address the constant-propagation code. But as you mentioned, I suppose this is hardly a high-priority item.

I'm closing this ticket as the conversions seem to be working fine right now. Thanks for all the support!