288 simplify boolean contstants #291
Conversation
There was a problem hiding this comment.
for logical constraints (and, or, impl), this is currently already done in our overloadings of the python operators (at factory time).
This kind of constraint-level simplification can also be done after flatten.
I think the case we want more is the other case you are describing, where we are using a bool (const or var) as an int, in a comparison with another int, e.g. bv >= 1, bv != 0 etc.
Also, I'm not sure that your code does a full traversal of the expression tree, e.g. I dont think you walk over the args of every expressions upto their leafs (variables or constants)?
perhaps we should do the other case in a separate pull request
|
Yes, I know for some operators we simpify at construction time (but for example not if you construct an I forgot to add the case of global constraints, then it should actually traverse the entire tree line 64 and line 99 The boolean simplification will basically be a switch statement summarizing the following table:
Maybe it does deserve to live in this pull request/transformation as well. I'll implement it and we can still remove it if this does not seem to be the right spot anyway. |
…pmpy into 288-simplify-boolean-contstants
…n-contstants # Conflicts: # cpmpy/solvers/z3.py
|
Updated with some more tests, I think it ready to merge now. |
cpmpy/transformations/normalize.py
Outdated
| if any(is_false_cst(arg) for arg in args): | ||
| newlist.append(1 if num_context else BoolVal(True)) | ||
| else: | ||
| newlist.append(Operator("or", [arg for arg in args if not isinstance(arg, BoolVal)])) |
There was a problem hiding this comment.
I think this would not clean a 'true' or np.true; I also think we are needlessly copying a lot of objects that do not change.
But I also don't have a solution straight away... will think about it
There was a problem hiding this comment.
I could just check for is_false_cst instead of the BoolVal here? (The is_false_cst on line 63 should be is_true_cst!) That check will also hold for np constants.
Not sure if we can do anything about the copying... Except for changing args in place but some transformation will have to copy them at least once as the users constraints should remain unchanged
cpmpy/transformations/normalize.py
Outdated
|
|
||
| elif isinstance(expr, Comparison): | ||
| lhs, rhs = simplify_boolean(expr.args, num_context=True) | ||
| if (isinstance(lhs, int) and isinstance(rhs, _BoolVarImpl)) or isinstance(lhs, BoolVal) and isinstance(rhs, _IntVarImpl): |
There was a problem hiding this comment.
Swap the comparison symbol too? Why swap?
There was a problem hiding this comment.
second case cannot happen, as BoolVal should be upcasted to int by line 97.
There was a problem hiding this comment.
So only case where we can do something smart is when one of the arguments is int and the other is BoolVal - Ignace.
There was a problem hiding this comment.
TODO: make sure comparison symbol is swapped too!
There was a problem hiding this comment.
TODO: note somewhere that we do not simplify comparisons between two integer expressions and between two Boolean expressions in general. We only simplify Boolean variables compared to integer values.
cpmpy/transformations/normalize.py
Outdated
| lhs, rhs = simplify_boolean(expr.args, num_context=True) | ||
| if (isinstance(lhs, int) and isinstance(rhs, _BoolVarImpl)) or isinstance(lhs, BoolVal) and isinstance(rhs, _IntVarImpl): | ||
| lhs, rhs = rhs, lhs | ||
| if isinstance(lhs, _BoolVarImpl) and isinstance(rhs, int): |
There was a problem hiding this comment.
The central idea is that a comparison of a Boolean variable to an integer value can always be simplified to a simple Boolean expression. E.g., p <= 0 simplifies to ~p`.
|
After previous meeting: Tias suggested to not only check for Boolean variables compared to integer values, but also to Boolean expressions compared to integer values. Ignace suggested this would not be a lot of work and he would update the PR. |
|
Adapted as Jo described above. |
…mpy into 288-simplify-boolean-contstants
# Conflicts: # tests/test_constraints.py
Implemented transformation to convert boolean constants into integers.
Related but not implemented are conversions of simple boolean expressions such as BV >= 1 to True.
It can also be done in this transformation, but then it should get a new name such as
simplify_booleanor something like that.The question is then how far do we want to go in this? In essence, we are checking if constraints posted to a solver are "satisfied by construction" and we can do this for many other expressions other than simple boolean expressions.