如何在z3py中声明所有变量相等？是否有对应Distinct()的Equal方法？

想要声明列表内所有元素相等，z3py中是否不存在类似Distinct()的Equal()方法？目前我使用如下写法可以实现需求：

from z3 import *
import numpy as np

s = Solver()

B = [BitVec(f"b{j}", 7) for j in range(11)]

C_eq = [B[i] == B[j] for i in range(3) for j in range(3) if i != j]

s.add(C_eq)

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

z3py 没有内置和Distinct()对应的Equal()/AllEqual()方法，你当前的写法功能是正确的，不过存在冗余约束：你的双层循环会生成大量重复的相等约束（比如B[0]==B[1]和B[1]==B[0]），虽然不影响最终求解结果，但会增加不必要的约束数量，拉低求解效率。

更简洁高效的写法是让列表内所有元素和首个元素比较即可，如果你的需求是列表前3个元素相等，可以写成：

# 仅需要i从1到2和B[0]比较，共2条约束，替代原来的6条冗余约束
C_eq = [B[i] == B[0] for i in range(1, 3)]

如果需要整个列表全相等，直接遍历整个列表即可：

C_eq = [b == B[0] for b in B]

如果日常使用频率高，也可以自己封装一个和Distinct用法一致的通用函数：

def AllEqual(expr_list):
    # 长度小于等于1的列表天然满足全相等条件
    if len(expr_list) <= 1:
        return BoolVal(True)
    return And([elem == expr_list[0] for elem in expr_list[1:]])

# 调用时直接当内置方法用就行
s.add(AllEqual(B[:3]))

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