rules/minion: apply weighted sum more often (negatives, equality)

These changes were motivated by the `basic/abs/03-flatten` test: it
should be a weighted sum, but is not. With this commit, this becomes a
weighted sum.

* Add more cases to weighted sum, allowing negated expressions to be put
  inside the weighted sum.

  +  -x ~> (-1,x) where x is an atom
  +  -e ~> (-1,__1), with new constraint` __1=aux e`

  An alternative approach would be to add a normalisation rule `-e ~> -1
  * e`; however, I don't think this should only happen inside sums, not
  in general.

* Turn non-flat weighted sum equals expressions into weighted sums.

  Expressions of the form `c*e1 + d*e2 + .. = t`, (where e1,e2 are
  non-flat) were not being turned into weighted sums.

  `sum_eq_to_inequalities` needs to run before a sumeq can be turned
  into a weighted sum, as `introduce_weighted_sumleq_sumgeq` only works
  on inequalites. However, flattening has a higher priority than this
  rule, which makes `introduce_weighted_sumleq_sumgeq` unapplicable to these
  expressions. (see 2833c5f (Convert weighted sums to Minion, 2025-01-07)).

  To fix this, this commit makes `sum_eq_to_inequalities` a higher
  priority than the flattening rules.

  A consequence of this is that more auxiliary variables are introduced
  than before, because non-flat expressions are being duplicated.

  For example:

  ```
  $ before

  (a/b) + c = d
  ~> __1 + c = d  [flatten_vecop]
  ~> __1 + c <= d /\ __1 + c >= d [sum_eq_to_inequalities]

  $ this commit

  (a/b) + c = d
  ~> (a/b) + c <= d /\ (a/b) + c >= d [sum_eq_to_inequalities]
  ~> __1 + c <= d  /\ __1 + c >= d    [flatten_vecop]
  ```

  I don't think this is a problem, however: because these are
  syntactically identical, CSE should easily merge them (once we
  implement it).

* Do not flatten sums inside leqs/geqs

  The priority change above causes an infinite cycle to occur between
  `flatten_binop` and `sum_eq_to_inequalities`:

  ```
  sum([|a|, |b|]) = c

    ~~> sum_eq_to_inequalities

  (sum([|a|, |b|]) <= c /\ sum([|a|, |b|]) <= c)

  --

  sum([|a|, |b|]) <= c

    ~~> flatten_binop

   __1 <= c

   with new top level constraints:

   __1 =aux sum([|a| , |b|])

   --

  sum([|a|, |b|]) =aux __1

    ~~> sum_eq_to_inequalities

  (sum([|a|, |b|]) <= __1 /\ sum([|a|, |b|]) <= __1)
   ```

   To fix this, this commit adds a special case to `flatten_binop` to
   ignore any Sum children of Leq and Geq.

conjure_oxide/tests/integration/basic/abs/01-simple/input-expected-rule-trace-human.txt

@@ -9,6 +9,12 @@ such that
 
 --
 
+(Sum([|x|, |y|]) = 10), 
+   ~~> sum_eq_to_inequalities ([("Minion", 4500)]) 
+And([(Sum([|x|, |y|]) <= 10), (Sum([|x|, |y|]) >= 10)]) 
+
+--
+
 Sum([|x|, |y|]), 
    ~~> flatten_vecop ([("Minion", 4200)]) 
 Sum([__0, __1]) 
@@ -20,6 +26,12 @@ new constraints:
   __1 =aux |y|
 --
 
+(Sum([__0, __1]) <= 10), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([__0, __1], 10) 
+
+--
+
 __0 =aux |x|, 
    ~~> introduce_abseq ([("Minion", 4400)]) 
 AbsEq(__0,x) 
@@ -32,21 +44,32 @@ AbsEq(__1,y)
 
 --
 
