From 0063a1c8ab64d7c90cd54a317d54664a7dd047bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=96zg=C3=BCr=20Akg=C3=BCn?= 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 = 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 = 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?= 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 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