z3py中如何将被Not取反的不等式转换为等价正向不等式

解决方案 #

基础场景（Not(x < y)转换）

直接使用z3py内置的z3.simplify()接口即可实现默认转换，代码示例如下：

import z3
x, y = z3.Ints("x y")
z3_expression = z3.Not(x<y)
print(z3.simplify(z3_expression))
# 输出结果：x >= y

补充场景（Not(x <= y)转换）

默认的simplify()没有启用全部算术重写规则，需要额外传入eq2ineq=True参数开启不等式转换规则，即可得到预期的x > y结果，代码示例如下：

z3_expression = z3.Not(x<=y)
z3_simplified_expression = z3.simplify(z3_expression, eq2ineq=True)
print(z3_simplified_expression)
# 输出结果：x > y

参数说明

• eq2ineq=True：让简化器自动将否定的比较运算、等式转换为等价的反向不等式，完全覆盖外层取反消去的需求场景。
• 如需统一输出格式，可额外添加arith_lhs=True参数，将所有算术项自动移到表达式左侧。

如果需要处理更复杂的自定义转换逻辑，还可以使用z3提供的重写器API自定义规则实现。

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