我知道 Z3 对非线性算术有一些支持，但想知道扩展到什么范围？是否可以指定支持和不支持（或可能超时）哪些类别的非线性算术？提前了解这些将帮助我尽早放弃我的任务。
似乎不支持与电源相关的内容，如下所示
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 可以处理可以简化为数字的指数。这是一个example http://rise4fun.com/Z3Py/woms,
x = Real('x')
y = Real('y')
solve(y == 3, x**y == 2)
在此示例中，y in x**y被重写为3在预处理步骤期间。经过预处理后，nlsat http://research.microsoft.com/en-us/um/people/leonardo/files/IJCAR2012.pdf调用非线性多项式实数运算的求解器。
关于非线性整数运算，请参见这个相关帖子 https://stackoverflow.com/questions/13898175/how-does-z3-handle-non-linear-integer-arithmetic/13898524#13898524.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
