diff --git a/cpmpy/transformations/flatten_model.py b/cpmpy/transformations/flatten_model.py index b434796ab..e4c057114 100644 --- 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 new file mode 100644 index 000000000..e243fc5e2 --- /dev/null +++ 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 index f47eb3936..b44c980ef 100644 --- 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])),'')