[SOLVED] Unexpected Behaviour in Z3 when working with exponentials

Unexpected Behaviour in Z3 when working with exponentials

I have the following code in which I am trying to return the value of e^x using z3. However, this code is returning y = 0

import z3

x, y = z3.Real('x'), z3.Real('y')
e = z3.RealVal(str(gmpy2.exp(gmpy2.mpfr(1)))) # or e^1, the Euler's number e
print(e)
s = z3.Solver()
s.add(x == 1134585759063987950064875850350910837993/1361129467683753853853498429727072845824)
s.add(y == e ** x)
s.check()
model = s.model()
print(model)

The output of this code is:

3397852285573806544200359339189/1250000000000000000000000000000
[x = 260488115293581/312500000000000, y = 0]

How can I fix this code?

Solution

If you add:

print(s.check())

you'll see that z3 prints:

unknown

This means that the solver wasn't able to come up with a model that is guaranteed to satisfy the constraints. (Exponentials are hard for SMT solvers: There are very good reasons for this, you can search stack-overflow for it.)

So, the model you print is irrelevant. Or, more precisely, is not guaranteed to satisfy the constraints since the solver is in unknown state.

So far as "fixing" this is concerned: You can't really. But if x is a constant, and e is a constant (already), so is e^x. Just calculate its value outside of z3, and plug it in.