Support globals to define their own negation

[ThomSerg]

Xor is not part of "Operator" but instead a special global. It was missing in the normalisation for constant bools.

Linked to the more general problem of #620. That issue covers the problem on how to handle boolean constants in a generic global constraint. This pull request only tackles the case for Xor.

[IgnaceBleukx]

This is indeed an open issue (also related to #620 though not fully fixed by this PR).
One issue remaining: namely the changed context of XOR, based on the number of true constants you removed from it. This needs to be fixed before it can be merged.

[IgnaceBleukx]

This goes wrong in the current transformation stack (see failing tests I pushed).
The issues is that simplify_boolean comes AFTER decompose_global. While xor is support toplevel, it is not supported nested, but here you make it nested... so it fails later on when we try to post ~xor.

I'm not really sure how to fix it, other than decomposing the xor here...

[IgnaceBleukx]

Ok so it turned out the fix was to push down the negation into one of the arguments in XOR.
This made me realize we can also do this for the "If then else" global constraint, so added a specialc case for that as well.

@ThomSerg I refactored your XOR-code for the simplification transformation. It's now slighly less efficient (iterates over args twice instead of once); but I think it's more readable this way, and compared to "and" and "or", the xor-case should much less frequent anyway. I you think the previous version should go in, also fine to me, feel free to revert the last commmit then ; )

[tias]

This sets a precedent, having an 'if' case for two specific named globals in a transformation, actually in two: in negation and in normalize.

As far as I know, all transformations are designed so that there is no 'special case' logic for individual globals in them, e.g. a user can add a new global with the same ease as a cpmpy developer. And as a starting developer there are no 'surprises' with magic places where additional logic happens. With this, we would add special negation and normalisation cases in the transfo...

So I don't like that.

I'm also not sure what the alternative is. For the 'negation' one could imagine an additional abstract function for globals 'negate_custom()' or so?
But for normalize... not sure.

Why did we need a custom normalize for Xor again?

[IgnaceBleukx]

I see this might indeed not be the best place to implement the negation;
In issue #692 I proposed a .negate function for global constraints, but I forgot about it while implementing this PR...

Xor and IfThenElse could be a good place to start implementing such a function. The default will just return ~self.

As for normalization of XOR, we run in the trouble later on if we do not normalize it.
Our simplify_boolean tranformation promises to remove any Boolean constants from the expression tree, but this is simply not true when they are used in global constraints.

E.g., XOR(a,b,True) ends up as is in OR-Tools, where there is no support for the Boolval, to convert it to a solver var. Alternatively, we can special case it in each solver interface, but that also seems unwanted.
Although actually, we also do this for numerical constants in some interfaces already. So maybe that is the way to go after all

Taking over implementation of PR

[tias]

Yes, great.

I do see two separate issues being addressed here... e.g. the 'negation' part is independent?

[IgnaceBleukx]

Yes that's true... I could split out the negation stuff to a different PR tho?
Then this would be simple patch fixing the special XOR case in OR-Tools, Z3 and Pysat (through linearize)

[IgnaceBleukx]

Turned out it was easier to just cherry pick the changes to the solver interfaces and the tests, opened new PR #717 for release