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を使用して非線形多項式制約を解除します。