我正在尝试学习 Z3，但下面的例子让我感到困惑：
from z3 import *
a = Int("a")
b = Int("b")
print(solve(2**a <= b))
print(solve(a > 0, b > 0, 2**a <= b))
我希望它返回“[a = 1, b = 2]”，但它反而返回“未能解决”。
为什么不能解决？
是否可以在 Z3 中使用幂和对数进行计算？我如何找到一个数字的二进制字符串表示的长度（log base 2）？
【问题讨论】：
长话短说，z3（或一般的 SMT 求解器）无法处理这样的非线性约束。求幂/对数等很难处理，并且没有针对整数的决策程序。即使超过实数，它们也难以处理。也就是说，求解器将应用一些启发式方法，这些方法可能有效，也可能无效。但是对于这些类型的限制，SMT 求解器并不是正确的工具。
有关 z3 中非线性算术的较早答案，请参阅此答案：https://stackoverflow.com/a/13898524/936310
如果您有兴趣，这里有更多详细信息。首先，在 SMTLib 或 z3 中没有整数的幂运算符。如果您查看生成的程序，您会发现它实际上超过了实际值：
from z3 import *
a = Int("a")
b = Int("b")
s = Solver()
s.add(2**a <= b)
print(s.sexpr())
print(s.check())
打印出来：
(declare-fun b () Int)
(declare-fun a () Int)
(assert (<= (^ 2 a) (to_real b)))
unknown
注意转换为to_real。 ^ 运算符自动创建一个实数。解决这个问题的方法是求解器是否可以提出一个实数的解，然后检查结果是否为整数。让我们看看如果我们尝试使用Reals 会发生什么：
from z3 import *
a = Real("a")
b = Real("b")
s = Solver()
s.add(2**a <= b)
print(s.check())
print(s.model())
打印出来：
sat
[b = 1, a = 0]
太棒了！但你也想要a > 0，b > 0；所以让我们补充一下：
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())
打印出来：
unknown
所以，求解器也无法处理这种情况。你可以玩弄战术（qfnra-nlsat），但一般来说不太可能处理这类问题。再次，请参阅https://stackoverflow.com/a/13898524/936310 了解详情。
【讨论】：