Simplify relational witness invariants

[sim642]

Simplifications

1. Use unary minus instead of subtraction from 0: 0 - x >= 0 → -x >= 0.
2. Move constant to other side instead of always comparing with 0: -10 + x >= 0 → x >= 10.
3. Don't add variables with coefficient 0. Apparently they are also iterated over.

TODO

• Avoid negation on both sides: -x >= -5 → 5 >= x.
• Avoid initial unary minus if possible: -x + y >= 0 → y - x >= 0.
• Convert dual octagon inequalities into one equality: x >= 0 && -x >= 0 → x == 0.
  • Use for exact filtering (works automatically).
• Avoid two constants: x + 5 = 0 → x = -5 (only happens if one side is default 0)? Needs ad-hoc logic and extra care to ensure unary minus does not overflow.

[michael-schwarz]

Are transformation such as avoid negation on both sides actually sound in the presence of overflows?

[sim642]

Are transformation such as avoid negation on both sides actually sound in the presence of overflows?

If anything, I think it should avoid overflows. The constraint from Apron is on mathematical integers, so x doesn't overflow, while -x could.
Similarly in -x >= -5 if x is minimum long long, then the invariant would have an overflow, whereas 5 >= x would not.

---

Above I described a bunch of small simplifications based on invariants I've seen and how they would look nicer. I started out trying to implement such simplifications, but eventually realized that the following algorithm pretty much does it all: put all terms with positive coefficients on one side and all of the ones with negative coefficients to the other (while removing the negation). So it's just a comparison between two sums.

We're still casting everything to long long to minimize the chance of overflow, but neither the old nor the new implementation guarantees that. For example, x - y + z >= 0 is now written as x + z >= y, where it could be that x + z overflows, but subtracting y in between would avoid that.
But either way we're not systematically handling it. That would require somehow trying/optimizing the variable order to keep all intermediate results in bounds. And not just the order of variables, but the placement of the parenthesis to choose evaluation order.

[michael-schwarz]

I think @DrMichaelPetter ran into some such issues when trying to assert constraints from his 2-variable domain, where doing some of these innocuous transformations lead to unsoundnesses. Maybe he can elaborate himself in the Gobcon today.

[DrMichaelPetter]

I think @DrMichaelPetter ran into some such issues ...

-x >= 5 was literally the constraint that was surprising me by overflowing in my experiments as well, when I synthesized constraints to propagate via event. We had a lengthy discussion and decided that unary minus was not particularly clever to choose for a synthesized constraint due to the inherent overflow.

[sim642]

Could either of you review this? This simplification is good for both human-readability and avoiding some obvious overflows.

[DrMichaelPetter]

Ok, it took me some time to understand this idea of partitioning into pterms and nterms, but now I get it. LGTM

[sim642]

Thanks! I added some comments to explain the partitioning and also the negation booleans that were there already before.