Remove SumEq expression

[niklasdewally]

Closes: #515

SumEq was used as an intermediate representation when rewriting sum(...) = e2 into flat sumgeq / sumleq constraints.

Instead, decompose sum(...) = e2 into sum(...) <= e2 /\ sum(...) >= e2 and let the normal Minion process for flattening these convert these to Minion.

---

Based on PR #570

Chain of upstream PRs as of 2025-01-08

• PR Convert Products to Minion #570:
  main ← nik/pr/add-mul/minion-conversion

  • PR Remove SumEq expression #571 (THIS ONE):
    nik/pr/add-mul/minion-conversion ← nik/pr/add-mul/remove-sum-eq

[ozgurakgun]

This chain of PRs thing at the bottom looks useful (and autogenerated?) What's your workflow that produces those?

[niklasdewally]

This chain of PRs thing at the bottom looks useful (and autogenerated?) What's your workflow that produces those?

I am trying out git machete.

Not completely sold on it though...

[ozgurakgun]

This chain of PRs thing at the bottom looks useful (and autogenerated?) What's your workflow that produces those?

I am trying out git machete.

Not completely sold on it though...

PR chains/stacks are useful though, so might be good. I'll look into it too.

[ozgurakgun]

LGTM, once rebased and tests pass etc.

[niklasdewally]

This chain of PRs thing at the bottom looks useful (and autogenerated?) What's your workflow that produces those?

I am trying out git machete.
Not completely sold on it though...

PR chains/stacks are useful though, so might be good. I'll look into it too.

On a similar note, I find doing git rebase --exec 'cargo test' main useful to check that each commit (as opposed to each PR, which is what Github does) has up to date tests. Makes seeing the effects of little rule changes much easier in the history.