fpRealToFP and fpToReal fail on trivial problems

[SamPruden]

See: https://stackoverflow.com/questions/75186194

Even trivial usage of fpRealToFP and fpToReal cause an unknown result. I haven't yet seen these conversions work under any circumstances.

>>> import z3
>>> r = z3.Real("r")
>>> f = z3.Const("f", z3.Float32())
>>> z3.solve(f > z3.fpRealToFP(z3.RNE(), r, z3.Float32()))
failed to solve
>>> z3.solve(z3.fpToReal(f) > r)
failed to solve

According to an answer by Alias on the linked SO question, this fails in Z3 but works in CVC5.

(set-logic ALL)
(set-option :produce-models true)
(declare-fun r () Real)
(declare-fun f () (_ FloatingPoint 8 24))
(assert (fp.gt f ((_ to_fp 8 24) roundNearestTiesToEven r)))
(check-sat)
(get-model)

z3 responds unknown, but cvc5 does much better on it:

$ cvc5 a.smt2
sat
(
(define-fun r () Real (- 1.0))
(define-fun f () (_ FloatingPoint 8 24) (fp #b0 #b11111110 #b11111111111111111111111))
)

[NikolajBjorner]

a couple of issues.

• A bug in building terms when there was a model, throws internal exception and handled as "unknown".
• fp.to_real creates terms with powers of 2. It is ill handled. It could be improved. So far a simple filter works for this example. The power-of-two expressions are not needed for the base example.

[NikolajBjorner]

The model appears to be incorrect.

[NikolajBjorner]

I am going to close this for now as resolved:

• there was a bug in encoding of to_fp that created wrong models. It was fixed.
• there was no support for exponentiation / powers in the solver to handle the encoding for to_fp. There is now a starting point for generating constraints on the fly for exponentiation and power operators. While it is highly incomplete it can with some luck apply to some of the cases generated by to_fp.

CVC5 uses a different approach for enforcing to_fp constraints. It is very possible better as it appears to expand axioms on the fly instead of using a one-shot encoding into arithmetic. On the other hand, it appears also incomplete relative to the semantics of to_fp form what I could see. The corner cases may not manifest in standard use cases (and what is a standard use case for to_fp? It seems it wasn't well used prior to this report).

There is a potentially nice project involved in handling other dynamic axioms for powers/exponentiation. It is self-contained and good entry point for someone interested in tinkering with internals while diving into approaches for handling non-linear functions.

It is encapsulated here:
https://github.com/Z3Prover/z3/blob/master/src/math/lp/nla_powers.cpp

There is good quality literature already on one approach to creating polynomial approximations.