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在预处理步骤期间x**y重写in 3.预处理后,调用非线性多项式实数算法的nlsat求解器.关于非线性整数运算,请参阅此相关文章.