some more typing of core

cpmpy/expressions/core.py

@@ -189,10 +189,10 @@ def __repr__(self) -> str:
                 strargs.append(f"{arg}")
         return "{}({})".format(self.name, ",".join(strargs))
 
-    def __hash__(self):
+    def __hash__(self) -> int:
         return hash(self.__repr__())
 
-    def has_subexpr(self):
+    def has_subexpr(self) -> bool:
         """ Does it contains nested :class:`Expressions <cpmpy.expressions.core.Expression>` (anything other than a :class:`~cpmpy.expressions.variables._NumVarImpl` or a constant)?
             Is of importance when deciding whether certain transformations are needed
             along particular paths of the expression tree.
@@ -204,8 +204,8 @@ def has_subexpr(self):
             return self._has_subexpr
 
         # micro-optimisations, cache the lookups
-        _NumVarImpl = cp.variables._NumVarImpl
-        _NDVarArray = cp.variables.NDVarArray
+        _NumVarImpl = cp.expressions.variables._NumVarImpl
+        _NDVarArray = cp.expressions.variables.NDVarArray
 
         # Initialize stack with direct access to private _args
         stack = list(self._args)
@@ -233,35 +233,59 @@ def has_subexpr(self):
         self._has_subexpr = False
         return False
 
-    def is_bool(self):
+    def is_bool(self) -> bool:
         """ is it a Boolean (return type) Operator?
             Default: yes
         """
         return True
 
-    def value(self):
-        return None # default
+    def value(self) -> Optional[int]:
+        return None  # default
 
-    def get_bounds(self):
+    def get_bounds(self) -> tuple[int, int]:
         if self.is_bool():
-            return 0, 1 #default for boolean expressions
+            return 0, 1  # default for boolean expressions
         raise NotImplementedError(f"`get_bounds` is not implemented for type {self}")
 
-    # keep for backwards compatibility
     def deepcopy(self, memodict={}):
+        """ DEPRECATED: use copy.deepcopy() instead
+
+        Will be removed in stable version.
+        """
         warnings.warn("Deprecated, use copy.deepcopy() instead, will be removed in stable version", DeprecationWarning)
         return copy.deepcopy(self, memodict)
 
-    # implication constraint: self -> other
-    # Python does not offer relevant syntax...
-    # for double implication, use equivalence self == other
-    def implies(self, other):
-        # other constant
-        if is_true_cst(other):
-            return BoolVal(True)
-        if is_false_cst(other):
-            return ~self
-        return Operator('->', [self, other])
+    def implies(self, other: ExprLike, simplify: bool = False) -> "Expression":
+        """Implication constraint: ``self -> other``.
+
+        Python does not offer relevant syntax for implication, call this method instead.
+        For double implication, use equivalence ``self == other``.
+
+        Args:
+            other (ExprLike): the right-hand-side of the implication
+            simplify (bool): if True, simplify True/False constants (might remove expressions & there variables from user-view)
+
+        Returns:
+            Expression: the implication constraint or a BoolVal if simplified
+
+        Simplification rules:
+            - self -> True :: BoolVal(True)
+            - self -> False :: ~self (Boolean inversion)
+        """
+        if not simplify:
+            return Operator('->', (self, other))
+
+        if isinstance(other, Expression):
+            if isinstance(other, BoolVal):  # simplify
+                if other.args[0]:
+                    return BoolVal(True)
+                return self.__invert__()  # not self
+            return Operator('->', (self, other))
+        else:  # simplify
+            assert isinstance(other, bool) or isinstance(other, np.bool_), f"implies: other must be a boolean, got {other}"
+            if other:
+                return BoolVal(True)
+            return self.__invert__()  # not self
 
     # Comparisons
     def __eq__(self, other):
@@ -427,19 +451,19 @@ def __rpow__(self, other: Any):
     def __neg__(self):
         if self.name == 'wsum':
             # negate the constant weights
-            return Operator(self.name, [[-a for a in self.args[0]], self.args[1]])
-        return Operator("-", [self])
+            return Operator(self.name, ([-a for a in self.args[0]], self.args[1]))
+        return Operator("-", (self,))
 
     def __pos__(self):
         return self
 
     def __abs__(self):
         return cp.Abs(self)
 
-    def __invert__(self):
-        if not (is_boolexpr(self)):
+    def __invert__(self) -> "Expression":
+        if not (self.is_bool()):
             raise TypeError("Not operator is only allowed on boolean expressions: {0}".format(self))
-        return Operator("not", [self])
+        return Operator("not", (self,))
 
     def __bool__(self) -> bool:
         raise ValueError(f"__bool__ should not be called on a CPMPy expression {self} as it will always return True\n"
@@ -452,7 +476,7 @@ class BoolVal(Expression):
     """
 
     def __init__(self, arg: bool|np.bool_) -> None:
