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')?

[tias]

I've demonstrated the precisely-typed way to implement the (changed, expr) pattern.

I think it nicely separates the actual expr-handling logic from the more generic handling of args.

I think it also uses fewer isinstance checks, esp on already flat expression lists, but I did not benchmark it.

It also exposes a potential bug in the merging of the top-level ands (did not test nor tried to fix).

Also pumpkin seems to fail on the online CI, because of a 'bool' constant where we should be having an expression... so either the bug from the line above, or somewhere earlier in the stack.

so... have a look, but feel free to revert if you prefer the previous, correctly working, version.

[IgnaceBleukx]

Reviewed your changes with the new pattern, I very much like it!
Added some doc updates on the parts that were unclear to me at first.

It's very interesting that the _args function has no logic at all built in about what is is trying to achieve.
This could in theory mean that we can abstract this function out completely and re-use a (hyper-optimized) version in other transformations as well.
Not sure how mypy-c'able that would be, but the abstract function could have the heading:

def recursive_arg_helper(args: list[Any] | tuple[Any,...], parent_expr_function: Callable[[Expression], tuple[bool, Expression]]) -> tuple[bool, list[Any] | tuple[Any,...]]

Next to refactor using the new pattern would be: safen, decompose and simplify_bool (I would start with simplify_bool)

This PR is good to merge for me after tests complete

[tias]

there could be a general pattern... but I don't mind adding implementations of versions of the same...

mypyc can't optimize 'argument is a function' well I think... I think those remain standard-python-boxed; just simple loops that call other C functions directly is what its best at.

[IgnaceBleukx]

Yes agreed : )