Implement ana.apron.invariant.diff-box directly in domain

[sim642]

This is on top of #1871.

This should be faster, because it doesn't require box domain analysis in parallel.
The domain is converted to box and back only during invariant generation.

It's also more precise in some sense because it can exclude box-like constraints, which cannot be inferred by box alone.
But maybe that's also a downside because it can exclude constraints, which still need the more precise domain.

So it's not clear to me what is the right thing. We could keep both, both that's one more configurable option which is unlikely to be useful.

[sim642]

I did some sv-benchmarks 60s 1GB 1 core level01 verify-validate runs with:

1. No diff-box
2. Previous diff-box
3. This diff-box

here: https://goblint.cs.ut.ee/results/297-all-validate-diff-box-direct-level01/table-generator-cmp.table.html#/.

Already using the old diff-box made a huge self-validation difference: 5075 → 5719. And that's even without noticeable slowdown: the extra box analysis cost is made up by less witness generation effort.
But the invariant count decrease is massive:

This makes less of a difference: 5719 → 5822, but it's a much nicer and cheaper implementation (although in the grand scheme of SV-COMP this doesn't show).
There's still some invariant count decrease: