Xor decomp simpl#908
Conversation
IgnaceBleukx
left a comment
IgnaceBleukx
left a comment
There was a problem hiding this comment.
Yes, this decomposition is much cleaner and clearer than before.
One comment about negation, otherwise good to go
| if len(new_args) == 0: | ||
| return [BoolVal(parity)], [] | ||
| if parity: # negate last argument | ||
| new_args[-1] = ~new_args[-1] |
There was a problem hiding this comment.
What happens if new_args[-1] is an expression? Then it will introduce a complex negation, right?
Ideally, we want to negate a variable here (see the .negate() of xor).
If there is no variable in any of the args, we can indeed negate this one, but we'll have to run push_down_negation again once we move that transformation before decompose (which I currently have in a local branch)
There was a problem hiding this comment.
yes, changed it to search for variables first.
Note that in the .negate(), I don't think we should be calling recurse_negate? I'm not actually sure where the negate pipeline comes from... I've removed the recurse_negate in it
There was a problem hiding this comment.
I think it came from when we weren't sure where to put negation either... Meanwhile I'm convinced it should go before decompose (currently it's right before flattening); so then globals cannot introduce negation anymore.
|
#827, #620, have not looked in detail but it all seems to boil down to the same thing: how to handle constants (e.g. in decompose). Its revealed in #929 that we should make sure our decomps only return Expressions, which I think would fix these issues. That is/can be done as part of our typing effort #913 |
3 participants
reactived by #906
closes #747
not sure what should now remain of #778
also leaves open that a user 'could' write BoolVal + BoolVal == 1, and that linearize would choke on this, somewhere...
it looks like we already had all the right tests, just not run for all solvers yet