在Z3中支持三角函数(例如: cos，tan)

Question

我想用Z3来优化一组方程。这里的问题是，我的方程是非线性的，但最重要的是，它们确实有三角函数。在z3中有没有办法解决这个问题呢？我正在使用z3py应用编程接口。