Z3 可以处理正弦函数和指数函数吗 [英] Can Z3 handle sinusoidal and exponential functions

问题描述

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

Based on some non-linear constraints on $a_k$,$b_k$, I have to find feasible set of the following fourier series expression:

$ 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$ 的约束是

Whereas constraints on $a_k$,$b_k$ and $a_0$ are

$ L \leq a_0 \leq U $

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

我可以使用 Z3 执行此操作吗?

Can I do this using Z3?

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

In addition to this can I use Z3 for exponential functions having complex powers, e.g. in fourier transform expression.

推荐答案

遗憾的是，Z3 尚不支持 sin、cos 和指数等超越函数.当前版本只能处理非线性多项式约束.您可以考虑 MetiTarski 定理证明者.顺便说一句，MetiTarski 使用 Z3 来解除非线性多项式约束.

Unfortunately, Z3 does not have support for transcendental functions such as sin, cos and exponential yet. The current version can only handle nonlinear polynomial constraints. You may consider the MetiTarski theorem prover. BTW, MetiTarski uses Z3 to discharge nonlinear polynomial constraints.

这篇关于Z3 可以处理正弦函数和指数函数吗的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！