conjure_core/rules/normalisers/
lt_gt.rs

Help
1//! Normalising rules for Lt and Gt.
2//!
3//! For Minion, these normalise into Leq and Geq respectively.
4
5use conjure_macros::register_rule;
6
7use crate::{
8    ast::{Atom, Expression as Expr, Literal as Lit, SymbolTable},
9    matrix_expr,
10    metadata::Metadata,
11    rule_engine::{ApplicationError::RuleNotApplicable, ApplicationResult, Reduction},
12};
13
14/// Converts Lt to Leq
15///
16/// Minion only for now, but this could be useful for other solvers too.
17///
18/// # Rationale
19///
20/// Minion supports Leq directly in some constraints, such as SumLeq, WeightedSumLeq, ...
21/// This transformation makes Lt work with these constraints too without needing special
22/// cases in the Minion conversion rules.
23#[register_rule(("Minion", 8400))]
24fn lt_to_leq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
25    let Expr::Lt(_, lhs, rhs) = expr.clone() else {
26        return Err(RuleNotApplicable);
27    };
28
29    // add to rhs so that this is in the correct form for ineq ( x <= y + k)
30    Ok(Reduction::pure(Expr::Leq(
31        Metadata::new(),
32        lhs,
33        Box::new(Expr::Sum(
34            Metadata::new(),
35            Box::new(matrix_expr![
36                *rhs,
37                Expr::Atomic(Metadata::new(), Atom::Literal(Lit::Int(-1))),
38            ]),
39        )),
40    )))
41}
42
43/// Converts Gt to Geq
44///
45/// Minion only for now, but this could be useful for other solvers too.
46///
47/// # Rationale
48///
49/// Minion supports Geq directly in some constraints, such as SumGeq, WeightedSumGeq, ...
50/// This transformation makes Gt work with these constraints too without needing special
51/// cases in the Minion conversion rules.
52#[register_rule(("Minion", 8400))]
53fn gt_to_geq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
54    let Expr::Gt(_, lhs, total) = expr.clone() else {
55        return Err(RuleNotApplicable);
56    };
57
58    Ok(Reduction::pure(Expr::Geq(
59        Metadata::new(),
60        Box::new(Expr::Sum(
61            Metadata::new(),
62            Box::new(matrix_expr![
63                *lhs,
64                Expr::Atomic(Metadata::new(), Atom::Literal(Lit::Int(-1))),
65            ]),
66        )),
67        total,
68    )))
69}
conjure_core/rules/normalisers/lt_gt.rs

conjure_core/rules/normalisers/
lt_gt.rs
