在Z3-Python中构建泰勒展开式三角函数并实现存在性查询

问题描述 #

需要在Z3中实现余弦（cos）和正弦（sin）的近似函数，用于执行类似Exists y. 0<=approx_cos(y)<=1的存在性查询。已知三角函数相关的非线性实数算术（NRA）问题通常不可判定，因此计划基于泰勒展开实现近似计算，但现有代码仅能计算特定角度的余弦值，无法用于约束查询。同时询问Z3是否提供内置阶乘操作。

现有计算代码：

from z3 import *
import math

def calculate_cosine(angle):
    solver = Solver()
    result = Real('result')

    # 余弦泰勒展开式（可扩展项如"+ angle**8/40320"）
    solver.add(result == 1 - angle**2/2 + angle**4/24 - angle**6/720)

    if solver.check() == sat:
        model = solver.model()
        cosine = model[result]
        return cosine

    return None

angle = math.pi / 8  # 弧度制角度
cosine = calculate_cosine(angle)
print(cosine)

解决方案 #

1. 构建可用于NRA查询的approx_cos函数

要让函数能被Z3求解器处理，无需在函数内创建Solver实例，直接返回泰勒展开的表达式即可，这样就能将其嵌入约束或量词中：

from z3 import *
import math

def approx_cos(angle):
    # 泰勒展开前几项，可根据精度需求增加更多项
    return 1 - (angle**2)/2 + (angle**4)/24 - (angle**6)/720

# 执行存在性查询示例
y = Real('y')
solver = Solver()
# 添加约束：0 ≤ approx_cos(y) ≤ 1
solver.add(And(approx_cos(y) >= 0, approx_cos(y) <= 1))

if solver.check() == sat:
    print("满足条件的y值：", solver.model()[y])
else:
    print("无解")

若要处理更大范围的角度（泰勒展开仅在0附近精度较高），可利用余弦的周期性、奇偶性优化函数，通过If语句将角度映射到近似区间：

def approx_cos(angle):
    pi = RealVal(math.pi)
    # 利用周期性2π，将角度映射到[0, 2π)
    mod_angle = angle % (2 * pi)
    # 进一步映射到[-π, π]，利用余弦奇偶性减少计算误差
    clamped_angle = If(mod_angle > pi, mod_angle - 2 * pi, mod_angle)
    
    return 1 - (clamped_angle**2)/2 + (clamped_angle**4)/24 - (clamped_angle**6)/720

2. Z3的阶乘操作

Z3没有内置的阶乘函数，可通过两种方式处理：

• 固定阶乘值：对于泰勒展开中用到的2!、4!、6!等固定值，直接使用常量（如2、24、720），避免求解器处理额外约束，效率更高。
• 自定义递归阶乘：若需要动态计算阶乘，可递归定义，但递归函数可能影响求解器性能，仅适合简单场景：

def z3_factorial(n):
    return If(n == 0, 1, n * z3_factorial(n - 1))

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