Convert Weighted Sums to Minion

[niklasdewally]

• Closes: Implement negation and negated sums #490, Implement conversion of sums with negations to weightedsumgeq and weightedsumleq #553
• Follow on PR of: Convert Products to Minion #570
• A previous version of this work can be found in Convert weighted sums to Minion #580

---

Add FlatWeightedSumGeq and FlatWeightedSumLeq Minion constraints, and
introduce_weightedsumleq_sumgeq rule to convert weighted sums to Minion
via these constraints.

DETAILS

This rule is a bit unusual compared to other introduction rules in that
it does its own flattening.

For example, introduce_sumleq only accepts sums of atoms and relies on
the generic flattening rules (flatten_binop / flatten_vecop) to run
before it flattens the sum.

a + (b*c) + (d*e) <= 10
  ~~> flatten_vecop
a + __0 + __1 <= 10

with new top level constraints

__0 =aux b*c
__1 =aux d*e

---

a + __0 + __1 <= 10
  ~~> introduce_sumleq
flat_sumleq([a,__0,__1],10)

...

However, weighted sums are expressed as sums of products, which are not
flat. Flattening a weighted sum generically makes it indistinguishable
from a sum:

1*a + 2*b + 3*c + d <= 10
  ~~> flatten_vecop
__0 + __1 + __2 + d <= 10

with new top level constraints

__0 =aux 1*a
__1 =aux 2*b
__2 =aux 3*c

Therefore, introduce_weightedsumleq_sumgeq does its own flattening, and
has a higher priority than flatten_vecop to prevent weighted sums being
generically flattened.

Having custom flattening semantics means that we can make more things
weighted sums.

For example, consider a + 2*b + 3*c*d + (e / f) + 5*(g/h) <= 18. This
rule turns this into a single flat_weightedsumleq constraint:

a + 2*b + 3*c*d + (e/f) + 5*(g/h) <= 30

  ~> introduce_weightedsumleq_sumgeq

flat_weightedsumleq([1,2,3,1,5],[a,b,__0,__1,__2],30)

with new top level constraints

__0 = c*d
__1 = e/f
__2 = g/h

The rules to turn terms into coefficient variable pairs are the following:

1. Non-weighted atom: a ~> (1,a)
2. Other non-weighted term: e ~> (1,__0), with new constraint __0 =aux e
3. Weighted atom: c*a ~> (c,a)
4. Weighted non-atom: c*e ~> (c,__0) with new constraint __0 =aux e
5. Weighted product: c*e*f ~> (c,__0) with new constraint __0 =aux (e*f)

[niklasdewally]

Coverage failing due to rust nightly bug: rust-lang/rust#135235

[ozgurakgun]

The rules to turn terms into coefficient variable pairs are the following:

1. Non-weighted atom: `a ~> (1,a)`

2. Other non-weighted term: `e ~> (1,__0), with new constraint __0 =aux e`

3. Weighted atom: `c*a ~> (c,a)`

4. Weighted non-atom: `c*e ~> (c,__0) with new constraint __0 =aux e`

5. Weighted product: `c*e*f ~> (c,__0) with new constraint __0 =aux (e*f)`

in the rules why do you need to distinguish between 4 and 5? does 4 not catch 5?

[niklasdewally]

in the rules why do you need to distinguish between 4 and 5? does 4 not catch 5?

4 is when the product has one constant child and one child that is not an atom.
In 5, the product has one constant child and many non-constant children.

5 could catch case 4, but that would result in the expression being wrapped in a product unnecessarily.

[ozgurakgun]

All looks good to me. Can you please copy/adapt the description in the PR to the documentation of introduce_weighted_sumleq_sumgeq rule before merging? the PR description is good, it would be a shame to lose it from the code.