非线性算法的Z3支持

Question

我知道Z3对非线性空间有一些支持，但我想知道扩展了什么？是否可以指定哪些类别的非线性算法是支持的，而不(或可能给出时间)？提前知道这些将有助于我提前完成任务。

似乎不支持与电源相关的内容，如下所示

def pow2(x): 
    k=Int('k')
    return Exists(k, And(k>=0,2**k==x))


prove(pow2(7))
failed to prove

Answer 1

Z3支持非线性多项式实算法。因此，不支持先验函数(如正弦和余弦)和指数函数(如2^x)。实际上，对于指数，Z3可以处理可以简化为数字的指数。这是一个示例，

x = Real('x')
y = Real('y')
solve(y == 3, x**y == 2)

在本例中，y In x**y在预处理步骤中被重写为3。经过预处理，调用了非线性多项式实算法的nlsat求解器。关于非线性整数算法，请参见这个相关员额。