From 0063a1c8ab64d7c90cd54a317d54664a7dd047bd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=96zg=C3=BCr=20Akg=C3=BCn?= <ozgurakgun@gmail.com>
Date: Fri, 10 Jan 2025 21:19:27 +0000
Subject: [PATCH 1/3] unify flatten_unop, flatten_binop, flatten_vecop

---
 crates/conjure_core/src/rules/minion.rs | 60 ++-----------------------
 1 file changed, 4 insertions(+), 56 deletions(-)

diff --git a/crates/conjure_core/src/rules/minion.rs b/crates/conjure_core/src/rules/minion.rs
index 6ed43e144c..187563cd4a 100644
--- a/crates/conjure_core/src/rules/minion.rs
+++ b/crates/conjure_core/src/rules/minion.rs
@@ -499,7 +499,7 @@ fn introduce_minuseq_from_aux_decl(expr: &Expr, _: &Model) -> ApplicationResult
 }
 
 #[register_rule(("Minion", 4200))]
-fn flatten_binop(expr: &Expr, model: &Model) -> ApplicationResult {
+fn flatten_generic(expr: &Expr, model: &Model) -> ApplicationResult {
     if !matches!(
         expr,
         Expr::SafeDiv(_, _, _)
@@ -507,65 +507,13 @@ fn flatten_binop(expr: &Expr, model: &Model) -> ApplicationResult {
             | Expr::SafeMod(_, _, _)
             | Expr::Leq(_, _, _)
             | Expr::Geq(_, _, _)
+            | Expr::Abs(_, _)
+            | Expr::Sum(_, _)
+            | Expr::Product(_, _)
     ) {
         return Err(RuleNotApplicable);
     }
 
-    let mut children = expr.children();
-    debug_assert_eq!(children.len(), 2);
-
-    let mut model = model.clone();
-    let mut num_changed = 0;
-    let mut new_tops: Vec<Expr> = vec![];
-
-    for child in children.iter_mut() {
-        if let Some(aux_var_info) = to_aux_var(child, &model) {
-            model = aux_var_info.model();
-            new_tops.push(aux_var_info.top_level_expr());
-            *child = aux_var_info.as_expr();
-            num_changed += 1;
-        }
-    }
-
-    if num_changed == 0 {
-        return Err(RuleNotApplicable);
-    }
-
-    let expr = expr.with_children(children);
-    Ok(Reduction::new(expr, new_tops, model.variables))
-}
-
-#[register_rule(("Minion", 4200))]
-fn flatten_unop(expr: &Expr, model: &Model) -> ApplicationResult {
-    if !matches!(expr, Expr::Abs(_, _)) {
-        return Err(RuleNotApplicable);
-    }
-
-    let mut children = expr.children();
-    debug_assert_eq!(children.len(), 1);
-    let child = &mut children[0];
-
-    let mut model = model.clone();
-    let mut new_tops: Vec<Expr> = vec![];
-
-    if let Some(aux_var_info) = to_aux_var(child, &model) {
-        model = aux_var_info.model();
-        new_tops.push(aux_var_info.top_level_expr());
-        *child = aux_var_info.as_expr();
-    } else {
-        return Err(RuleNotApplicable);
-    }
-
-    let expr = expr.with_children(children);
-    Ok(Reduction::new(expr, new_tops, model.variables))
-}
-
-#[register_rule(("Minion", 4200))]
-fn flatten_vecop(expr: &Expr, model: &Model) -> ApplicationResult {
-    if !matches!(expr, Expr::Sum(_, _) | Expr::Product(_, _)) {
-        return Err(RuleNotApplicable);
-    }
-
     let mut children = expr.children();
 
     let mut model = model.clone();

From 9bda933dced1387fc828084b6d36d0c882513229 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=96zg=C3=BCr=20Akg=C3=BCn?= <ozgurakgun@gmail.com>
Date: Fri, 10 Jan 2025 21:21:34 +0000
Subject: [PATCH 2/3] update test files - only change is applied rule names

---
 .../abs/01-simple/input-expected-rule-trace-human.txt     | 2 +-
 .../basic/abs/02-neg/input-expected-rule-trace-human.txt  | 2 +-
 .../abs/03-nested/input-expected-rule-trace-human.txt     | 8 ++++----
 .../abs/04-bounds/input-expected-rule-trace-human.txt     | 2 +-
 .../basic/div/04/input-expected-rule-trace-human.txt      | 2 +-
 .../basic/div/05/div-05-expected-rule-trace-human.txt     | 2 +-
 .../basic/div/06/div-06-expected-rule-trace-human.txt     | 2 +-
 .../basic/mod/04/input-expected-rule-trace-human.txt      | 2 +-
 .../basic/mod/05/mod-05-expected-rule-trace-human.txt     | 2 +-
 .../basic/mod/06/mod-06-expected-rule-trace-human.txt     | 2 +-
 .../neg/02-nested-neg/input-expected-rule-trace-human.txt | 2 +-
 .../input-expected-rule-trace-human.txt                   | 2 +-
 .../basic/neg/05-sum/input-expected-rule-trace-human.txt  | 2 +-
 .../neg/06-sum-nested/input-expected-rule-trace-human.txt | 2 +-
 .../product/01-simple/input-expected-rule-trace-human.txt | 2 +-
 .../input-expected-rule-trace-human.txt                   | 2 +-
 .../03-simple-eq/input-expected-rule-trace-human.txt      | 2 +-
 .../input-expected-rule-trace-human.txt                   | 4 ++--
 .../input-expected-rule-trace-human.txt                   | 6 +++---
 .../input-expected-rule-trace-human.txt                   | 4 ++--
 .../input-expected-rule-trace-human.txt                   | 4 ++--
 .../input-expected-rule-trace-human.txt                   | 6 +++---
 .../input-expected-rule-trace-human.txt                   | 4 ++--
 23 files changed, 34 insertions(+), 34 deletions(-)

diff --git a/conjure_oxide/tests/integration/basic/abs/01-simple/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/abs/01-simple/input-expected-rule-trace-human.txt
index 703aa4bd90..ea223432b8 100644
--- a/conjure_oxide/tests/integration/basic/abs/01-simple/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/abs/01-simple/input-expected-rule-trace-human.txt
@@ -10,7 +10,7 @@ such that
 --
 
 Sum([|x|, |y|]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__0, __1]) 
 new variables:
   __0: int(0..5)
diff --git a/conjure_oxide/tests/integration/basic/abs/02-neg/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/abs/02-neg/input-expected-rule-trace-human.txt
index e94addf01e..1fb17915a7 100644
--- a/conjure_oxide/tests/integration/basic/abs/02-neg/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/abs/02-neg/input-expected-rule-trace-human.txt
@@ -22,7 +22,7 @@ such that
 --
 
 Sum([|x|, |y|]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__0, __1]) 
 new variables:
   __0: int(0..5)
diff --git a/conjure_oxide/tests/integration/basic/abs/03-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/abs/03-nested/input-expected-rule-trace-human.txt
index 65309324be..24652f2ee3 100644
--- a/conjure_oxide/tests/integration/basic/abs/03-nested/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/abs/03-nested/input-expected-rule-trace-human.txt
@@ -155,7 +155,7 @@ And([(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]) = 10)]),
 --
 
 Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__0, __1]) 
 new variables:
   __0: int(0..10)
