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 950505baaa..f00cb219bd 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 @@ -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 index 6b531e816e..b7e020e974 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 @@ -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/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input-expected-rule-trace-human.txt index d14e49cf4f..e2b8446903 100644 --- a/conjure_oxide/tests/integration/basic/sum/01-deeply-nested/input-expected-rule-trace-human.txt +++ b/conjure_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/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 2a4f0c4e70..25570a6b90 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 @@ -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/conjure_oxide/tests/integration/basic/weighted-sum/01-simple/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/weighted-sum/01-simple/input-expected-rule-trace-human.txt index beae3759ae..82ff1d8924 100644 --- a/conjure_oxide/tests/integration/basic/weighted-sum/01-simple/input-expected-rule-trace-human.txt +++ b/conjure_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/conjure_oxide/tests/integration/basic/weighted-sum/02-needs-normalising/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/weighted-sum/02-needs-normalising/input-expected-rule-trace-human.txt index 655439d20a..536eb15c30 100644 --- a/conjure_oxide/tests/integration/basic/weighted-sum/02-needs-normalising/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/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/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input-expected-rule-trace-human.txt index 191078fb82..129f2c1ec0 100644 --- a/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input-expected-rule-trace-human.txt +++ b/conjure_oxide/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/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-rewrite.serialised.json index 5773a11a65..2d45eba597 100644 --- a/conjure_oxide/tests/integration/eprime-minion/partial-eval-01-add/input.expected-rewrite.serialised.json +++ b/conjure_oxide/tests/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/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input-expected-rule-trace-human.txt index 191078fb82..129f2c1ec0 100644 --- a/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input-expected-rule-trace-human.txt +++ b/conjure_oxide/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/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-rewrite.serialised.json index 5773a11a65..2d45eba597 100644 --- a/conjure_oxide/tests/integration/eprime-minion/partial-eval-add/input.expected-rewrite.serialised.json +++ b/conjure_oxide/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 index 129b68782d..c88364b6e8 100644 --- 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 index da637a210c..bc5059851f 100644 --- 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) -- diff --git a/conjure_oxide/tests/integration/xyz/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/xyz/input-expected-rule-trace-human.txt index 129b68782d..c88364b6e8 100644 --- a/conjure_oxide/tests/integration/xyz/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/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/crates/conjure_core/src/ast/expressions.rs b/crates/conjure_core/src/ast/expressions.rs index 8045cdb456..c681394a7d 100644 --- a/crates/conjure_core/src/ast/expressions.rs +++ b/crates/conjure_core/src/ast/expressions.rs @@ -101,15 +101,6 @@ pub enum Expression { #[compatible(JsonInput)] Minus(Metadata, Box<Expression>, Box<Expression>), - /* Flattened SumEq. - * - * Note: this is an intermediary step that's used in the process of converting from conjure model to minion. - * This is NOT a valid expression in either Essence or minion. - * - * ToDo: This is a stop gap solution. Eventually it may be better to have multiple constraints instead? (gs248) - */ - SumEq(Metadata, Vec<Expression>, Box<Expression>), - /// Ensures that sum(vec) >= x. /// /// Low-level Minion constraint. @@ -323,7 +314,6 @@ impl Expression { Expression::Leq(_, _, _) => Some(Domain::BoolDomain), Expression::Gt(_, _, _) => Some(Domain::BoolDomain), Expression::Lt(_, _, _) => Some(Domain::BoolDomain), - Expression::SumEq(_, _, _) => Some(Domain::BoolDomain), Expression::FlatSumGeq(_, _, _) => Some(Domain::BoolDomain), Expression::FlatSumLeq(_, _, _) => Some(Domain::BoolDomain), Expression::MinionDivEqUndefZero(_, _, _, _) => Some(Domain::BoolDomain), @@ -413,7 +403,6 @@ impl Expression { Expression::Lt(_, _, _) => Some(ReturnType::Bool), Expression::SafeDiv(_, _, _) => Some(ReturnType::Int), Expression::UnsafeDiv(_, _, _) => Some(ReturnType::Int), - Expression::SumEq(_, _, _) => Some(ReturnType::Bool), Expression::FlatSumGeq(_, _, _) => Some(ReturnType::Bool), Expression::FlatSumLeq(_, _, _) => Some(ReturnType::Bool), Expression::MinionDivEqUndefZero(_, _, _, _) => Some(ReturnType::Bool), @@ -517,14 +506,6 @@ impl Display for Expression { Expression::Lt(_, box1, box2) => { write!(f, "({} < {})", box1.clone(), box2.clone()) } - Expression::SumEq(_, expressions, expr_box) => { - write!( - f, - "SumEq({}, {})", - pretty_vec(expressions), - expr_box.clone() - ) - } Expression::FlatSumGeq(_, box1, box2) => { write!(f, "SumGeq({}, {})", pretty_vec(box1), box2.clone()) } diff --git a/crates/conjure_core/src/rules/constant_eval.rs b/crates/conjure_core/src/rules/constant_eval.rs index def16a5532..b2cfcb53ef 100644 --- a/crates/conjure_core/src/rules/constant_eval.rs +++ b/crates/conjure_core/src/rules/constant_eval.rs @@ -114,9 +114,6 @@ pub fn eval_constant(expr: &Expr) -> Option<Lit> { Some(Lit::Bool(b == result)) } - Expr::SumEq(_, exprs, a) => { - flat_op::<i32, bool>(|e, a| e.iter().sum::<i32>() == a, exprs, a).map(Lit::Bool) - } Expr::MinionModuloEqUndefZero(_, a, b, c) => { // From Savile Row. Same semantics as division. // @@ -226,6 +223,7 @@ where f(a) } +#[allow(dead_code)] fn flat_op<T, A>(f: fn(Vec<T>, T) -> A, a: &[Expr], b: &Expr) -> Option<A> where T: TryFrom<Lit>, diff --git a/crates/conjure_core/src/rules/minion.rs b/crates/conjure_core/src/rules/minion.rs index 475449e9da..e2addc1d0e 100644 --- a/crates/conjure_core/src/rules/minion.rs +++ b/crates/conjure_core/src/rules/minion.rs @@ -18,7 +18,7 @@ use crate::Model; use uniplate::Uniplate; use ApplicationError::RuleNotApplicable; -use super::utils::{expressions_to_atoms, is_atom, is_flat, to_aux_var}; +use super::utils::{expressions_to_atoms, is_flat, to_aux_var}; register_rule_set!("Minion", 100, ("Base"), (SolverFamily::Minion)); @@ -499,81 +499,6 @@ fn introduce_sumleq(expr: &Expr, _: &Model) -> ApplicationResult { /// eq(sum([a, b]), c) => sumeq([a, b], c) /// ``` -#[register_rule(("Minion", 4200))] -fn sum_eq_to_sumeq(expr: &Expr, _: &Model) -> ApplicationResult { - fn try_get_args(sum_expr: &Expr, value: &Expr) -> Option<(Vec<Expr>, Expr)> { - let Expr::Sum(_, xs) = sum_expr else { - return None; - }; - - Some((xs.clone(), value.clone())) - } - - let (xs, value) = match expr { - Expr::Eq(_, a, b) => { - // get arguments symmetrically - try_get_args(a, b) - .or_else(|| try_get_args(b, a)) - .ok_or(RuleNotApplicable) - } - - Expr::AuxDeclaration(_, name, e) => { - let value = Atom::Reference(name.clone()).into(); - let xs = match *e.clone() { - Expr::Sum(_, xs) => Ok(xs), - _ => Err(RuleNotApplicable), - }?; - - Ok((xs, value)) - } - - _ => Err(RuleNotApplicable), - }?; - - if !(xs.iter().all(is_atom)) { - return Err(RuleNotApplicable); - } - - Ok(Reduction::pure(Expr::SumEq( - Metadata::new(), - xs, - Box::new(value), - ))) -} - -/// Converts a `SumEq` to an `And(SumGeq, SumLeq)` -/// -/// This is a workaround for Minion not having support for a flat "equals" operation on sums -/// -/// ```text -/// sumeq([a, b], c) -> watched_and({ -/// sumleq([a, b], c), -/// sumgeq([a, b], c) -/// }) -/// ``` -#[register_rule(("Minion", 4400))] -fn sumeq_to_minion(expr: &Expr, _: &Model) -> ApplicationResult { - let Expr::SumEq(_, exprs, eq_to) = expr.clone() else { - return Err(RuleNotApplicable); - }; - - let Some(atoms) = expressions_to_atoms(&exprs) else { - return Err(RuleNotApplicable); - }; - - let Expr::Atomic(_, eq_to_atom) = *eq_to else { - return Err(RuleNotApplicable); - }; - - Ok(Reduction::pure(Expr::And( - Metadata::new(), - vec![ - Expr::FlatSumLeq(Metadata::new(), atoms.clone(), eq_to_atom.clone()), - Expr::FlatSumGeq(Metadata::new(), atoms, eq_to_atom), - ], - ))) -} - /** * Convert a Lt to an Ineq @@ -785,3 +710,33 @@ fn not_constraint_to_reify(expr: &Expr, _: &Model) -> ApplicationResult { Atom::Literal(Lit::Bool(false)), ))) } + +// FIXME: updatedisplay impl + +//FIXME: refactor symmetry checking for eq into its own function + +/// Decomposes `sum(....) = e` into `sum(...) =< e /\`sum(...) >= e` +/// +/// # Rationale +/// Minion only has `SumLeq` and `SumGeq` constraints. +#[register_rule(("Minion", 4100))] +fn sum_eq_to_inequalities(expr: &Expr, _: &Model) -> ApplicationResult { + // + let (sum, e1): (Box<Expr>, Box<Expr>) = match expr.clone() { + Expr::Eq(_, e1, e2) if matches!(*e1, Expr::Sum(_, _)) => Ok((e1, e2)), + Expr::Eq(_, e1, e2) if matches!(*e2, Expr::Sum(_, _)) => Ok((e2, e1)), + + Expr::AuxDeclaration(_, name, e1) if matches!(*e1, Expr::Sum(_, _)) => { + Ok((e1, Box::new(Expr::Atomic(Metadata::new(), name.into())))) + } + _ => Err(RuleNotApplicable), + }?; + + Ok(Reduction::pure(Expr::And( + Metadata::new(), + vec![ + Expr::Leq(Metadata::new(), sum.clone(), e1.clone()), + Expr::Geq(Metadata::new(), sum.clone(), e1), + ], + ))) +} diff --git a/crates/conjure_core/src/rules/partial_eval.rs b/crates/conjure_core/src/rules/partial_eval.rs index 37954fbbc7..c8575815f4 100644 --- a/crates/conjure_core/src/rules/partial_eval.rs +++ b/crates/conjure_core/src/rules/partial_eval.rs @@ -199,41 +199,6 @@ fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult { Lt(_, _, _) => Err(RuleNotApplicable), SafeDiv(_, _, _) => Err(RuleNotApplicable), UnsafeDiv(_, _, _) => Err(RuleNotApplicable), - SumEq(m, vec, eq) => { - let mut acc = 0; - let mut new_vec: Vec<Expr> = Vec::new(); - let mut n_consts = 0; - for expr in vec { - if let Expr::Atomic(_, Atom::Literal(Int(x))) = expr { - n_consts += 1; - acc += x; - } else { - new_vec.push(expr); - } - } - - if let Expr::Atomic(_, Atom::Literal(Int(x))) = *eq { - if acc != 0 { - // when rhs is a constant, move lhs constants to rhs - return Ok(Reduction::pure(SumEq( - m, - new_vec, - Box::new(Expr::Atomic( - Default::default(), - Atom::Literal(Int(x - acc)), - )), - ))); - } - } else if acc != 0 { - new_vec.push(Expr::Atomic(Default::default(), Atom::Literal(Int(acc)))); - } - - if n_consts <= 1 { - Err(RuleNotApplicable) - } else { - Ok(Reduction::pure(SumEq(m, new_vec, eq))) - } - } AllDiff(m, vec) => { let mut consts: HashSet<i32> = HashSet::new();