Can Z3 handle sinusoidal and exponential functions

问题:

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

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

Can I do this using Z3?

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

回答1:

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.