Decompose globals

[IgnaceBleukx]

New transformation to decompose any unsupported global constraints in flat expressions.
Code is functional but can be somewhat compacted I think...

Transformation should be run after flatten() for every solver so we do not have to decompose globals at a later stage.

Work in progress still

[IgnaceBleukx]

Significantly cleaned up the code of the new transformation.
Last design decision we should agree upon is whether to also have an argument to the new transformation supported_reified. Now these globals are decomposed in reify_rewrite based on the supported list we get there.
I'm doubtfull as we also handle global constraint differently in other transformations such as in only_numexpr_eq, but no decompositions, so yeah, not sure...
What do you think @JoD, @tias and @Wout4?

[JoD]

Looks good, but the decompose algorithm has many edge cases that are not covered, probably correctly so. So I'd like some more comment and explanation why these do not need to be covered.

[IgnaceBleukx]

Added some documentation and covered + tested more edge cases.
Most comments are resolved I think, except for merging "bound calculation" first.

[IgnaceBleukx]

Merged master with bound calculations into this branch, now Element can do a proper check if it is total or not.

[JoD]

Allright, I'm pretty sure this is not the final word on decomposing globals, but it is a good step in the right direction. I've got two open comments left that should be easy to resolve, so the PR gets an approve.

Broader concerns:

• what about abs? This one should simply be a global constraint.
• this decomposition code assumes a lot about the form of the constraints (e.g., flattened). Based on these assumptions, we get a lot of if-then cases that are handled, and now we hope that we handled all possibilities. A different way of decomposing would be to traverse the expression trees, keeping track of whether we are in a reified or non-reified (top-level) expression. We return the appropriate decomposition to the parent, who then replaces its child. This is a generic way of decomposing, which to me looks less hard to maintain. But it is out of the scope of this MR.

[IgnaceBleukx]

I agree we should make abs a global constraint indeed. We can then provide a decompose_comparison for that one as well.

Regarding decomposing globals in the expression tree, I thought about it as well but there are many edges cases which are unclear how to handle.
For example lets assume we have the following situation: a solver supporting AllDifferent but not Max
Then how do we decompose the max constraints in the constraint AllDifferent(max(a,b,c), max(x,y,z), max(p,q,r))?
We have a decompose_comparison for numerical global functions like these but they do not appear in a comparison in this case!
This leaves us with 2 options: decomposing the AllDifferent into pairwise inequalities, then do decompose_comparison for every max expression or flatten the constraint to [AllDifferent(IV0, IV1, IV2), max(a,b,c) = IV0, max(x,y,z) = IV1, max(p,q,r) = IV2]

So it is to prevent these cases I opted for decomposing the globals after flattening