remove SumEq expression

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.
conjure-cp · Jan 7, 2025 · 47dfea4 · 47dfea4
1 parent 08a6f04
commit 47dfea4
Show file tree

Hide file tree

Showing 17 changed files with 188 additions and 215 deletions.
diff --git a/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt
@@ -15,14 +15,20 @@ MinusEq(__0,y)
 --
 
 (x = Sum([__0, z])), 
-   ~~> sum_eq_to_sumeq ([("Minion", 4200)]) 
-SumEq([__0, z], x) 
+   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
+And([(Sum([__0, z]) <= x), (Sum([__0, z]) >= x)]) 
 
 --
 
-SumEq([__0, z], x), 
-   ~~> sumeq_to_minion ([("Minion", 4400)]) 
-And([SumLeq([__0, z], x), SumGeq([__0, z], x)]) 
+(Sum([__0, z]) <= x), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([__0, z], x) 
+
+--
+
+(Sum([__0, z]) >= x), 
+   ~~> introduce_sumgeq ([("Minion", 4400)]) 
+SumGeq([__0, z], x) 
 
 --
 
diff --git a/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt
@@ -65,14 +65,20 @@ MinusEq(__1,z)
 --
 
 (x = Sum([__0, __1, -1, a, b])), 
-   ~~> sum_eq_to_sumeq ([("Minion", 4200)]) 
-SumEq([__0, __1, -1, a, b], x) 
+   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
+And([(Sum([__0, __1, -1, a, b]) <= x), (Sum([__0, __1, -1, a, b]) >= x)]) 
 
 --
 
-SumEq([__0, __1, -1, a, b], x), 
-   ~~> sumeq_to_minion ([("Minion", 4400)]) 
-And([SumLeq([__0, __1, -1, a, b], x), SumGeq([__0, __1, -1, a, b], x)]) 
+(Sum([__0, __1, -1, a, b]) <= x), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([__0, __1, -1, a, b], x) 
+
+--
+
+(Sum([__0, __1, -1, a, b]) >= x), 
+   ~~> introduce_sumgeq ([("Minion", 4400)]) 
+SumGeq([__0, __1, -1, a, b], x) 
 
 --
 
diff --git a/...re_oxide/tests/integration/basic/sum/01-deeply-nested/input-expected-rule-trace-human.txt b/...re_oxide/tests/integration/basic/sum/01-deeply-nested/input-expected-rule-trace-human.txt
@@ -5,14 +5,20 @@ Sum([a, b, c, d, e])
 --
 
 (Sum([a, b, c, d, e]) = 5), 
-   ~~> sum_eq_to_sumeq ([("Minion", 4200)]) 
-SumEq([a, b, c, d, e], 5) 
+   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
+And([(Sum([a, b, c, d, e]) <= 5), (Sum([a, b, c, d, e]) >= 5)]) 
 
 --
 
-SumEq([a, b, c, d, e], 5), 
-   ~~> sumeq_to_minion ([("Minion", 4400)]) 
-And([SumLeq([a, b, c, d, e], 5), SumGeq([a, b, c, d, e], 5)]) 
+(Sum([a, b, c, d, e]) <= 5), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([a, b, c, d, e], 5) 
+
+--
+
+(Sum([a, b, c, d, e]) >= 5), 
+   ~~> introduce_sumgeq ([("Minion", 4400)]) 
+SumGeq([a, b, c, d, e], 5) 
 
 --
 
diff --git a/...ide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt b/...ide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt
@@ -45,14 +45,20 @@ DivEq(__0, a, 3)
 --
 
 __0 =aux Sum([x, y, z]), 
-   ~~> sum_eq_to_sumeq ([("Minion", 4200)]) 
-SumEq([x, y, z], __0) 
+   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
+And([(Sum([x, y, z]) <= __0), (Sum([x, y, z]) >= __0)]) 
 
 --
 
-SumEq([x, y, z], __0), 
-   ~~> sumeq_to_minion ([("Minion", 4400)]) 
-And([SumLeq([x, y, z], __0), SumGeq([x, y, z], __0)]) 
+(Sum([x, y, z]) <= __0), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([x, y, z], __0) 
+
+--
+
+(Sum([x, y, z]) >= __0), 
+   ~~> introduce_sumgeq ([("Minion", 4400)]) 
+SumGeq([x, y, z], __0) 
 
 --
 
diff --git a/..._oxide/tests/integration/basic/weighted-sum/01-simple/input-expected-rule-trace-human.txt b/..._oxide/tests/integration/basic/weighted-sum/01-simple/input-expected-rule-trace-human.txt
@@ -20,18 +20,6 @@ with changed declarations:
   + __2: int(6..12)
 --
 
