A possible problem in z3's Float to Real conversion function.

[Alex-Mathai-98]

Hi ! Before going into my problem, I wanted to first thank all the amazing contributors here for this fantastic open sourced repository. It's genuinely wonderful.

Now straight to the problem. I have been trying my best to make use of the fpToReal function at https://github.com/Z3Prover/z3/blob/master/src/api/python/z3/z3.py#L10725. However, when I try to solve even simple constraints with this function the solver returns unknown. I have detailed an example below.

from z3 import *
solver = Solver()
x = FP('x',Float32())
y = fpToReal(x)
solver.add(y == RealVal(99.2))
solver.check()

The above snippet returns unknown. Would someone be able to help me understand why this happens ? @NikolajBjorner

[LeventErkok]

Related: https://github.com/Z3Prover/z3/issues/6548. Bottom line, z3's handling of fpToReal is rather weak; even constant conversions give it hard time. In my experiments, I found cvc5 to perform better for floats; so you might try that as a fall-back if possible.

As an aside, that 99.2 can't be represented precisely as a single-precision float, so the answer you'd expect in this case would be unsat. In fact, CVC5 finds this. Note that you have to be careful with x being NaN or infinity, so the following is the equivalent smt-lib:

(set-logic ALL)
(set-option :produce-models true)
(declare-fun x () (_ FloatingPoint 8 24))
(assert (not (fp.isNaN x)))
(assert (not (fp.isInfinite x)))
(assert (= (/ 496.0 5.0) (fp.to_real x)))
(check-sat)
(get-model)

For this one z3 says unknown, but cvc5 solves it just fine and returns unsat.

If you change the number to (= (/ 495.0 5.0)), (i.e. 99), then cvc5 finds that number, but z3 still says unknown.

[Alex-Mathai-98]

@LeventErkok - thankyou so much for your detailed reply. Going forward I shall add the checks for Nan and infinity. I think the floating point logic needs some more time to mature.

I did have a follow up question though ... is there a rounding function for floats .... in which case could I do something like fpToReal(roundFunction(float)) == RealVal(99.2).

I ask this because I am guessing that this would help relax the constraints on the float variable (from exactly equal to roughly equal) and may help in getting a solution.

[LeventErkok]

Rounding makes sense when the target is a floating-point number. You probably want to convert the real to a float and then compare. Take a look at https://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml.

I think the function you want in this case is

((_ tofp eb sb) RoundingMode Real ( FloatingPoint eb sb))

[[(_ to_fp eb sb)]](r, x) = +/-infinity if x 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 x according to rounding mode r.

That is, convert the real 99.2 to a single precision float using whatever rounding mode you want, and then compare that to your float. The z3py version is called fpRealToFP.

[Alex-Mathai-98]

@LeventErkok - yes, indeed the reverse logic makes more sense. Thanks, let me try this.

[LeventErkok]

Yes; that seems to work better:

from z3 import *
solver = Solver()
x = FP('x',Float32())
solver.add(x == fpRealToFP(RNE(), RealVal(99.2), Float32()))
print(solver.check())
print(solver.model())

This prints:

sat
[x = 1.5499999523162841796875*(2**6)]

And that value is close to 99.19999694824219 as a double-precision IEEE754 number, which is probably the closest you can get under the RNE rounding. (I'm saying "probably" since I haven't manually verified that, but cvc5 produces the same result, so I think it should be good.)

[Alex-Mathai-98]

Thank you so much @LeventErkok ! I will mark this as closed now. Thanks once again.

[LeventErkok]

@NikolajBjorner might still want to take a look at it, since there’s some improvements z3 can definitely do with respect to these conversions.