1
use conjure_cp::essence_expr;
2
use conjure_cp::{
3
    ast::Metadata,
4
    ast::{Atom, Expression as Expr, Moo, SymbolTable},
5
    into_matrix_expr,
6
    rule_engine::{
7
        ApplicationError, ApplicationResult, Reduction, register_rule, register_rule_set,
8
    },
9
};
10
use uniplate::Uniplate;
11

            
12
use ApplicationError::RuleNotApplicable;
13

            
14
register_rule_set!("Base", ());
15

            
16
/// This rule simplifies expressions where the operator is applied to an empty set of sub-expressions.
17
///
18
/// For example:
19
/// - `or([])` simplifies to `false` since no disjunction exists.
20
/// - `and([])` simplifies to `true` since no conjunction exists.
21
///
22
/// **Applicable examples:**
23
/// ```text
24
/// or([])  ~> false
25
/// X([]) ~> Nothing
26
/// ```
27
#[register_rule(("Base", 8800))]
28
425467
fn remove_empty_expression(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
29
    // excluded expressions
30
123743
    if matches!(
31
425467
        expr,
32
        Expr::Atomic(_, _)
33
            | Expr::Root(_, _)
34
            | Expr::Comprehension(_, _)
35
            | Expr::FlatIneq(_, _, _, _)
36
            | Expr::FlatMinusEq(_, _, _)
37
            | Expr::FlatSumGeq(_, _, _)
38
            | Expr::FlatSumLeq(_, _, _)
39
            | Expr::FlatProductEq(_, _, _, _)
40
            | Expr::FlatWatchedLiteral(_, _, _)
41
            | Expr::FlatWeightedSumGeq(_, _, _, _)
42
            | Expr::FlatWeightedSumLeq(_, _, _, _)
43
            | Expr::MinionDivEqUndefZero(_, _, _, _)
44
            | Expr::MinionModuloEqUndefZero(_, _, _, _)
45
            | Expr::MinionWInIntervalSet(_, _, _)
46
            | Expr::MinionWInSet(_, _, _)
47
            | Expr::MinionElementOne(_, _, _, _)
48
            | Expr::MinionPow(_, _, _, _)
49
            | Expr::MinionReify(_, _, _)
50
            | Expr::MinionReifyImply(_, _, _)
51
            | Expr::FlatAbsEq(_, _, _)
52
            | Expr::Min(_, _)
53
            | Expr::Max(_, _)
54
            | Expr::AllDiff(_, _)
55
            | Expr::FlatAllDiff(_, _)
56
            | Expr::AbstractLiteral(_, _)
57
    ) {
58
301724
        return Err(ApplicationError::RuleNotApplicable);
59
123743
    }
60

            
61
123743
    if !expr.children().is_empty() {
62
123725
        return Err(ApplicationError::RuleNotApplicable);
63
18
    }
64

            
65
18
    let new_expr = match expr {
66
        Expr::Or(_, _) => essence_expr!(false),
67
        Expr::And(_, _) => essence_expr!(true),
68
        _ => {
69
18
            return Err(ApplicationError::RuleNotApplicable);
70
        } // _ => And(Metadata::new(), Box::new(matrix_expr![])),
71
    };
72

            
73
    Ok(Reduction::pure(new_expr))
74
425467
}
75

            
76
/**
77
 * Turn a Min into a new variable and post a top-level constraint to ensure the new variable is the minimum.
78
 * ```text
79
 * min([a, b]) ~> c ; c <= a & c <= b & (c = a | c = b)
80
 * ```
81
 */
82
#[register_rule(("Base", 6000))]
83
275377
fn min_to_var(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
84
275377
    let Expr::Min(_, inside_min_expr) = expr else {
85
275137
        return Err(RuleNotApplicable);
86
    };
87

            
88
240
    let Some(exprs) = inside_min_expr.as_ref().clone().unwrap_list() else {
89
177
        return Err(RuleNotApplicable);
90
    };
91

            
92
63
    let domain = expr.domain_of().ok_or(ApplicationError::DomainError)?;
93
63
    let mut symbols = symbols.clone();
94

            
95
63
    let atom_inner = Atom::new_ref(symbols.gensym(&domain));
96
63
    let atom_expr = Expr::Atomic(Metadata::new(), atom_inner);
97

            
98
63
    let mut new_top = Vec::new();
99
63
    let mut disjunction = Vec::new();
100
135
    for e in exprs {
101
        // Use the Expr::Atomic version in constraints
102
135
        new_top.push(essence_expr!(&atom_expr <= &e));
103
135
        disjunction.push(essence_expr!(&atom_expr = &e));
104
135
    }
105
    // TODO: deal with explicit index domains
106
63
    new_top.push(Expr::Or(
107
63
        Metadata::new(),
108
63
        Moo::new(into_matrix_expr![disjunction]),
109
63
    ));
110

            
111
63
    Ok(Reduction::new(
112
        // Return the Expr::Atomic
113
63
        essence_expr!(&atom_expr),
114
63
        new_top,
115
63
        symbols.clone(),
116
63
    ))
117
275377
}
118

            
119
/**
120
 * Turn a Max into a new variable and post a top level constraint to ensure the new variable is the maximum.
121
 * ```text
122
 * max([a, b]) ~> c ; c >= a & c >= b & (c = a | c = b)
123
 * ```
124
 */
125
#[register_rule(("Base", 6000))]
126
275377
fn max_to_var(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
127
275377
    let Expr::Max(_, inside_max_expr) = expr else {
128
275182
        return Err(RuleNotApplicable);
129
    };
130

            
131
195
    let Some(exprs) = inside_max_expr.as_ref().clone().unwrap_list() else {
132
138
        return Err(RuleNotApplicable);
133
    };
134

            
135
57
    let domain = expr.domain_of().ok_or(ApplicationError::DomainError)?;
136
57
    let mut symbols: SymbolTable = symbols.clone();
137

            
138
57
    let atom_inner = Atom::new_ref(symbols.gensym(&domain));
139
57
    let atom_expr = Expr::Atomic(Metadata::new(), atom_inner);
140

            
141
57
    let mut new_top = Vec::new(); // the new variable must be more than or equal to all the other variables
142
57
    let mut disjunction = Vec::new(); // the new variable must more than or equal to one of the variables
143
117
    for e in exprs {
144
117
        new_top.push(essence_expr!(&atom_expr >= &e));
145
117
        disjunction.push(essence_expr!(&atom_expr = &e));
146
117
    }
147
    // FIXME: deal with explicitly given domains
148
57
    new_top.push(Expr::Or(
149
57
        Metadata::new(),
150
57
        Moo::new(into_matrix_expr![disjunction]),
151
57
    ));
152

            
153
57
    Ok(Reduction::new(essence_expr!(&atom_expr), new_top, symbols))
154
275377
}