FP to real and back conversions don't seem to be operational about z3 HOT 4 CLOSED

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.

from z3.

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.

from z3.

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.

from z3.

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.

from z3.