Z3 Python API中扩展欧几里得算法建模触发无限循环求助

核心问题根源 #

• 无限循环的直接原因是Python对Z3 If函数的急切求值：Z3的If是普通Python函数，调用时会先完整计算所有传入参数，再执行分支选择。你在If的递归分支中直接写的extended_euclid(b, a % b)会被Python立即执行，完全忽略b == 0的判断，直接触发Python层面的无限递归，根本不会进入Z3的解析阶段。
• 当输入的b是Z3符号变量（非具体Python整数）时，b == 0返回的是Z3布尔表达式，不是Python原生的True/False，哪怕用Python三元表达式做分支，也会永远走到递归分支，继续触发无限调用。

实现逻辑错误 #

• 重复调用三次递归函数分别取d、x1、y1，属于无意义的重复计算，即使不无限递归也会导致三次重复的递归流程，效率极低。
• 基例分支中对q的赋值完全多余且错误：b=0时不需要计算商q，你写的If(b == 0, 1, a // b)中基例赋值的1没有任何逻辑作用。
• 代码中print s.sexpr()是Python2语法，Python3环境下需要改为print(s.sexpr())。

Z3递归建模的正确方案 #

不能依赖Python运行时递归来生成Z3符号表达式，需要用Z3原生的递归函数声明+公理定义：

1. 先声明递归函数的输入输出类型
2. 用全称量词定义基例、递归步的约束公理
3. 将公理加入求解器，由Z3自行推导递归规则

修正示例代码 #

from z3 import *

# 声明Z3递归函数：输入两个整数，返回三元组(d, x, y)
# Z3原生不支持直接返回三元组，用3个Int输出表示结果
ext_euclid = Function(
    'ext_euclid',
    IntSort(), IntSort(),  # 入参a, b
    IntSort(), IntSort(), IntSort()  # 出参d, x, y
)

a, b = Ints('a b')
d, x, y = Ints('d x y')
s = Solver()

# 定义递归公理
# 基例：b=0时，返回(a, 1, 0)
s.add(ForAll([a], ext_euclid(a, 0) == (a, 1, 0)))

# 递归步：b≠0时的规则
q, x1, y1 = Ints('q x1 y1')
s.add(ForAll([a, b, q, x1, y1],
             Implies(
                 And(
                     b != 0,
                     q == a // b,
                     ext_euclid(b, a % b) == (d, x1, y1)
                 ),
                 ext_euclid(a, b) == (d, y1, x1 - y1 * q)
             )))

# 添加测试约束：验证gcd(a,b)=1的场景
s.add(ext_euclid(a, b) == (1, x, y))
s.add(a != 0, b != 0)

print(s.check())
print(s.model())

注：如果Z3在解析全称量词时出现无限展开，可按需开启匹配模式，或使用Fixpoint引擎处理递归定义的函数。

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