@@ -166,7 +166,7 @@ new constraints:
 --
 
 |Sum([SafeDiv(x, 2), y, -(z)])|, 
-   ~~> flatten_unop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 |__2| 
 new variables:
   __2: int(-10..8)
@@ -181,7 +181,7 @@ AbsEq(__0,__2)
 --
 
 SafeDiv(|y|, 2), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(__3, 2) 
 new variables:
   __3: int(0..5)
@@ -202,7 +202,7 @@ DivEq(__3, 2, __1)
 --
 
 Sum([SafeDiv(x, 2), y, -(z)]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__4, y, __5]) 
 new variables:
   __4: int(-3..1)
diff --git a/conjure_oxide/tests/integration/basic/abs/04-bounds/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/abs/04-bounds/input-expected-rule-trace-human.txt
index 085ec347a6..255b3d8fb4 100644
--- a/conjure_oxide/tests/integration/basic/abs/04-bounds/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/abs/04-bounds/input-expected-rule-trace-human.txt
@@ -10,7 +10,7 @@ such that
 --
 
 Product([y, |x|]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Product([y, __0]) 
 new variables:
   __0: int(0..3)
diff --git a/conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt
index 307ee877ae..bc4524cbce 100644
--- a/conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt
@@ -53,7 +53,7 @@ Not((c != 0)),
 --
 
 (a != SafeDiv(b, c)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (a != __0) 
 new variables:
   __0: int(0..3)
diff --git a/conjure_oxide/tests/integration/basic/div/05/div-05-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/div/05/div-05-expected-rule-trace-human.txt
index 061f3c09e4..0390a26a05 100644
--- a/conjure_oxide/tests/integration/basic/div/05/div-05-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/div/05/div-05-expected-rule-trace-human.txt
@@ -35,7 +35,7 @@ And([(c != 0)]),
 --
 
 (a != SafeDiv(b, c)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (a != __0) 
 new variables:
   __0: int(0..3)
diff --git a/conjure_oxide/tests/integration/basic/div/06/div-06-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/div/06/div-06-expected-rule-trace-human.txt
index 307ee877ae..bc4524cbce 100644
--- a/conjure_oxide/tests/integration/basic/div/06/div-06-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/div/06/div-06-expected-rule-trace-human.txt
@@ -53,7 +53,7 @@ Not((c != 0)),
 --
 
 (a != SafeDiv(b, c)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (a != __0) 
 new variables:
   __0: int(0..3)
diff --git a/conjure_oxide/tests/integration/basic/mod/04/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/mod/04/input-expected-rule-trace-human.txt
index a663fdf320..49f10cb879 100644
--- a/conjure_oxide/tests/integration/basic/mod/04/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/mod/04/input-expected-rule-trace-human.txt
@@ -53,7 +53,7 @@ Not((c != 0)),
 --
 
 (a != SafeMod(b,c)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (a != __0) 
 new variables:
   __0: int(0..2)
diff --git a/conjure_oxide/tests/integration/basic/mod/05/mod-05-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/mod/05/mod-05-expected-rule-trace-human.txt
index 98deb9ba20..13b6ed3058 100644
--- a/conjure_oxide/tests/integration/basic/mod/05/mod-05-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/mod/05/mod-05-expected-rule-trace-human.txt
@@ -35,7 +35,7 @@ And([(c != 0)]),
 --
 
 (a != SafeMod(b,c)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (a != __0) 
 new variables:
   __0: int(0..2)
diff --git a/conjure_oxide/tests/integration/basic/mod/06/mod-06-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/mod/06/mod-06-expected-rule-trace-human.txt
index a663fdf320..49f10cb879 100644
--- a/conjure_oxide/tests/integration/basic/mod/06/mod-06-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/mod/06/mod-06-expected-rule-trace-human.txt
@@ -53,7 +53,7 @@ Not((c != 0)),
 --
 
 (a != SafeMod(b,c)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (a != __0) 
 new variables:
   __0: int(0..2)
diff --git a/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input-expected-rule-trace-human.txt
index 59a38fffdc..058bfc20b5 100644
--- a/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input-expected-rule-trace-human.txt
@@ -35,7 +35,7 @@ And([(z != 0)]),
 --
 
 SafeDiv(-(y), z), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(__0, z) 
 new variables:
   __0: int(-1..1)
diff --git a/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt
index 34d86bbb44..0167ef8bf6 100644
--- a/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt
@@ -83,7 +83,7 @@ And([(x = SafeDiv(-(SafeDiv(y, z)), z)), (z != 0), (z != 0)])
 --
 
 SafeDiv(-(SafeDiv(y, z)), z), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(__0, z) 
 new variables:
   __0: int(-1..1)
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
index 538170342c..7651f9eb72 100644
--- 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
@@ -11,7 +11,7 @@ such that
 --
 
 Sum([-(y), z]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__0, z]) 
 new variables:
   __0: int(-1..1)
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
index 19fb2450aa..106c88aa29 100644
--- 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
@@ -55,7 +55,7 @@ a
 --
 
 Sum([-(y), -(z), -1, a, b]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__0, __1, -1, a, b]) 
 new variables:
   __0: int(-1..1)
diff --git a/conjure_oxide/tests/integration/basic/product/01-simple/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/product/01-simple/input-expected-rule-trace-human.txt
index 2c75cd55bc..60afeb8b18 100644
--- a/conjure_oxide/tests/integration/basic/product/01-simple/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/product/01-simple/input-expected-rule-trace-human.txt
@@ -29,7 +29,7 @@ Sum([15, -1]),
 --
 
 (Product([x, y, z]) <= 14), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__0 <= 14) 
 new variables:
   __0: int(8..64)
diff --git a/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt
index 3b136688d1..39edfac116 100644
--- a/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt
@@ -42,7 +42,7 @@ And([(a != 0)]),
 --
 
 SafeDiv(Sum([x, y, z]), a), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(__0, a) 
 new variables:
   __0: int(6..14)
diff --git a/conjure_oxide/tests/integration/basic/weighted-sum/03-simple-eq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/weighted-sum/03-simple-eq/input-expected-rule-trace-human.txt
index 3784b7b1fa..129c1ec18b 100644
--- a/conjure_oxide/tests/integration/basic/weighted-sum/03-simple-eq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/weighted-sum/03-simple-eq/input-expected-rule-trace-human.txt
@@ -10,7 +10,7 @@ such that
 --
 
 Sum([Product([2, x]), Product([3, y])]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__0, __1]) 
 new variables:
   __0: int(4..8)
diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt
index 7735749dca..f516e70283 100644
--- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt
@@ -71,7 +71,7 @@ And([(SafeDiv(x, SafeDiv(y, z)) = 10), (SafeDiv(y, z) != 0), (z != 0)])
 --
 
 SafeDiv(x, SafeDiv(y, z)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(x, __0) 
 new variables:
   __0: int(0..5)
@@ -86,7 +86,7 @@ DivEq(x, __0, 10)
 --
 
 (SafeDiv(y, z) != 0), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__1 != 0) 
 new variables:
   __1: int(0..5)
diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt
index 2aac0466cd..fcf1e61353 100644
--- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt
@@ -71,7 +71,7 @@ And([(SafeDiv(x, SafeDiv(y, z)) != 10), (SafeDiv(y, z) != 0), (z != 0)])
 --
 
 (SafeDiv(x, SafeDiv(y, z)) != 10), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__0 != 10) 
 new variables:
   __0: int(0..20)
@@ -80,7 +80,7 @@ new constraints:
 --
 
 (SafeDiv(y, z) != 0), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__1 != 0) 
 new variables:
   __1: int(0..5)
@@ -89,7 +89,7 @@ new constraints:
 --
 
 SafeDiv(x, SafeDiv(y, z)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(x, __2) 
 new variables:
   __2: int(0..5)
diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt
index 1b8bbf1d1e..e4506e8720 100644
--- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt
@@ -95,7 +95,7 @@ Not((z != 0)),
 --
 
 (SafeDiv(x, SafeDiv(y, z)) != 10), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__0 != 10) 
 new variables:
   __0: int(0..20)
@@ -110,7 +110,7 @@ DivEq(y, z, 0)
 --
 
 SafeDiv(x, SafeDiv(y, z)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(x, __1) 
 new variables:
   __1: int(0..5)
diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt
index 05b5a442a7..061ac06d5d 100644
--- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt
@@ -71,7 +71,7 @@ And([(SafeMod(x,SafeMod(y,z)) = 3), (SafeMod(y,z) != 0), (z != 0)])
 --
 
 SafeMod(x,SafeMod(y,z)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeMod(x,__0) 
 new variables:
   __0: int(0..5)
@@ -86,7 +86,7 @@ ModEq(x, __0, 3)
 --
 
 (SafeMod(y,z) != 0), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__1 != 0) 
 new variables:
   __1: int(0..5)
diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt
index dbdbcba0e3..198e95ff68 100644
--- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt
@@ -71,7 +71,7 @@ And([(SafeMod(x,SafeMod(y,z)) != 3), (SafeMod(y,z) != 0), (z != 0)])
 --
 
 (SafeMod(x,SafeMod(y,z)) != 3), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__0 != 3) 
 new variables:
   __0: int(0..2)
@@ -80,7 +80,7 @@ new constraints:
 --
 
 (SafeMod(y,z) != 0), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__1 != 0) 
 new variables:
   __1: int(0..3)
