如何在Z3Py当前上下文中重新定义公式以验证等价性？

问题场景 #

• 编写了check_sat和check_equiv函数用于验证Z3Py公式f1、f2的等价性
• 当check_equiv内部直接定义f1、f2时代码正常运行，但将外部来源的f1、f2作为参数传入时功能失效
• 已知f1、f2来自不同来源但共享同一全局上下文，且无法修改这些来源的代码，希望通过在check_equiv内重新定义公式解决问题

原代码 #

def check_sat(*args):
    s = Solver()
    for v in args:
        s.add(v)
    return s.check()


def check_equiv(f1, f2):
    # a, b = Ints('a b')
    # f1 = Not(a == b)
    # f2 = Not(b == a)
    if check_sat(f1, Not(f2)) == unsat:
       return True
    else:
       return False

解决方案 #

可以在check_equiv内重新定义与原公式语义等价的表达式来解决问题，具体说明如下：

可行性原因 #

外部传入的f1、f2可能存在隐性问题：比如变量看似同名但实际是不同实例、表达式被外部代码意外修改、或者存在上下文绑定的隐式冲突。重新定义公式能确保使用的是当前函数内明确控制的、基于同一全局上下文的表达式，彻底规避外部来源带来的未知干扰。

修改示例 #

假设原传入的f1、f2基于全局整数变量a和b，修改后的check_equiv函数如下：

def check_equiv(f1, f2):
    # 基于同一全局上下文重新定义等价公式
    a, b = Ints('a b')
    new_f1 = Not(a == b)
    new_f2 = Not(b == a)
    if check_sat(new_f1, Not(new_f2)) == unsat:
        return True
    else:
        return False

注意事项 #

• 重新定义的公式必须和原传入的f1、f2语义完全一致，否则等价性验证结果会不准确
• 如果原公式涉及更多变量或复杂逻辑，需要先确认原公式的变量集合和表达式结构，再对应构建新的等价表达式
• 由于已知所有公式共享同一全局上下文，重新定义变量时会自动复用上下文内的已有变量实例，不会产生上下文冲突

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