I'm trying to solve simple problem which involves calculating square root, yet for some reason z3 throws an error like failed to solve or z3types.Z3Exception: model is not available
from z3 import *
x = Int('x')
y = Int('y')
solve(x > 0, y > x, y ** 0.5 == x)
from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
s.add(x > 0)
s.add(y > x)
s.add(y ** 0.5 == x)
print(s.check())
print(s.model())
What I'm doing wrong?
There are two problems here. One you can fix. Other, unfortunately not.
The first is the use of the constant 0.5. z3 tries to be helpful and coerces constants, but in this case it doesn't do what you think it should. If you try:
from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
s.add(x > 0)
s.add(y > x)
s.add(y ** 0.5 == x)
print(s.sexpr())
It'll print:
(declare-fun x () Int)
(declare-fun y () Int)
(assert (> x 0))
(assert (> y x))
(assert (= (^ y 0) (to_real x)))
Note what happened to your constant 0.5. It became 0. z3 does this because it sees y is an integer, and thus coerces the constant 0.5 to an integer, which truncates the value to 0. Clearly, this isn't what you wanted. The proper way to code this is:
s.add(y ** Q(1,2) == x)
where Q(1,2) represents the real number 1/2, i.e., 0.5. In this case, z3 will coerce y to a real value.
I should add that there's no deep/good reason why z3 behaves this way. It could've been more careful and coerced what you wrote correctly as well, alas that's not what it does. So, this isn't a bug. It's just how z3 works, something you have to keep in mind.
Having said that, if you try the above encoding, you'll notice that z3 still can't solve this problem. It'll print unknown. The reason for this is more technical, but suffice it to say that the exponentiation function is hard to reason with. It brings non-linear arithmetic into play and mixed with Integers/Reals, this leads to a theory that does not have a decision procedure.
What can you do? Well, it really depends on your what your ultimate goal is. But a good starting point is to avoid exponentiation, and cast everything in terms of multiplication instead:
s.add(y == x * x)
If you do this, you'll get:
sat
[x = 2, y = 4]
whether this'll work in all problems is hard to guess. Different problems might require different encodings. But bottom line, avoid the exponentiation operator if you can, especially when mixing reals and integers: It creates really difficult problems for SMT solvers, and you'll unlikely to get successful results when exponentiation is heavily used.