z3 - Z3 python 对待 x**2 与 x*x 不同？

Question

Z3 Python 接口似乎不喜欢 ** 运算符，它可以处理 x*x 但不能处理 x**2 如下例所示

>>> x,y = x,y=Reals('x y')
>>> z3.prove(Implies(x -6 == 0,x**2 -36 == 0))
failed to prove
[x = 6]
>>> z3.prove(Implies(x -6 == 0,x*x -36 == 0))
proved

Answer 1

您可能在 Linux 或 OSX 上使用 4.3.0 版。4.3.0 版在这些平台上存在配置问题。如果是这样的话，我建议你下载4.3.1版本。4.3.1 版将在 Linux 和 OSX 上证明这两个查询。在 4.3.0 版中，Linux 和 OSX 默认不启用自动配置。因此，Z3 将始终使用对非线性算术不完整的通用求解器，也不支持幂运算符。启用自动配置后，Z3 检测到这两个问题在非线性实数算术片段中，并切换到nlsat 求解器。

顺便说一句，要在 4.3.0 版本上手动启用自动配置，您可以使用命令z3.set_option(auto_config=True).