如何在Z3 Python中使用内置三角函数求解存在性约束？

问题原因 #

你之前的代码报错是因为Z3 Python绑定中的三角函数采用大写命名，比如Cos而非小写的cos，小写名称未被识别。

正确实现方式 #

要得到满足0 ≤ cos(y) ≤ 1的具体y值，无需使用Exists量词（存在量词绑定的变量不会出现在最终模型中），直接将y作为自由变量添加约束求解即可。示例代码如下：

from z3 import *

y = Real('y')
solver = Solver()
# 添加约束：cos(y)在0到1之间
solver.add(Cos(y) >= 0, Cos(y) <= 1)

if solver.check() == sat:
    model = solver.model()
    # 获取y的具体值，启用model_completion补全变量赋值
    y_value = model.eval(y, model_completion=True)
    # 可选：转换为十进制格式输出
    print(f"y := {y_value.as_decimal(5)}")
else:
    print(solver.check())

关键说明 #

• Z3支持的三角函数包括Cos、Sin、Tan等，均为大写开头，需严格使用正确名称。
• 对于简单的超越函数约束，Z3可以返回可满足的模型（比如y=0时cos(y)=1，y=1.5708即π/2时cos(y)=0）。但复杂的非线性超越约束可能返回unknown，这是由超越算术的不可判定性决定的。
• 如果需要更精确的数值输出，可通过as_decimal(n)指定小数位数，n为保留的小数长度。

内容的提问来源于stack exchange，提问作者Theo Deep