Z3 python 对待 x**2 与 x*x 不同? [英] Z3 python treats x**2 different than x*x?

问题描述

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

<预><代码>>>>x,y = x,y=Reals('x y')>>>z3.prove(暗示(x -6 == 0,x**2 -36 == 0))未能证明[x = 6]>>>z3.prove(暗示(x -6 == 0,x*x -36 == 0))证实

解决方案

您可能在 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).

It seems that Z3 Python interface doesn't like the ** operator , it can deal with x*x but not x**2 as shown in the example below

>>> 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

解决方案

You are probably using version 4.3.0 on Linux or OSX. Version 4.3.0 has a configuration problem on these platforms. If that is the case, I suggest you download version 4.3.1. Version 4.3.1 will prove both queries on Linux and OSX. In version 4.3.0 auto-configuration is not enabled by default on Linux and OSX. Thus, Z3 will always use a general purpose solver that is not complete for nonlinear arithmetic, nor has support for the power operator. When auto-configuration is enabled, Z3 detects that these two problems are in the nonlinear real arithmetic fragment, and switches to the nlsat solver.

BTW, to manually enable auto-configuration on version 4.3.0, you may use the command z3.set_option(auto_config=True).

这篇关于Z3 python 对待 x**2 与 x*x 不同?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！