Z3 支持非线性算术 [英] Z3 support for nonlinear arithmetic
问题描述
我知道 Z3 对非线性算术有一些支持,但想知道扩展到了什么?是否可以指定支持哪些类别的非线性算术而不支持(或可能会超时)?提前了解这些将有助于我尽早中止我的任务.
I understand that Z3 has some supports for nonlinear arith but wondering to what extends ? Is it possible to specify what classes of nonlinear arithmetics are supported and are not (or likely to give time out) ? Know these in advances will help me abort my task early.
似乎不支持与电源相关的东西,如下所示
Seems like power related stuff is not supported as shown below
def pow2(x):
k=Int('k')
return Exists(k, And(k>=0,2**k==x))
prove(pow2(7))
failed to prove
推荐答案
Z3 支持非线性多项式 实数运算.因此,不支持超越函数(例如,正弦和余弦)和指数函数(例如,2^x
).实际上,对于指数,Z3 可以处理可以简化为数字的指数.这是一个示例,
Z3 supports nonlinear polynomial Real arithmetic. So, there is no support for transcendental functions (e.g., sine and cosine), and exponential (e.g., 2^x
). Actually, for the exponential, Z3 can handle exponents that can be simplified to numerals. Here is an example,
x = Real('x')
y = Real('y')
solve(y == 3, x**y == 2)
在此示例中,x**y
中的 y
在预处理步骤中被重写为 3
.预处理后,nlsat 非线性求解器多项式实数算法被调用.关于非线性整数运算,请参阅这篇相关帖子.
In this example, the y
in x**y
is rewritten to 3
during a preprocessing step. After preprocessing, the nlsat solver for nonlinear polynomial real arithmetic is invoked.
Regarding nonlinear integer arithmetic, see this related post.
这篇关于Z3 支持非线性算术的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!