为何Z3在该Python代码中抛出‘sort mismatch’异常？

核心原因 #

问题出在Z3对表达式相等性比较的严格类型检查上：

• Python的in运算符会遍历列表，逐个执行x == 元素的比较
• Z3重载了表达式对象的__eq__方法，比较时会强制要求两个表达式的sort（类型）完全匹配
• 你定义的State是自定义枚举类型，和x的Bool类型属于完全不同的类型体系，无法进行类型转换合并，因此直接抛出sort mismatch异常

而当s改为Int类型时，Z3允许不同基本内置类型（如Int和Bool）进行比较（尽管这种比较在逻辑场景中通常没有意义），不会触发类型断言错误，因此in操作能正常执行。

修复方案 #

如果你的需求是检查Python对象实例是否相同（即是否是同一个Z3变量），不要用Z3的重载比较，改用Python原生的身份判断：

from z3 import *
x= Bool('x')
State, (A,B) = EnumSort('State',['A', 'B'])
s = Const('s', State)
vars = [s,x]

# 方案1：用any()结合is判断
if any(item is x for item in vars):
    print('yes')

# 方案2：遍历判断
for item in vars:
    if item is x:
        print('yes')
        break

如果是想做逻辑上的表达式相等性检查，那必须确保比较的两个表达式类型一致，跨类型的逻辑比较本身没有意义，应当避免。

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