only_bv_reifies

cpmpy/transformations/reification.py

@@ -23,6 +23,27 @@
     - reify_rewrite():      rewrites reifications not supported by a solver to ones that are
 """
 
+def only_bv_reifies(constraints):
+    newcons = []
+    for cpm_expr in constraints:
+        if cpm_expr.name in ['->', "=="]:
+            a0, a1 = cpm_expr.args
+            if not isinstance(a0, _BoolVarImpl) and \
+                    isinstance(a1, _BoolVarImpl):
+                # BE -> BV :: ~BV -> ~BE
+                if cpm_expr.name == '->':
+                    newexpr = [(~a1).implies(recurse_negation(a0))]
+                else:
+                    newexpr = [a1 == a0]  # BE == BV :: BV == BE
+                    if not a0.is_bool():
+                        newexpr = flatten_constraint(newexpr)
+                newcons.extend(newexpr)
+            else:
+                newcons.append(cpm_expr)
+        else:
+            newcons.append(cpm_expr)
+    return newcons
+
 def only_bv_implies(constraints):
     """
         Transforms all reifications to BV -> BE form
@@ -35,17 +56,13 @@ def only_bv_implies(constraints):
         AFTER `flatten()`
     """
     newcons = []
+    constraints = flatten_constraint(only_bv_reifies(constraints))
+
     for cpm_expr in constraints:
         # Operators: check BE -> BV
         if cpm_expr.name == '->':
             a0,a1 = cpm_expr.args
-            if not isinstance(a0, _BoolVarImpl) and \
-                    isinstance(a1, _BoolVarImpl):
-                # BE -> BV :: ~BV -> ~BE
-                newexpr = (~a1).implies(recurse_negation(a0))
-                #newexpr = (~a1).implies(~a0)  # XXX when push_down_neg is separate, negated_normal no longer needed separately
-                newcons.extend(only_bv_implies(flatten_constraint(newexpr)))
-            elif isinstance(a1, Comparison) and \
+            if isinstance(a1, Comparison) and \
                     a1.name == '==' and a1.args[0].is_bool() and a1.args[1].is_bool():
                 # BV0 -> BV2 == BV3 :: BV0 -> (BV2->BV3 & BV3->BV2)
                 #                   :: BV0 -> (BV2->BV3) & BV0 -> (BV3->BV2)

tests/test_transf_reif.py

@@ -12,26 +12,6 @@ def setUp(self):
         _IntVarImpl.counter = 0
         _BoolVarImpl.counter = 0
 
-    def test_only_bv_implies(self):
-        a,b,c = [boolvar(name=n) for n in "abc"]
-
-        cases = [((a).implies(b), "[(a) -> (b)]"),
-                 ((~a).implies(b), "[(~a) -> (b)]"),
-                 ((a).implies(b|c), "[(a) -> ((b) or (c))]"),
-                 ((a).implies(b&c), "[(a) -> ((b) and (c))]"),
-                 ((b|c).implies(a), "[(~a) -> (~b), (~a) -> (~c)]"),
-                 ((b&c).implies(a), "[(~a) -> ((~b) or (~c))]"),
-                 ((a)==(b), "[(a) -> (b), (b) -> (a)]"),
-                 ((~a)==(b), "[(~a) -> (b), (b) -> (~a)]"),
-                 ((b|c)==(a), "[(~a) -> (~b), (~a) -> (~c), (a) -> ((b) or (c))]"),
-                 ((b&c)==(a), "[(~a) -> ((~b) or (~c)), (a) -> (b), (a) -> (c)]"),
-                ]
-
-        # test transformation
-        for (expr, strexpr) in cases:
-            self.assertEqual( str(only_bv_implies((expr,))), strexpr )
-            self.assertTrue(Model(expr).solve())
-
     def test_reif_element(self):
         bvs = boolvar(shape=5, name="bvs")
         iv = intvar(1,10, name="iv")