diff --git a/cpmpy/transformations/reification.py b/cpmpy/transformations/reification.py index 354c3ee30..3cf0eabc9 100644 --- a/cpmpy/transformations/reification.py +++ b/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