From 15d5cd2021d6cf08eb0042763f7242092efe2927 Mon Sep 17 00:00:00 2001
From: Dimos Tsouros <dimosts988@gmail.com>
Date: Mon, 18 Sep 2023 15:03:14 +0200
Subject: [PATCH] only_bv_reifies

---
 cpmpy/transformations/reification.py | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

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