Open
Conversation
IgnaceBleukx
reviewed
Apr 6, 2026
Collaborator
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
| assert cp.Xor(bv).value() | ||
|
|
||
| def test_xor_with_constants(self): | ||
| def test_xor_with_constants(self, solver): |
Collaborator
There was a problem hiding this comment.
I thought you had to use the pytest fixture for this to work?
| if len(new_args) == 0: | ||
| return [BoolVal(parity)], [] | ||
| if parity: # negate last argument | ||
| new_args[-1] = ~new_args[-1] |
Collaborator
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)
Collaborator
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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