move normalization of '!=' from flatten to push down negation

CPMpy · May 17, 2024 · 17073f4 · 17073f4
1 parent 93ccde5
commit 17073f4
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 8 deletions.
diff --git a/cpmpy/transformations/flatten_model.py b/cpmpy/transformations/flatten_model.py
@@ -225,12 +225,6 @@ def flatten_constraint(expr):
                 lexpr, rexpr = rexpr, lexpr
                 rewritten = True
 
-            # rewrite 'BoolExpr != BoolExpr' to normalized 'BoolExpr == ~BoolExpr'
-            if exprname == '!=' and lexpr.is_bool() and rexpr.is_bool():
-                exprname = '=='
-                rexpr = ~rexpr
-                rewritten = True
-
             # already flat?
             if all(__is_flat_var(arg) for arg in [lexpr, rexpr]):
                 if not rewritten:

diff --git a/cpmpy/transformations/negation.py b/cpmpy/transformations/negation.py
@@ -5,7 +5,7 @@
 from .normalize import toplevel_list
 from ..expressions.core import Expression, Comparison, Operator, BoolVal
 from ..expressions.variables import _BoolVarImpl, _NumVarImpl
-from ..expressions.utils import is_any_list, has_nested
+from ..expressions.utils import is_any_list, has_nested, is_boolexpr
 
 
 def push_down_negation(lst_of_expr, toplevel=True):
@@ -26,7 +26,7 @@ def push_down_negation(lst_of_expr, toplevel=True):
             # can be a nested list with expressions?
             newlist.append(push_down_negation(expr, toplevel=toplevel))
 
-        elif not has_nested(expr) and not (hasattr(expr, 'name') and expr.name == 'not'):
+        elif not has_nested(expr) and not (hasattr(expr, 'name') and (expr.name == 'not' or expr.name == '!=')):
             newlist.append(expr)  # no need to do anything
 
         elif expr.name == "not":
@@ -38,6 +38,13 @@ def push_down_negation(lst_of_expr, toplevel=True):
             else:
                 newlist.append(arg_neg)
 
+        # rewrite 'BoolExpr != BoolExpr' to normalized 'BoolExpr == ~BoolExpr'
+        elif expr.name == '!=':
+            lexpr, rexpr = expr.args
+            if is_boolexpr(lexpr) and is_boolexpr(rexpr):
+                newexpr = (lexpr == recurse_negation(rexpr))
+                newlist.append(newexpr)
+
         else:
             # an Expression, we remain in the positive case
             newargs = push_down_negation(expr.args, toplevel=False)  # check if 'not' is present in arguments