Refactor push_down_negation

[IgnaceBleukx]

Refactored push_down_negation transformation in similar spirit to recent rewrites of safening and decompose.

Returns a flag whether some of the expressions are changed, so eliminates any redundant copying of the argument (which was actually a todo in the original implementation)

Also added an optimization where Boolean variables are chosen to be negated instead of an expression when simplifying BExpr != BV.

I'm not sure about keeping the toplevel flag, but it's required as flatten expects a list of constraints without toplevel ands...

[tias]

In #908 I saw that Xor.negate imports recurse_negate instead of doing ~self.args[0].

Is it in the contract of negate() that it should not introduce a negation itself? If so, can this be documented somehwere (e.g. in globalconstraints doc where 'optionally, can implement negate')?