Z3-Python自定义Complex类型使用Exists量词触发Invalid bounded variables错误

• 你使用的Complex类型是基于Python实现的自定义封装类，本质是把实部、虚部两个Z3原生数值变量打包成一个容器，Z3内置的Exists、ForAll量词仅识别原生Z3变量实例，无法识别自定义类对象，直接传入Complex实例会被判定为非法绑定变量。
• Z3量词对绑定变量列表的格式要求为一维扁平结构，不支持嵌套列表，所以传入[[x.r, x.i], [y.r, y.i]]这类嵌套结构也会触发变量合法性校验报错。

方案1：封装量词适配层（轻量方案） #

你可以保留现有复数类的实现，仅对量词接口做封装，上层使用时仍按ComplexExists([x,y], phi)的逻辑传入复数实例列表，内部自动把实部、虚部变量打平为一维列表传入Z3原生量词，上层使用完全感知不到底层打平逻辑，符合预期的使用习惯：

def ComplexExists(complex_vars, phi):
    bounded_vars = []
    for c in complex_vars:
        bounded_vars.append(c.r)
        bounded_vars.append(c.i)
    return Exists(bounded_vars, phi)

# 上层使用方式符合逻辑预期
x = Complex('x')
y = Complex('y')
l_1 = (-1000.5 == x*x)
l_2 = (y == x)
phi = Implies(l_1, l_2)
solve(ComplexExists([x, y], phi))

方案2：用Z3代数数据类型定义复数（彻底方案） #

如果你需要Z3原生识别复数类型，可以用Z3的代数数据类型(ADT)直接定义复数结构，定义完成后Z3可直接识别复数变量实例，支持直接传入量词：

# 定义复数ADT
Complex = Datatype('Complex')
Complex.declare('mk_complex', ('r', RealSort()), ('i', RealSort()))
Complex = Complex.create()

# 自定义运算逻辑（比如相等、乘法等，按需实现）
def complex_eq(a, b):
    return And(Complex.r(a) == Complex.r(b), Complex.i(a) == Complex.i(b))

def complex_mul(a, b):
    return Complex.mk_complex(
        Complex.r(a)*Complex.r(b) - Complex.i(a)*Complex.i(b),
        Complex.r(a)*Complex.i(b) + Complex.i(a)*Complex.r(b)
    )

# 使用时直接定义复数变量，可直接传入量词
x = Const('x', Complex)
y = Const('y', Complex)
solve(Exists([x], complex_eq(x, Complex.mk_complex(1, 0))))

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