strict typing and implemetation of Comparison#879
strict typing and implemetation of Comparison#879tias wants to merge 1 commit intomypy_oper_initfrom
Conversation
IgnaceBleukx
left a comment
There was a problem hiding this comment.
Indeed many interesting aspects!
I agree we should not support floats, but the silent cast gives me some anxiety... Numpy used to have a np.can_cast function for checking if the cast is safe, but it no longer works for Python ints/floats; so not sure if there still is an efficient way of handling floats in a safe manner (i.e., raising an error/warning)
For the .value()/argval change, see my comment above, I strongly believe we should either catch the IncompleteFunctionErr in the .value() function of Comparison; or stick with using argval there too.
| elif other_int == 0: | ||
| return ~self | ||
| else: | ||
| raise ValueError(f"Comparison {self} == {other_int} is not valid. Expected Boolean Expression or Boolean constant, but got {other_int}.") |
There was a problem hiding this comment.
According to our own spec, it is actually valid? You can use a Boolean expression as an integer anywhere you like. It's just that it is replaced withfalse by the simplify_boolean transformation.
There was a problem hiding this comment.
We can't return False here just yet tho, as we need to keep all variables until we arrive at the solver
| if other is False or other == 0: | ||
| return ~self | ||
| return Comparison("==", self, other) | ||
| def __eq__(self, other: object): |
There was a problem hiding this comment.
Shouldn't other be ExprLike?
Also, we can add the return type Expression?
There was a problem hiding this comment.
we have to be equal or more general than the superclass typing, which is 'object'
| elif other_int == 1: | ||
| return ~self | ||
| else: | ||
| raise ValueError(f"Comparison {self} == {other_int} is not valid. Expected Boolean Expression or Boolean constant, but got {other_int}.") |
There was a problem hiding this comment.
Copy-paste err in eror message
|
|
||
| def __lt__(self, other): | ||
| return Comparison("<", self, other) | ||
| def __lt__(self, other: object): |
There was a problem hiding this comment.
For these we can add return type Comparison
| allowed = {'==', '!=', '<=', '<', '>=', '>'} | ||
|
|
||
| def __init__(self, name: str, left: ExprLike, right: ExprLike) -> None: | ||
| def __init__(self, name: str, left: Expression, right: Expression|int) -> None: |
There was a problem hiding this comment.
I agree with this change, but we should add something inthe docstring saying that these comparisons should not be created manually as we don't do any type checking in the constructor.
The fact that left is never an integer is purely due to the way how Python implements operator overloading
| elif self.name == ">": return arg_vals[0] > arg_vals[1] | ||
| elif self.name == ">=": return arg_vals[0] >= arg_vals[1] | ||
| return None # default | ||
| lhs_val = self.args[0].value() |
There was a problem hiding this comment.
Why not use argvals here? There are certainly cases where this left-hand side can be partial?
On the current master, the IncompleteFunctionErr raising was stopped at the Comparison level; but now it can travel further up when calling .value()
I would have to think a bit harder if it can also result in a wrong answer from the value function, but it's definetly unexpected:
x,y = cp.intvar(0,5, shape=2, name=tuple("xy"))
x._value = 3
y._value = 0
comp = x//y == 2
print(comp.value()) # raises IncompleteFunctionErr
print(argval(comp)) # ok this works fine
bv = cp.boolvar()
bv._value = True
expr = comp == bv
print(expr)
print(expr.value()) # also raises IncompleteFunctionErr, used to work fine on master
print(argval(expr))| for x,y in [(numexpr,rhs), (rhs,numexpr)]: | ||
| # check if the constraint we are trying to construct is always UNSAT | ||
| if any(eval_comparison(comp_name, xb,yb) for xb in get_bounds(x) for yb in get_bounds(y)): | ||
| if any(eval_comparison(comp_name, xb,yb) for xb in get_bounds(x) for yb in get_bounds(y)) \ |
There was a problem hiding this comment.
We should update this test to use the utils.eval_comparison function, as this is also the way uses will/should make the comparisons themselves
|
I'm going to leave this hanging to pick up later (probably in separate PRs) So, identified issues:
|
A first attempt to make the typing and implementation more precise.
Reveals many interesting things:
Const CMP Expr, which is never possible for a user (python reverse-posts the comparison) so we should not support nor test itBoolExpr == 4which is invalid and we now raise...x // ys which we now trip over because value() no longer uses argval() which silently hid that; maybe we should explicitly catch expected Incomplete's in the test suite? or they are generated by accident (no partial transform)?Also, we now, as a hot path, try to convert any non-Expression to integer. If it fails, ValueError, if it succeeds we have our int. But this 'silently' converts integers to floats... (and we have a Z3 test that used a float) We don't support floats so we shouldn't test floats, but do we find it acceptable to silently convert floats? I do, but we should document it then...
(the alternative is 2 additional isinstance checks on every non-Expression in the comparison RHS)