fn inline_constant_matrix_subject_for_minion(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
/// For example, `m[i, 2]` becomes `[m[1,2], ..., m[n,2]][i]` in one rewrite, without cloning `m`
/// Introduces `FlatWeightedSumLeq`, `FlatWeightedSumGeq`, `FlatSumLeq`, FlatSumGeq` constraints.
/// If the input is a weighted sum, the weighted sum constraints are used, otherwise the standard
/// Cases 6 and 7 could potentially be a normalising rule `-e ~> -1*e`. However, I think that we
fn introduce_weighted_sumleq_sumgeq(expr: &Expr, symtab: &SymbolTable) -> ApplicationResult {
/// If the term is in the form <coefficient> * <non flat expression>, the expression is flattened
/// + Returns [`ApplicationError::RuleNotApplicable`] if the term is a product containing a matrix
/// + Returns [`ApplicationError::RuleNotApplicable`] if the expression cannot be placed into an
/// (`minus_to_sum`, flatten, `introduce_abseq`, `introduce_mineq`, `matrix_to_list`) and, worse,
/// duplicates work on the two copies of `|e|`. This rule runs above `minus_to_sum` (8400) so the
/// Channel `e` into an atom for the Lee abs argument, preferring a flat weighted sum for `a - b`.
/// Lowers a bare `min([a, b, ...])` to an auxiliary bound by Minion's native `min` constraint.
// `SafePow` leaves its value unconstrained where `a ** b` is undefined (negative exponents and
// `0 ** 0`); definedness is enforced separately. Minion's `pow` instead fails on most negative
fn unwrap_flatten_in_global_cardinality(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
fn alldifferent_except_to_gccweak(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
fn alldifferent_variable_except(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
if eval_constant(except).is_some() || !except.domain_of().is_some_and(|domain| domain.is_int())
/// Native element requires a valid index; materialise identity entries across the finite bounds.
fn introduce_index_of_from_aux_decl(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
/// (a matrix of plain int/bool literals is left to the native `element`/`table` lowering, which
/// Minion-specific "list of atoms" primitive, since a compound element has no single atom to put
/// in such a list. `value`'s own equality against a compound literal is resolved by the ordinary
/// tuple-literal-equality machinery once this reaches the general rule engine again (this rule
/// `types::tuple::horizontal::tuple_literal_eq_literal` still apply to them on the next pass).
fn pad_represented_index_of_list(atom_list: Vec<Atom>, result: &Reference) -> Option<Vec<Atom>> {
fn indexed_index_of_literal_parts(matrix_expr: &Expr) -> Option<(Vec<i32>, Moo<GroundDomain>)> {
fn index_of_value_may_be_outside_matrix(value_expr: &Expr, search_values: &[i32]) -> bool {
fn index_of_table_rows(value_expr: &Expr, search_values: &[i32]) -> Result<Expr, ApplicationError> {
// matrix map to themselves as indices. Without this, out-of-matrix lookups become unconstrained
fn introduce_reifyimply_ineq_from_imply(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
fn resolve_safeindex_index_of_aux(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
fn drop_invalid_constant_index_of_safeindex_aux(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
fn introduce_wininterval_set_from_indomain(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
fn introduce_element_from_index(expr: &Expr, symtab: &SymbolTable) -> ApplicationResult {
// Minion's `element` is 1-based. A list already is, so it needs no shift; any other contiguous
/// `None` when the index domain is not a contiguous integer range covering exactly the elements,
/// because implications can be expressed as a `reifyimply` constraint, which takes a constraint as
#[register_rule("Minion", 4200, [SafeDiv, Neq, SafeMod, SafePow, Leq, Geq, Abs, Neg, Not, SafeIndex, InDomain, ToInt])]
// We only want to flatten products containing matrix literals that are lists but not child terms, e.g.
#[register_rule("Minion", 1000, [* / AbstractLiteral, * / Atomic])] // lower than matrix_to_list
/// The regular bool_lit case is dealt with directly by the Minion solver interface (as it is a
/// This rule has lower priority than boolean_literal_to_wliteral so that we can assume that the
Expr::AuxDeclaration(_, reference, e) => Ok((Atom::from(reference.clone()), e.clone())),
.any(|c| matches!(c, Expr::AuxDeclaration(_, _, e) if matches!(e.as_ref(), Expr::ToInt(_, _)))),