@@ -89,7 +89,7 @@ new constraints:
 --
 
 SafeMod(x,SafeMod(y,z)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeMod(x,__2) 
 new variables:
   __2: int(0..3)
diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt
index f18cba67c1..6a19e66fba 100644
--- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt
@@ -95,7 +95,7 @@ Not((z != 0)),
 --
 
 (SafeMod(x,SafeMod(y,z)) != 3), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__0 != 3) 
 new variables:
   __0: int(0..2)
@@ -110,7 +110,7 @@ ModEq(y, z, 0)
 --
 
 SafeMod(x,SafeMod(y,z)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeMod(x,__1) 
 new variables:
   __1: int(0..3)

From d793ded6d93d89d4c055570838194eb425e353b6 Mon Sep 17 00:00:00 2001
From: Niklas Dewally <niklas@dewally.com>
Date: Fri, 10 Jan 2025 22:54:10 +0000
Subject: [PATCH 3/3] rules/minion: remove `flatten_minus_eq`

Instead, use `flatten_generic` to flatten `Neg` expressions, and
`introduce_minuseq_from_aux_var` and `introduce_minuseq_from_eq` to
create FlatMinusEq expressions.

This is consistent with other expressions, which have simpler
introduction functions that expect flat input, and rely on
`flatten_generic` to make the input flat.
---
 .../input-expected-rule-trace-human.txt       | 12 +++-
 .../input-expected-rule-trace-human.txt       | 12 +++-
 crates/conjure_core/src/rules/minion.rs       | 59 +------------------
 3 files changed, 19 insertions(+), 64 deletions(-)

diff --git a/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt
index fac461436e..af9dc8f25c 100644
--- a/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt
@@ -46,15 +46,21 @@ And([(z != 0)]),
 
 --
 
-(x = -(SafeDiv(y, z))), 
-   ~~> flatten_minuseq ([("Minion", 4200)]) 
-MinusEq(x,__0) 
+-(SafeDiv(y, z)), 
+   ~~> flatten_generic ([("Minion", 4200)]) 
+-(__0) 
 new variables:
   __0: int(-1..1)
 new constraints:
   __0 =aux SafeDiv(y, z)
 --
 
+(x = -(__0)), 
+   ~~> introduce_minuseq_from_eq ([("Minion", 4400)]) 
+MinusEq(x,__0) 
+
+--
+
 __0 =aux SafeDiv(y, z), 
    ~~> introduce_diveq ([("Minion", 4200)]) 
 DivEq(y, z, __0) 
diff --git a/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt
index 0167ef8bf6..afb1d94635 100644
--- a/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt
+++ b/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt
@@ -97,15 +97,21 @@ DivEq(__0, z, x)
 
 --
 
-__0 =aux -(SafeDiv(y, z)), 
-   ~~> flatten_minuseq ([("Minion", 4200)]) 
-MinusEq(__0,__1) 
+-(SafeDiv(y, z)), 
+   ~~> flatten_generic ([("Minion", 4200)]) 
+-(__1) 
 new variables:
   __1: int(-1..1)
 new constraints:
   __1 =aux SafeDiv(y, z)
 --
 
+__0 =aux -(__1), 
+   ~~> introduce_minuseq_from_aux_decl ([("Minion", 4400)]) 
+MinusEq(__0,__1) 
+
+--
+
 __1 =aux SafeDiv(y, z), 
    ~~> introduce_diveq ([("Minion", 4200)]) 
 DivEq(y, z, __1) 
diff --git a/crates/conjure_core/src/rules/minion.rs b/crates/conjure_core/src/rules/minion.rs
index 187563cd4a..c7a8669315 100644
--- a/crates/conjure_core/src/rules/minion.rs
+++ b/crates/conjure_core/src/rules/minion.rs
@@ -2,11 +2,8 @@
 /*        Rules for translating to Minion-supported constraints         */
 /************************************************************************/
 
-use std::borrow::Borrow as _;
-
 use crate::ast::{Atom, DecisionVariable, Domain, Expression as Expr, Literal as Lit};
 
-use crate::ast::Name;
 use crate::metadata::Metadata;
 use crate::rule_engine::{
     register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction,
@@ -510,6 +507,7 @@ fn flatten_generic(expr: &Expr, model: &Model) -> ApplicationResult {
             | Expr::Abs(_, _)
             | Expr::Sum(_, _)
             | Expr::Product(_, _)
+            | Expr::Neg(_, _)
     ) {
         return Err(RuleNotApplicable);
     }
@@ -570,61 +568,6 @@ fn flatten_eq(expr: &Expr, model: &Model) -> ApplicationResult {
     Ok(Reduction::new(expr, new_tops, model.variables))
 }
 
-/// Flattens `a=-e`, where e is a non-atomic expression.
-///
-/// ```text
-/// a = -e ~> a = MinusEq(a,__x), __x =aux e
-///  
-///  where a is atomic, e is not atomic
-/// ```
-#[register_rule(("Minion", 4200))]
-fn flatten_minuseq(expr: &Expr, m: &Model) -> ApplicationResult {
-    // TODO: case where a is a literal not a ref?
-
-    // parses arguments a = -e, where a is an atom and e is a non-atomic expression
-    // (when e is an atom, flattening is done, so introduce_minus_eq should be applied instead)
-    fn try_get_args(name: &Expr, negated_expr: &Expr) -> Option<(Name, Expr)> {
-        let Expr::Atomic(_, Atom::Reference(name)) = name else {
-            return None;
-        };
-
-        let Expr::Neg(_, e) = negated_expr else {
-            return None;
-        };
-
-        Some((name.clone(), *e.clone()))
-    }
-
-    let (name, e) = match expr {
-        // parse arguments symmetrically
-        Expr::Eq(_, a, b) => try_get_args(a.borrow(), b.borrow())
-            .or_else(|| try_get_args(b.borrow(), a.borrow()))
-            .ok_or(RuleNotApplicable),
-
-        Expr::AuxDeclaration(_, name, e) => match e.borrow() {
-            Expr::Neg(_, e) => Some((name.clone(), (*e.clone()))),
-            _ => None,
-        }
-        .ok_or(RuleNotApplicable),
-
-        _ => Err(RuleNotApplicable),
-    }?;
-
-    let aux_var_out = to_aux_var(&e, m).ok_or(RuleNotApplicable)?;
-
-    let new_expr = Expr::FlatMinusEq(
-        Metadata::new(),
-        Atom::Reference(name),
-        aux_var_out.as_atom(),
-    );
-
-    Ok(Reduction::new(
-        new_expr,
-        vec![aux_var_out.top_level_expr()],
-        aux_var_out.model().variables,
-    ))
-}
-
 // TODO: normalise equalities such that atoms are always on the LHS.
 // i.e. always have a = sum(x,y,z), not sum(x,y,z) = a