-__0 =aux Sum([__1, __2]), 
-   ~~> sum_eq_to_sumeq ([("Minion", 4200)]) 
-SumEq([__1, __2], __0) 
-
---
-
-SumEq([__1, __2], __0), 
-   ~~> sumeq_to_minion ([("Minion", 4400)]) 
-And([SumLeq([__1, __2], __0), SumGeq([__1, __2], __0)]) 
-
---
-
 __1 =aux Product([2, x]), 
    ~~> introduce_producteq ([("Minion", 4200)]) 
 FlatProductEq(x,2,__1) 
@@ -50,3 +38,21 @@ Ineq(__0, 12, -1)
 
 --
 
+__0 =aux Sum([__1, __2]), 
+   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
+And([(Sum([__1, __2]) <= __0), (Sum([__1, __2]) >= __0)]) 
+
+--
+
+(Sum([__1, __2]) <= __0), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([__1, __2], __0) 
+
+--
+
+(Sum([__1, __2]) >= __0), 
+   ~~> introduce_sumgeq ([("Minion", 4400)]) 
+SumGeq([__1, __2], __0) 
+
+--
+
diff --git a/...s/integration/basic/weighted-sum/02-needs-normalising/input-expected-rule-trace-human.txt b/...s/integration/basic/weighted-sum/02-needs-normalising/input-expected-rule-trace-human.txt
@@ -68,18 +68,6 @@ with changed declarations:
   + __5: int(-25..-10)
 --
 
-__0 =aux Sum([__1, __2, __3, __4, __5]), 
-   ~~> sum_eq_to_sumeq ([("Minion", 4200)]) 
-SumEq([__1, __2, __3, __4, __5], __0) 
-
---
-
-SumEq([__1, __2, __3, __4, __5], __0), 
-   ~~> sumeq_to_minion ([("Minion", 4400)]) 
-And([SumLeq([__1, __2, __3, __4, __5], __0), SumGeq([__1, __2, __3, __4, __5], __0)]) 
-
---
-
 __1 =aux Product([5, x]), 
    ~~> introduce_producteq ([("Minion", 4200)]) 
 FlatProductEq(x,5,__1) 
@@ -126,3 +114,21 @@ Ineq(__0, 10, -1)
 
 --
 
+__0 =aux Sum([__1, __2, __3, __4, __5]), 
+   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
+And([(Sum([__1, __2, __3, __4, __5]) <= __0), (Sum([__1, __2, __3, __4, __5]) >= __0)]) 
+
+--
+
+(Sum([__1, __2, __3, __4, __5]) <= __0), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([__1, __2, __3, __4, __5], __0) 
+
+--
+
+(Sum([__1, __2, __3, __4, __5]) >= __0), 
+   ~~> introduce_sumgeq ([("Minion", 4400)]) 
+SumGeq([__1, __2, __3, __4, __5], __0) 
+
+--
+
diff --git a/...e/tests/integration/eprime-minion/partial-eval-01-add/input-expected-rule-trace-human.txt b/...e/tests/integration/eprime-minion/partial-eval-01-add/input-expected-rule-trace-human.txt
@@ -11,20 +11,20 @@ Sum([x, y, 35])
 --
 
 (Sum([x, y, 35]) = 100), 
-   ~~> sum_eq_to_sumeq ([("Minion", 4200)]) 
-SumEq([x, y, 35], 100) 
+   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
+And([(Sum([x, y, 35]) <= 100), (Sum([x, y, 35]) >= 100)]) 
 
 --
 
-SumEq([x, y, 35], 100), 
-   ~~> partial_evaluator ([("Base", 9000)]) 
-SumEq([x, y], 65) 
+(Sum([x, y, 35]) <= 100), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([x, y, 35], 100) 
 
 --
 
-SumEq([x, y], 65), 
-   ~~> sumeq_to_minion ([("Minion", 4400)]) 
-And([SumLeq([x, y], 65), SumGeq([x, y], 65)]) 
+(Sum([x, y, 35]) >= 100), 
+   ~~> introduce_sumgeq ([("Minion", 4400)]) 
+SumGeq([x, y, 35], 100) 
 
 --
 
diff --git a/...ests/integration/eprime-minion/partial-eval-01-add/input.expected-rewrite.serialised.json b/...ests/integration/eprime-minion/partial-eval-01-add/input.expected-rewrite.serialised.json
@@ -23,11 +23,16 @@
                   "Reference": {
                     "UserName": "y"
                   }
+                },
+                {
+                  "Literal": {
+                    "Int": 35
+                  }
                 }
               ],
               {
                 "Literal": {
-                  "Int": 65
+                  "Int": 100
                 }
               }
             ]
