new testfile

CPMpy · Sep 21, 2023 · 0c02a88 · 0c02a88
1 parent 5ba1421
commit 0c02a88
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 29 deletions.
diff --git a/cpmpy/transformations/flatten_model.py b/cpmpy/transformations/flatten_model.py
@@ -350,15 +350,6 @@ def normalized_boolexpr(expr):
 
             # LHS: check if Boolexpr == smth:
             if (exprname == '==' or exprname == '!=') and lexpr.is_bool():
-                if is_num(rexpr):
-                    # BoolExpr == 0|False
-                    assert (not rexpr), f"should be false: {rexpr}" # 'true' is preprocessed away
-                    if exprname == '==':
-                        nnexpr = recurse_negation(lexpr)
-                        return normalized_boolexpr(nnexpr)
-                    else: # !=, should only be possible in dubble negation
-                        return normalized_boolexpr(lexpr)
-
                 # this is a reified constraint, so lhs must be var too to be in normal form
                 (lhs, lcons) = get_or_make_var(lexpr)
                 if expr.name == '!=' and rvar.is_bool():

diff --git a/tests/test_trans_normalize.py b/tests/test_trans_normalize.py
@@ -0,0 +1,29 @@
+import unittest
+
+import cpmpy as cp
+from cpmpy.transformations.normalize import  normalize_boolexpr
+
+
+class TransSimplify(unittest.TestCase):
+    def test_normalize(self):
+        a ,b ,c ,d ,e ,f = cp.boolvar(shape=6)
+        self.assertEqual(str(normalize_boolexpr([a | (b & c) | d])) ,'[or([BV0, BV1, BV3]), or([BV0, BV2, BV3])]')
+        self.assertEqual(str(normalize_boolexpr([a | (b & (c & d)) | e]))
+                         ,'[or([BV0, BV1, BV4]), or([BV0, BV2, BV4]), or([BV0, BV3, BV4])]')
+        self.assertEqual(str(normalize_boolexpr([a | (b.implies(c)) | e])) ,'[or([BV0, ~BV1, BV2, BV4])]')
+        self.assertEqual(str(normalize_boolexpr([a | (b.implies(c.implies(d))) | e])) ,'[or([BV0, ~BV1, ~BV2, BV3, BV4])]')
+        self.assertEqual(str(normalize_boolexpr([a | ((b.implies(f)).implies(c.implies(d))) | e]))
+                         ,'[or([BV0, BV1, ~BV2, BV3, BV4]), or([BV0, ~BV5, ~BV2, BV3, BV4])]')
+        self.assertEqual(str(normalize_boolexpr([a | ((b.implies(f)).implies(c)) | e]))
+                         ,'[or([BV0, BV1, BV2, BV4]), or([BV0, ~BV5, BV2, BV4])]')
+        self.assertEqual(str(normalize_boolexpr([a | ((b.implies(f)).implies(c & d)) | e])),
+                         ('[or([BV0, BV1, BV2, BV4]), or([BV0, BV1, BV3, BV4]), or([BV0, ~BV5, BV2, '
+                          'BV4]), or([BV0, ~BV5, BV3, BV4])]'))
+        self.assertEqual(str(normalize_boolexpr([b.implies(f & a & c)]))
+                         ,'[(BV1) -> (BV5), (BV1) -> (BV0), (BV1) -> (BV2)]')
+        self.assertEqual(str(normalize_boolexpr([(b | d).implies(f)])) ,'[(~BV5) -> (~BV1), (~BV5) -> (~BV3)]')
+        self.assertEqual(str(normalize_boolexpr([(b | d).implies(f & a & c)])),
+                         ('[(~BV5) -> (~BV1), (~BV5) -> (~BV3), (~BV0) -> (~BV1), (~BV0) -> (~BV3), '
+                          '(~BV2) -> (~BV1), (~BV2) -> (~BV3)]'))
+        self.assertEqual(str(normalize_boolexpr([(b.implies(c)).implies(f & a)]))
+                         ,('[(~BV5) -> (BV1), (~BV5) -> (~BV2), (~BV0) -> (BV1), (~BV0) -> (~BV2)]'))
diff --git a/tests/test_trans_simplify.py b/tests/test_trans_simplify.py
@@ -2,7 +2,7 @@
 
 import cpmpy as cp
 from cpmpy.expressions.core import Operator, BoolVal, Comparison
-from cpmpy.transformations.normalize import simplify_boolean, toplevel_list, normalize_boolexpr
+from cpmpy.transformations.normalize import simplify_boolean, toplevel_list
 
 
 class TransSimplify(unittest.TestCase):
@@ -100,22 +100,3 @@ def test_with_floats(self):
         self.assertEqual(str(self.transform(expr)), '[(iv[0]) == (iv[1])]')
 
 
-    def test_normalize(self):
-        a,b,c,d,e,f = cp.boolvar(shape=6)
-        self.assertEqual(str(normalize_boolexpr([a | (b & c) | d])),'[or([BV0, BV1, BV3]), or([BV0, BV2, BV3])]')
-        self.assertEqual(str(normalize_boolexpr([a | (b & (c & d)) | e])),'[or([BV0, BV1, BV4]), or([BV0, BV2, BV4]), or([BV0, BV3, BV4])]')
-        self.assertEqual(str(normalize_boolexpr([a | (b.implies(c)) | e])),'[or([BV0, ~BV1, BV2, BV4])]')
-        self.assertEqual(str(normalize_boolexpr([a | (b.implies(c.implies(d))) | e])),'[or([BV0, ~BV1, ~BV2, BV3, BV4])]')
-        self.assertEqual(str(normalize_boolexpr([a | ((b.implies(f)).implies(c.implies(d))) | e])),'[or([BV0, BV1, ~BV2, BV3, BV4]), or([BV0, ~BV5, ~BV2, BV3, BV4])]')
-        self.assertEqual(str(normalize_boolexpr([a | ((b.implies(f)).implies(c)) | e])),'[or([BV0, BV1, BV2, BV4]), or([BV0, ~BV5, BV2, BV4])]')
-        self.assertEqual(str(normalize_boolexpr([a | ((b.implies(f)).implies(c & d)) | e])),
-                         ('[or([BV0, BV1, BV2, BV4]), or([BV0, BV1, BV3, BV4]), or([BV0, ~BV5, BV2, '
-                          'BV4]), or([BV0, ~BV5, BV3, BV4])]'))
-        self.assertEqual(str(normalize_boolexpr([b.implies(f & a & c)])),'[(BV1) -> (BV5), (BV1) -> (BV0), (BV1) -> (BV2)]')
-        self.assertEqual(str(normalize_boolexpr([(b | d).implies(f)])),'[(~BV5) -> (~BV1), (~BV5) -> (~BV3)]')
-        self.assertEqual(str(normalize_boolexpr([(b | d).implies(f & a & c)])),
-                         ('[(~BV5) -> (~BV1), (~BV5) -> (~BV3), (~BV0) -> (~BV1), (~BV0) -> (~BV3), '
-                          '(~BV2) -> (~BV1), (~BV2) -> (~BV3)]'))
-        self.assertEqual(str(normalize_boolexpr([(b.implies(c)).implies(f & a)])),('[(~BV5) -> (BV1), (~BV5) -> (~BV2), (~BV0) -> (BV1), (~BV0) -> (~BV2)]'))
-        #self.assertEqual(str(normalize_boolexpr([b == a + c])),'')
-        self.assertEqual(str(normalize_boolexpr([b + d == a + c])),'')