-(Sum([__0, __1]) = 10), 
-   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
-And([(Sum([__0, __1]) <= 10), (Sum([__0, __1]) >= 10)]) 
+Sum([|x|, |y|]), 
+   ~~> flatten_vecop ([("Minion", 4200)]) 
+Sum([__2, __3]) 
+new variables:
+  __2: int(0..5)
+  __3: int(0..5)
+new constraints:
+  __2 =aux |x|
+  __3 =aux |y|
+--
+
+(Sum([__2, __3]) >= 10), 
+   ~~> introduce_sumgeq ([("Minion", 4400)]) 
+SumGeq([__2, __3], 10) 
 
 --
 
-(Sum([__0, __1]) <= 10), 
-   ~~> introduce_sumleq ([("Minion", 4400)]) 
-SumLeq([__0, __1], 10) 
+__2 =aux |x|, 
+   ~~> introduce_abseq ([("Minion", 4400)]) 
+AbsEq(__2,x) 
 
 --
 
-(Sum([__0, __1]) >= 10), 
-   ~~> introduce_sumgeq ([("Minion", 4400)]) 
-SumGeq([__0, __1], 10) 
+__3 =aux |y|, 
+   ~~> introduce_abseq ([("Minion", 4400)]) 
+AbsEq(__3,y) 
 
 --
 
@@ -56,10 +79,14 @@ find x: int(-5..5)
 find y: int(-5..5)
 find __0: int(0..5)
 find __1: int(0..5)
+find __2: int(0..5)
+find __3: int(0..5)
 
 such that
 
-And([SumLeq([__0, __1], 10), SumGeq([__0, __1], 10)]),
+And([SumLeq([__0, __1], 10), SumGeq([__2, __3], 10)]),
 AbsEq(__0,x),
-AbsEq(__1,y)
+AbsEq(__1,y),
+AbsEq(__2,x),
+AbsEq(__3,y)
 

conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-minion.solutions.json

@@ -2,24 +2,32 @@
   {
     "__0": 5,
     "__1": 5,
+    "__2": 5,
+    "__3": 5,
     "x": -5,
     "y": -5
   },
   {
     "__0": 5,
     "__1": 5,
+    "__2": 5,
+    "__3": 5,
     "x": -5,
     "y": 5
   },
   {
     "__0": 5,
     "__1": 5,
+    "__2": 5,
+    "__3": 5,
     "x": 5,
     "y": -5
   },
   {
     "__0": 5,
     "__1": 5,
+    "__2": 5,
+    "__3": 5,
     "x": 5,
     "y": 5
   }

conjure_oxide/tests/integration/basic/abs/01-simple/input.expected-rewrite.serialised.json

@@ -41,12 +41,12 @@
               [
                 {
                   "Reference": {
-                    "MachineName": 0
+                    "MachineName": 2
                   }
                 },
                 {
                   "Reference": {
-                    "MachineName": 1
+                    "MachineName": 3
                   }
                 }
               ],
@@ -95,9 +95,45 @@
           }
         }
       ]
+    },
+    {
+      "FlatAbsEq": [
+        {
+          "clean": false,
+          "etype": null
+        },
+        {
+          "Reference": {
+            "MachineName": 2
+          }
+        },
+        {
+          "Reference": {
+            "UserName": "x"
+          }
+        }
+      ]
+    },
+    {
+      "FlatAbsEq": [
+        {
+          "clean": false,
+          "etype": null
+        },
+        {
+          "Reference": {
+            "MachineName": 3
+          }
+        },
+        {
+          "Reference": {
+            "UserName": "y"
+          }
+        }
+      ]
     }
   ],
-  "next_var": 2,
+  "next_var": 4,
   "variables": [
     [
       {
@@ -133,6 +169,40 @@
         }
       }
     ],
