CODEWITHSUNDEEP
z3
hafizul asad
hafizul asad

Reputation: 527

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.

Upvotes: 0

Views: 761

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

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.

Upvotes: 2

Related Questions