如何移除Z3逻辑门中的重复布尔变量？

核心思路 #

遍历Z3逻辑表达式的子节点，利用AST节点的相等性去重，再重新构造对应的逻辑门（如Or/And），仅保留唯一的变量实例。

实现代码 #

from z3 import *

def remove_duplicate_args(expr):
    # 处理Or逻辑门
    if is_or(expr):
        # 借助字典键的唯一性去重，同时保留原节点顺序
        unique_children = list(dict.fromkeys(expr.children()))
        # 空Or返回恒假值，否则重新构造Or
        return Or(*unique_children) if unique_children else BoolVal(False)
    # 处理And逻辑门
    elif is_and(expr):
        unique_children = list(dict.fromkeys(expr.children()))
        # 空And返回恒真值，否则重新构造And
        return And(*unique_children) if unique_children else BoolVal(True)
    # 非多参数逻辑门的表达式直接返回原内容
    else:
        return expr

# 测试示例
a = Bool('a')
b = Bool('b')
c = Bool('a')
or_gate = Or(a, b, c)

cleaned_or = remove_duplicate_args(or_gate)
print(cleaned_or)  # 输出: Or(a, b)

关键细节说明 #

• 节点相等性：Z3中同名的布尔变量（如示例里的a和c）会被判定为相等，dict.fromkeys()能基于此自动完成去重。
• 顺序保留：Python 3.7及以上版本的字典会保留插入顺序，因此去重后的子节点顺序与原表达式一致。
• 边界处理：空Or返回BoolVal(False)（逻辑或的恒假值），空And返回BoolVal(True)（逻辑与的恒真值），完全符合Z3的语义规则。
• 扩展性：如果需要支持其他多参数逻辑操作（如Xor），只需添加对应的is_xor(expr)判断分支，用相同方式重新构造即可。

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