-        arg = bool(arg)  # will raise ValueError if not a Boolean-able
+        arg = bool(arg)
         super(BoolVal, self).__init__("boolval", (arg,))
 
     def value(self) -> bool:
@@ -545,21 +569,30 @@ def has_subexpr(self) -> bool:
         """
         return False # BoolVal is a wrapper for a python or numpy constant boolean.
 
-    def implies(self, other: ExprLike) -> Expression:
-        my_val: bool = self.args[0]
-        if isinstance(other, Expression):
-            assert other.is_bool(), "implies: other must be a boolean expression"
-            if my_val:  # T -> other :: other
-                return other
-            return Operator("->", [self, other])  # do not simplify to True, would remove other from user view
-        else:
-            # should we check whether it actually is bool and not int?
-            if my_val:  # T -> other :: other
-                return BoolVal(bool(other))
-            else:  # F -> other :: True
-                return BoolVal(True)
-            # note that this can return a BoolVal(True)
+    def implies(self, other: ExprLike, simplify: bool = False) -> Expression:
+        """Implication constraint: ``BoolVal -> other``.
+
+        Args:
+            other (ExprLike): the right-hand-side of the implication
+            simplify (bool): if True, simplify True/False constants (might remove expressions & there variables from user-view)
+
+        Returns:
+            Expression: the implication constraint or a BoolVal if simplified
 
+        Simplification rules:
+            - BoolVal(True) -> other :: other (BoolVal-ified if needed)
+            - BoolVal(False) -> other :: BoolVal(True)
+        """
+        if not simplify:
+            return Operator('->', (self, other))
+
+        if self.args[0]:
+            if not isinstance(other, Expression):
+                assert isinstance(other, bool) or isinstance(other, np.bool_), f"implies: other must be a boolean, got {other}"
+                return BoolVal(other)
+            return other
+        else:
+            return BoolVal(True)
 
 class Comparison(Expression):
     """Represents a comparison between two sub-expressions

cpmpy/transformations/int2bool.py

@@ -50,7 +50,7 @@ def _encode_expr(ivarmap, expr, encoding, csemap=None):
         p, consequent = expr.args
         constraints, domain_constraints = _encode_expr(ivarmap, consequent, encoding, csemap=csemap)
         return (
-            [p.implies(constraint) for constraint in constraints],
+            [p.implies(constraint, simplify=True) for constraint in constraints],
             domain_constraints,
         )
     elif isinstance(expr, Comparison):
@@ -355,7 +355,7 @@ def encode_domain_constraint(self):
         if len(self._xs) <= 1:
             return []
         # Encode implication chain `x>=d -> x>=d-1` (using `zip` to create a sliding window)
-        return [curr.implies(prev) for prev, curr in zip(self._xs, self._xs[1:])]
+        return [curr.implies(prev, simplify=True) for prev, curr in zip(self._xs, self._xs[1:])]
 
     def _offset(self, d):
         return d - self._x.lb - 1

tests/test_trans_simplify.py

@@ -25,8 +25,12 @@ def test_bool_ops(self):
 
         expr = Operator("->", [self.bvs[0], True])
         assert str(self.transform(expr)) == "[boolval(True)]"
+        expr = Operator("->", [self.bvs[0], BoolVal(True)])
+        assert str(self.transform(expr)) == "[boolval(True)]"
         expr = Operator("->", [self.bvs[0], False])
         assert str(self.transform(expr)) == "[~bv[0]]"
+        expr = Operator("->", [self.bvs[0], BoolVal(False)])
+        assert str(self.transform(expr)) == "[~bv[0]]"
         expr = Operator("->", [True, self.bvs[0]])
         assert str(self.transform(expr)) == "[bv[0]]"
         expr = Operator("->", [False, self.bvs[0]])