Push down negation before decompose

[IgnaceBleukx]

Re-order the transformations such that negation is pushed down into the arguments of a "not" operator before we call decompose.

This allows to implement efficient implementations of negated global constraints (e.g., ~Table becomes Negtable).
We can also do this for some more (e.g., ~AllDiff(x) becomes NValue(x) < len(x)). We should probably do some small experiments to see what is more efficient? Also depends on the decomp of NValue of course if that one is not supported...

Downside is that no transformation can explicitly introduce negation, and needs to call recurse_negation themself. This turned out to be simpler to implement than I first thought.

Efficiency-wise, there might be some gains because we now have one transformation less to be called in each recursiveflatten_constraint call. I then also noticed we call simplify_boolean in each recursive flatten call, I've added a flag to disable it when we can. Not sure if this should remain in this PR

[tias]

you will have to rebase/merge master in I guess, now that push down negation rewrite is in (in a different form)

[tias]

almost there.

I guess you checked that no global cons/func introduces a negation, even on the latest master?

Also, we since have 'scip' as a solver, can you check that all solvers on master that need changing are changed?

[IgnaceBleukx]

Processed the review, there were indeed a couple of cases where the decomposition/negation of a global might introduce negation.

Updated scip and docs

[IgnaceBleukx]

Also updated the newly added highs solver, should be ready to go in after tests complete?

[tias]

if we pushed down negation before, and decompose can not contain negation, then there can be no negation here?

or, if we do catch remaining negations here, then we do not have the strict requirment that decompose's can not contain negation?

[IgnaceBleukx]

expr here is the original expression; so if we had ~AllDifferent(x,y,z), expr would be 'not', and the new_args would be and(x != y, x != z, y != z), which we would have to negate.

I've renamed the variables now to make this more clear

[tias]

I don't get it yet...

so negate leaves ~AllDiff? What else does it leave with a toplevel ~?

and here we are in decompose, and if we encounter ~Smth, we will call recurse_negate(Smth), but in the case of ~AllDiff, our decompose is counting on recurse_negate() to do the treatment of the global...

Indeed, I can see that recurse_negate() will check for a global and then walk its args and call Glob.negate() on it. But if it already has that logic, why did we not use it when doing push_down_negation??

E.g. I would expect either:

1. push_down_negate does not push negations over globals; and decompose_global is left to do that, so it will check the ~Glob case and itself handle the pushing down

2. push_down_negate also pushes negation over globals; then decompose_global can assume the input is negation-free

[IgnaceBleukx]

Ah yes there were idd some parts we can just keep the ~var part, fixed now.

[tias]

we should first resolve the other discussion about 'not'.

After resolving that, we should note that there is an ignored case here where arg.name == not but arg.has_subexpr=False and then this not would remain untreated.