z3 - Z3 可以处理正弦函数和指数函数吗

Question

基于对 的一些非线性约束$a_k$,$b_k$，我必须找到以下傅立叶级数表达式的可行集：

$ x(t)= {a_0+ \sum_{k=1}^{\infty}   (a_k\cos(2\pi f_0 kt)+(b_k\sin(2\pi f_0 kt))}

而约束$a_k$,$b_k$和$a_0$是

$ L \leq a_0 \leq U $

$ Lower_bound \leq a_k^2+b_k^2 \leq Upper_bound

我可以用 Z3 做到这一点吗？

除此之外，我可以将 Z3 用于具有复数幂的指数函数，例如在傅立叶变换表达式中。

Answer 1

不幸的是，Z3 还不支持超越函数，例如sin,cos和指数函数。当前版本只能处理非线性多项式约束。您可以考虑MetiTarski 定理证明器。顺便说一句，MetiTarski 使用 Z3 来解除非线性多项式约束。