+    [
+      {
+        "MachineName": 2
+      },
+      {
+        "domain": {
+          "IntDomain": [
+            {
+              "Bounded": [
+                0,
+                5
+              ]
+            }
+          ]
+        }
+      }
+    ],
+    [
+      {
+        "MachineName": 3
+      },
+      {
+        "domain": {
+          "IntDomain": [
+            {
+              "Bounded": [
+                0,
+                5
+              ]
+            }
+          ]
+        }
+      }
+    ],
     [
       {
         "UserName": "x"

conjure_oxide/tests/integration/basic/abs/02-neg/input-expected-rule-trace-human.txt

@@ -21,6 +21,12 @@ such that
 
 --
 
+(Sum([|x|, |y|]) = 10), 
+   ~~> sum_eq_to_inequalities ([("Minion", 4500)]) 
+And([(Sum([|x|, |y|]) <= 10), (Sum([|x|, |y|]) >= 10)]) 
+
+--
+
 Sum([|x|, |y|]), 
    ~~> flatten_vecop ([("Minion", 4200)]) 
 Sum([__0, __1]) 
@@ -32,6 +38,12 @@ new constraints:
   __1 =aux |y|
 --
 
+(Sum([__0, __1]) <= 10), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([__0, __1], 10) 
+
+--
+
 __0 =aux |x|, 
    ~~> introduce_abseq ([("Minion", 4400)]) 
 AbsEq(__0,x) 
@@ -44,21 +56,32 @@ AbsEq(__1,y)
 
 --
 
-(Sum([__0, __1]) = 10), 
-   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
-And([(Sum([__0, __1]) <= 10), (Sum([__0, __1]) >= 10)]) 
+Sum([|x|, |y|]), 
+   ~~> flatten_vecop ([("Minion", 4200)]) 
+Sum([__2, __3]) 
+new variables:
+  __2: int(0..5)
+  __3: int(0..5)
+new constraints:
+  __2 =aux |x|
+  __3 =aux |y|
+--
+
+(Sum([__2, __3]) >= 10), 
+   ~~> introduce_sumgeq ([("Minion", 4400)]) 
+SumGeq([__2, __3], 10) 
 
 --
 
-(Sum([__0, __1]) <= 10), 
-   ~~> introduce_sumleq ([("Minion", 4400)]) 
-SumLeq([__0, __1], 10) 
+__2 =aux |x|, 
+   ~~> introduce_abseq ([("Minion", 4400)]) 
+AbsEq(__2,x) 
 
 --
 
-(Sum([__0, __1]) >= 10), 
-   ~~> introduce_sumgeq ([("Minion", 4400)]) 
-SumGeq([__0, __1], 10) 
+__3 =aux |y|, 
+   ~~> introduce_abseq ([("Minion", 4400)]) 
+AbsEq(__3,y) 
 
 --
 
@@ -68,10 +91,14 @@ find x: int(-5..5)
 find y: int(-5..5)
 find __0: int(0..5)
 find __1: int(0..5)
+find __2: int(0..5)
+find __3: int(0..5)
 
 such that
 
-And([SumLeq([__0, __1], 10), SumGeq([__0, __1], 10)]),
+And([SumLeq([__0, __1], 10), SumGeq([__2, __3], 10)]),
 AbsEq(__0,x),
-AbsEq(__1,y)
+AbsEq(__1,y),
+AbsEq(__2,x),
+AbsEq(__3,y)
 

conjure_oxide/tests/integration/basic/abs/02-neg/input.expected-minion.solutions.json

@@ -2,24 +2,32 @@
   {
     "__0": 5,
     "__1": 5,
+    "__2": 5,
+    "__3": 5,
     "x": -5,
     "y": -5
   },
   {
     "__0": 5,
     "__1": 5,
+    "__2": 5,
+    "__3": 5,
     "x": -5,
     "y": 5
   },
   {
     "__0": 5,
     "__1": 5,
+    "__2": 5,
+    "__3": 5,
     "x": 5,
     "y": -5
   },
   {
     "__0": 5,
     "__1": 5,
+    "__2": 5,
+    "__3": 5,
     "x": 5,
     "y": 5
   }