@@ -48,11 +53,16 @@
                   "Reference": {
                     "UserName": "y"
                   }
+                },
+                {
+                  "Literal": {
+                    "Int": 35
+                  }
                 }
               ],
               {
                 "Literal": {
-                  "Int": 65
+                  "Int": 100
                 }
               }
             ]

diff --git a/...xide/tests/integration/eprime-minion/partial-eval-add/input-expected-rule-trace-human.txt b/...xide/tests/integration/eprime-minion/partial-eval-add/input-expected-rule-trace-human.txt
@@ -11,20 +11,20 @@ Sum([x, y, 35])
 --
 
 (Sum([x, y, 35]) = 100), 
-   ~~> sum_eq_to_sumeq ([("Minion", 4200)]) 
-SumEq([x, y, 35], 100) 
+   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
+And([(Sum([x, y, 35]) <= 100), (Sum([x, y, 35]) >= 100)]) 
 
 --
 
-SumEq([x, y, 35], 100), 
-   ~~> partial_evaluator ([("Base", 9000)]) 
-SumEq([x, y], 65) 
+(Sum([x, y, 35]) <= 100), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([x, y, 35], 100) 
 
 --
 
-SumEq([x, y], 65), 
-   ~~> sumeq_to_minion ([("Minion", 4400)]) 
-And([SumLeq([x, y], 65), SumGeq([x, y], 65)]) 
+(Sum([x, y, 35]) >= 100), 
+   ~~> introduce_sumgeq ([("Minion", 4400)]) 
+SumGeq([x, y, 35], 100) 
 
 --
 
diff --git a/...e/tests/integration/eprime-minion/partial-eval-add/input.expected-rewrite.serialised.json b/...e/tests/integration/eprime-minion/partial-eval-add/input.expected-rewrite.serialised.json
@@ -23,11 +23,16 @@
                   "Reference": {
                     "UserName": "y"
                   }
+                },
+                {
+                  "Literal": {
+                    "Int": 35
+                  }
                 }
               ],
               {
                 "Literal": {
-                  "Int": 65
+                  "Int": 100
                 }
               }
             ]
@@ -48,11 +53,16 @@
                   "Reference": {
                     "UserName": "y"
                   }
+                },
+                {
+                  "Literal": {
+                    "Int": 35
+                  }
                 }
               ],
               {
                 "Literal": {
-                  "Int": 65
+                  "Int": 100
                 }
               }
             ]

diff --git a/conjure_oxide/tests/integration/eprime-minion/xyz/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/eprime-minion/xyz/input-expected-rule-trace-human.txt
@@ -5,14 +5,20 @@ Sum([a, b, c])
 --
 
 (Sum([a, b, c]) = 4), 
-   ~~> sum_eq_to_sumeq ([("Minion", 4200)]) 
-SumEq([a, b, c], 4) 
+   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
+And([(Sum([a, b, c]) <= 4), (Sum([a, b, c]) >= 4)]) 
 
 --
 
-SumEq([a, b, c], 4), 
-   ~~> sumeq_to_minion ([("Minion", 4400)]) 
-And([SumLeq([a, b, c], 4), SumGeq([a, b, c], 4)]) 
+(Sum([a, b, c]) <= 4), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([a, b, c], 4) 
+
+--
+
+(Sum([a, b, c]) >= 4), 
+   ~~> introduce_sumgeq ([("Minion", 4400)]) 
+SumGeq([a, b, c], 4) 
 
 --
 

diff --git a/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt
@@ -22,21 +22,27 @@ with changed declarations:
   + __1: int(1..4)
 --
 
+(__0 >= 2), 
+   ~~> geq_to_ineq ([("Minion", 4100)]) 
+Ineq(2, __0, 0) 
+
+--
+
 (x = Sum([__1, 1])), 
-   ~~> sum_eq_to_sumeq ([("Minion", 4200)]) 
-SumEq([__1, 1], x) 
+   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
+And([(Sum([__1, 1]) <= x), (Sum([__1, 1]) >= x)]) 
 
 --
 
-SumEq([__1, 1], x), 
-   ~~> sumeq_to_minion ([("Minion", 4400)]) 
-And([SumLeq([__1, 1], x), SumGeq([__1, 1], x)]) 
+(Sum([__1, 1]) <= x), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([__1, 1], x) 
 
 --
 
-(__0 >= 2), 
-   ~~> geq_to_ineq ([("Minion", 4100)]) 
-Ineq(2, __0, 0) 
+(Sum([__1, 1]) >= x), 
+   ~~> introduce_sumgeq ([("Minion", 4400)]) 
+SumGeq([__1, 1], x) 
 
 --