I'm trying to learn Z3 and the following example baffles me:
from z3 import *
a = Int("a")
b = Int("b")
print(solve(2**a <= b))
print(solve(a > 0, b > 0, 2**a <= b))
I would expect it returns "[a = 1, b = 2]" but it instead returns "failed to solve".
Why cannot it be solved?
Is it possible to compute with powers and logarithms in Z3 at all? How do I find, say, the length of binary string representation of a number (log base 2)?
Long story short, z3 (or SMT solvers in general) cannot deal with non-linear constraints like this. Exponentiation/Logs etc are difficult to deal with, and there are no decision procedures for them over the integers. Even over reals they are difficult to handle. That is, the solver will apply some heuristics, which may or may not work. But for these sorts of constraints, SMT solvers are just not the right tool.
For an earlier answer on non-linear arithmetic in z3, see this answer: https://stackoverflow.com/a/13898524/936310
Here're some more details if you are interested. First, there is no power-operator for integers in SMTLib or z3. If you look at the generated program, you'll see that it's actually over real values:
from z3 import *
a = Int("a")
b = Int("b")
s = Solver()
s.add(2**a <= b)
print(s.sexpr())
print(s.check())
This prints:
(declare-fun b () Int)
(declare-fun a () Int)
(assert (<= (^ 2 a) (to_real b)))
unknown
Note the conversion to to_real. The ^ operator automatically creates a real. The way this would be solved is if the solver can come up with a solution over reals, and then checks to see if the result is an integer. Let's see what happens if we try with Reals:
from z3 import *
a = Real("a")
b = Real("b")
s = Solver()
s.add(2**a <= b)
print(s.check())
print(s.model())
This prints:
sat
[b = 1, a = 0]
Great! But you also wanted a > 0, b > 0; so let's add that:
from z3 import *
a = Real("a")
b = Real("b")
s = Solver()
s.add(2**a <= b)
s.add(a > 0)
s.add(b > 0)
print(s.check())
This prints:
unknown
So, the solver can't handle this case either. You can play around with tactics (qfnra-nlsat), but it's unlikely to handle problems of this sort in general. Again, refer to https://stackoverflow.com/a/13898524/936310 for details.