在 Z3 中支持三角函数（例如：cos、tan）答案

【问题标题】：Support of trigonometric functions ( e.g.: cos, tan) in Z3在 Z3 中支持三角函数（例如：cos、tan）
【发布时间】：2018-12-28 05:09:39
【问题描述】：

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

【问题讨论】：

【解决方案1】：

SMT 求解器通常不支持超越数和三角函数。

正如Christopher 指出的（谢谢！），Z3 确实支持三角函数和超越函数；但支持相当有限。（实际上，这意味着您不应该期望 Z3 决定您向其抛出的每一个公式；在复杂的情况下，它最有可能简单地返回 unknown。）

另外，请注意 Z3 的优化求解器不处理非线性方程；所以你将无法优化它们。对于这类优化问题，传统的 SMT 求解器并不是正确的选择。

但是，如果您对 δ-可满足性（允许一定的误差因子）感到满意，那么请查看 dReal，它可以处理三角函数：http://dreal.github.io/ 然而，据我所知，它没有'不执行优化。

【讨论】：

次要细节：Z3 确实支持三角函数和超越函数，但这种支持非常有限，可能对优化问题没有用处。另见link.springer.com/chapter/10.1007%2F978-3-642-38574-2_12
谢谢@ChristophWintersteiger，我不知道有这行。编辑了我的答案以反映 Z3 中的最新技术。三角函数是否通过 Python API 公开？