Rewrite decompose_globals to work at tree level

[IgnaceBleukx]

We should rewrite the decompose_globals transformation to work with non-flattened constraints.
This way, less auxiliary variables are introduced.

Some special edge cases to take care of in this transformation:

• Nesting of global numerical constraints:
  For example: AllDiff(max(x,y,z), p,q) when AllDiff is supported but not max should become [AllDiff(aux,pq), max(x,y,z).decompose_comparison('==',aux)]
• Global constraints in negative context: make sure to use decompose_negation
• Partial global constraints: see discussion in Incomplete functions on rhs of implication #184

In essence, this function should walk trough the expression tree and decompose any unsupported global constraint/function BEFORE flattening. This allows downstream transformations to completely ignore global constraints and allows solvers such as z3 which directly work on the expression tree level to not worry about special global constraint cases.

[Wout4]

The advantage of flattening first however, is that there is no need for the whole decompose_negation thing
Do you have an example or insight of why this leads to more auxiliary variables?

[IgnaceBleukx]

We have to implement the logic for any object-oriented solver (such as Z3) anyway. So I think it would be best to just make it a transformation and let all solvers benefit from the effort.