FP to real and back conversions don't seem to be operational

[LeventErkok]

This is on the unstable branch.

I'm experimenting with floating-point to real (fp.to_real) and back-conversions ((_ to_fp eb sb)). It appears Z3 is always producing unknown or going away forever for queries that involve these conversions. Is something wrong with the way I've constructed the benchmarks (logic-selection comes to mind), or is this just not quite working well yet?

Here's an example benchmark that causes Z3 to run forever. (Well, I just killed it after a while)

; Automatically generated by SBV. Do not edit.
(set-option :produce-models true)
(set-logic QF_FP)
; --- uninterpreted sorts ---
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
; --- skolem constants ---
(declare-fun s0 () Real)
(declare-fun s1 () RoundingMode)
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(assert ; no quantifiers
   (let ((s2 ((_ to_fp 8 24) s1 s0)))
   (let ((s3 (fp.to_real s2)))
   (let ((s4 (distinct s0 s3)))
   s4))))
(check-sat)

And this one causes Z3 to issue unknown:

; Automatically generated by SBV. Do not edit.
(set-option :produce-models true)
(set-logic QF_FP)
; --- uninterpreted sorts ---
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
; --- skolem constants ---
(declare-fun s0 () Real)
(declare-fun s1 () RoundingMode)
(declare-fun s2 () RoundingMode)
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(assert ; no quantifiers
   (let ((s3 ((_ to_fp 8 24) s1 s0)))
   (let ((s4 ((_ to_fp 8 24) s2 s0)))
   (let ((s5 (not (fp.eq s3 s4))))
   s5))))
(check-sat)

[wintersteiger]

Floating-point constraints are usually translated first into bit-vectors and then into propositional SAT. Conversion terms from/to (non-numeral) reals translate into large non-linear constraints over the reals, which the (new, fast) purely propositional SAT solver can't handle, so it falls back to the (old, slow) SMT core that handles all theories, but is often slower. In the case of these non-linear constraints it's simply not strong enough and it either doesn't terminate or gives up early and returns unknown.

For numerals, we can get rid of those expressions altogether (and I've added another one of those in 59911f78), but for general constraints, there is no efficient method yet.

[wintersteiger]

Closing this issue as all questions are answered. There is no simple solution to the performance problems, so will require more research. Feel free to re-open if new information becomes available.

[LeventErkok]

Indeed, there isn't much point to keeping this ticket here.

I'll just note that most of the interesting floating-point verification work actually involves showing that certain operations will produce exact results. The typical approach is to take two floats, convert them to reals, do the operation with infinite precision, and turn the result back to a float using the rounding mode. Then, one shows that this result is precisely the same as just doing the corresponding operation directly on the floats without moving to reals and back. (This is the required behavior in the IEEE754 sense.)

I'd even say that this is the raison d'etre for why we want an automated floating-point logic in the first place.

Of course, none of this is criticism for Z3 or SMT. It's just that such problems are hard and more research is needed. But without proper real/float conversion support in solvers, the automation is inherently limited in its industrial use.

[wintersteiger]

You're completely right of course and we are aware of those problems. We have plans to extend the floating point reasoning in that direction, but that will take some time.