conjure_core/rules/normalisers/
lt_gt.rs

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

conjure_core/rules/normalisers/
lt_gt.rs
