z3 - 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)

在这个例子中，yin在预处理步骤中x**y被重写。3预处理后，调用非线性多项式实数算术的nlsat求解器。关于非线性整数算术，请参阅此相关帖子。