Z3 python对待x ** 2与x * x不同？
发布时间：2020-12-20 13:31:27 所属栏目：Python 来源：网络整理
导读：似乎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 解决方法 您可能在Linux或OSX上使
|
似乎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
解决方法
您可能在Linux或OSX上使用4.3.0版.版本4.3.0在这些平台上存在配置问题.如果是这种情况,我建议您下载版本
4.3.1.版本4.3.1将证明Linux和OSX上的两个查询.在版本4.3.0中,默认情况下,Linux和OSX上未启用自动配置.因此,Z3将始终使用非完整的非通用算法的通用求解器,也不支持幂运算符.启用自动配置后,Z3会检测到这两个问题都在非线性实数算术片段中,并切换到
nlsat solver.
顺便说一句,要在4.3.0版本上手动启用自动配置,您可以使用命令z3.set_option(auto_config = True). （编辑：李大同） 【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容! |