Conversation
IgnaceBleukx
left a comment
There was a problem hiding this comment.
Great, that should do away with a lot of weird cases in the transformation stack...
Maybe also add the optional argument to expressions.utils.implies? We use it when we're not sure the lhs is an expression
IgnaceBleukx
left a comment
There was a problem hiding this comment.
Minor comments on docs, and one potential simplification in implies that we can always do, regardless of the simplify arg
| def value(self): | ||
| return None # default | ||
| def value(self) -> Optional[int]: | ||
| return None # default |
There was a problem hiding this comment.
Shouldn't this raise a NotImplemented error instead? It seems weird to have a default value for a method that every subclass absolutely should override...
| """Implication constraint: ``self -> other``. | ||
|
|
||
| Python does not offer relevant syntax for implication, call this method instead. | ||
| For double reification (<->), use equivalence ``self == other``. |
There was a problem hiding this comment.
Choco has expr.reify_with, which we could also add maybe? That would just redirect to ==
(Not for this PR, but smt to think about in the future)
|
|
||
| Args: | ||
| other (ExprLike): the right-hand-side of the implication | ||
| simplify (bool): if True, simplify True/False constants (might remove expressions & their variables from user-view) |
There was a problem hiding this comment.
"might eliminate..." is more accurate?
|
|
||
| def __invert__(self): | ||
| if not (is_boolexpr(self)): | ||
| def __invert__(self) -> "Expression": |
There was a problem hiding this comment.
So this __invert__ is typed, because we call it in implies, right? And that one is also typed.
Next PR should probably type the other __xxx__ methods?
| Expression: the implication constraint or a BoolVal if simplified | ||
|
|
||
| Simplification rules: | ||
| - BoolVal(True) -> other :: other (BoolVal-ified if needed) |
There was a problem hiding this comment.
We can always apply this one, it does not remove user vars
| return math.floor(expr), math.ceil(expr) | ||
|
|
||
| def implies(expr, other): | ||
| # first to are declarations for typing purposes only |
one notable change is about 'implies' and simplification...
one principle is that we typically don't simplify expressions at creation time, only at transformation time (subject to some exceptions).
I now make this more explicit, making 'simplify' an option to implies (which we don't activate anywhere at the moment). So for the user we wont delete expressions and variables unexpectedly, and for us, if we want it to activate we can.