conjure_core/rules/
base.rs

Help
1use std::rc::Rc;
2
3use conjure_core::ast::{Atom, Expression as Expr, Literal as Lit, SymbolTable};
4use conjure_core::metadata::Metadata;
5use conjure_core::rule_engine::{
6    register_rule, register_rule_set, ApplicationError, ApplicationError::RuleNotApplicable,
7    ApplicationResult, Reduction,
8};
9use uniplate::Uniplate;
10
11use Atom::*;
12use Expr::*;
13use Lit::Bool;
14
15use crate::ast::Declaration;
16use crate::{into_matrix_expr, matrix_expr};
17
18register_rule_set!("Base", ());
19
20/// This rule simplifies expressions where the operator is applied to an empty set of sub-expressions.
21///
22/// For example:
23/// - `or([])` simplifies to `false` since no disjunction exists.
24///
25/// **Applicable examples:**
26/// ```text
27/// or([])  ~> false
28/// X([]) ~> Nothing
29/// ```
30#[register_rule(("Base", 8800))]
31fn remove_empty_expression(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
32    // excluded expressions
33    if matches!(
34        expr,
35        Atomic(_, _)
36            | Root(_, _)
37            | Comprehension(_, _)
38            | FlatIneq(_, _, _, _)
39            | FlatMinusEq(_, _, _)
40            | FlatSumGeq(_, _, _)
41            | FlatSumLeq(_, _, _)
42            | FlatProductEq(_, _, _, _)
43            | FlatWatchedLiteral(_, _, _)
44            | FlatWeightedSumGeq(_, _, _, _)
45            | FlatWeightedSumLeq(_, _, _, _)
46            | MinionDivEqUndefZero(_, _, _, _)
47            | MinionModuloEqUndefZero(_, _, _, _)
48            | MinionWInIntervalSet(_, _, _)
49            | MinionElementOne(_, _, _, _)
50            | MinionPow(_, _, _, _)
51            | MinionReify(_, _, _)
52            | MinionReifyImply(_, _, _)
53            | FlatAbsEq(_, _, _)
54            | Min(_, _)
55            | Max(_, _)
56            | AllDiff(_, _)
57            | FlatAllDiff(_, _)
58            | AbstractLiteral(_, _)
59    ) {
60        return Err(ApplicationError::RuleNotApplicable);
61    }
62
63    if !expr.children().is_empty() {
64        return Err(ApplicationError::RuleNotApplicable);
65    }
66
67    let new_expr = match expr {
68        Or(_, _) => Atomic(Metadata::new(), Literal(Bool(false))),
69        _ => And(Metadata::new(), Box::new(matrix_expr![])),
70    };
71
72    Ok(Reduction::pure(new_expr))
73}
74
75/**
76 * Turn a Min into a new variable and post a top-level constraint to ensure the new variable is the minimum.
77 * ```text
78 * min([a, b]) ~> c ; c <= a & c <= b & (c = a | c = b)
79 * ```
80 */
81#[register_rule(("Base", 6000))]
82fn min_to_var(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
83    let Expr::Min(_, inside_min_expr) = expr else {
84        return Err(RuleNotApplicable);
85    };
86
87    // let matrix expressions / comprehensions be unrolled first before applying this rule.
88    let Some(exprs) = inside_min_expr.as_ref().clone().unwrap_list() else {
89        return Err(RuleNotApplicable);
90    };
91
92    let mut symbols = symbols.clone();
93    let new_name = symbols.gensym();
94
95    let mut new_top = Vec::new(); // the new variable must be less than or equal to all the other variables
96    let mut disjunction = Vec::new(); // the new variable must be equal to one of the variables
97    for e in exprs {
98        new_top.push(Leq(
99            Metadata::new(),
100            Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),
101            Box::new(e.clone()),
102        ));
103        disjunction.push(Eq(
104            Metadata::new(),
105            Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),
106            Box::new(e.clone()),
107        ));
108    }
109    // TODO: deal with explicit index domains
110    new_top.push(Or(
111        Metadata::new(),
112        Box::new(into_matrix_expr![disjunction]),
113    ));
114
115    let domain = expr
116        .domain_of(&symbols)
117        .ok_or(ApplicationError::DomainError)?;
118    symbols.insert(Rc::new(Declaration::new_var(new_name.clone(), domain)));
119
120    Ok(Reduction::new(
121        Atomic(Metadata::new(), Reference(new_name)),
122        new_top,
123        symbols,
124    ))
125}
126
127/**
128 * Turn a Max into a new variable and post a top level constraint to ensure the new variable is the maximum.
129 * ```text
130 * max([a, b]) ~> c ; c >= a & c >= b & (c = a | c = b)
131 * ```
132 */
133#[register_rule(("Base", 6000))]
134fn max_to_var(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
135    let Expr::Max(_, inside_max_expr) = expr else {
136        return Err(RuleNotApplicable);
137    };
138
139    let Some(exprs) = inside_max_expr.as_ref().clone().unwrap_list() else {
140        return Err(RuleNotApplicable);
141    };
142
143    let mut symbols = symbols.clone();
144    let new_name = symbols.gensym();
145
146    let mut new_top = Vec::new(); // the new variable must be more than or equal to all the other variables
147    let mut disjunction = Vec::new(); // the new variable must more than or equal to one of the variables
148    for e in exprs {
149        new_top.push(Geq(
150            Metadata::new(),
151            Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),
152            Box::new(e.clone()),
153        ));
154        disjunction.push(Eq(
155            Metadata::new(),
156            Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),
157            Box::new(e.clone()),
158        ));
159    }
160    // FIXME: deal with explicitly given domains
161    new_top.push(Or(
162        Metadata::new(),
163        Box::new(into_matrix_expr![disjunction]),
164    ));
165
166    let domain = expr
167        .domain_of(&symbols)
168        .ok_or(ApplicationError::DomainError)?;
169    symbols.insert(Rc::new(Declaration::new_var(new_name.clone(), domain)));
170
171    Ok(Reduction::new(
172        Atomic(Metadata::new(), Reference(new_name)),
173        new_top,
174        symbols,
175    ))
176}
conjure_core/rules/base.rs

conjure_core/rules/
base.rs
