1
/************************************************************************/
2
/*        Rules for translating to Minion-supported constraints         */
3
/************************************************************************/
4

            
5
use crate::ast::{
6
    Constant as Const, DecisionVariable, Domain, Expression as Expr, Range, SymbolTable,
7
};
8
use crate::metadata::Metadata;
9
use crate::rule_engine::{
10
    register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction,
11
};
12
use crate::solver::SolverFamily;
13
use crate::Model;
14
use uniplate::biplate::Uniplate;
15

            
16
register_rule_set!("Minion", 100, ("Base"), (SolverFamily::Minion));
17

            
18
fn is_nested_sum(exprs: &Vec<Expr>) -> bool {
19
    for e in exprs {
20
        if let Expr::Sum(_, _) = e {
21
            return true;
22
        }
23
    }
24
    false
25
}
26

            
27
/**
28
 * Helper function to get the vector of expressions from a sum (or error if it's a nested sum - we need to flatten it first)
29
 */
30
fn sum_to_vector(expr: &Expr) -> Result<Vec<Expr>, ApplicationError> {
31
    match expr {
32
        Expr::Sum(_, exprs) => {
33
            if is_nested_sum(exprs) {
34
                Err(ApplicationError::RuleNotApplicable)
35
            } else {
36
                Ok(exprs.clone())
37
            }
38
        }
39
        _ => Err(ApplicationError::RuleNotApplicable),
40
    }
41
}
42

            
43
// /**
44
//  * Convert an Eq to a conjunction of Geq and Leq:
45
//  * ```text
46
//  * a = b => a >= b && a <= b
47
//  * ```
48
//  */
49
// #[register_rule(("Minion", 100))]
50
// fn eq_to_minion(expr: &Expr, _: &Model) -> ApplicationResult {
51
//     match expr {
52
//         Expr::Eq(metadata, a, b) => Ok(Reduction::pure(Expr::And(
53
//             metadata.clone_dirty(),
54
//             vec![
55
//                 Expr::Geq(metadata.clone_dirty(), a.clone(), b.clone()),
56
//                 Expr::Leq(metadata.clone_dirty(), a.clone(), b.clone()),
57
//             ],
58
//         ))),
59
//         _ => Err(ApplicationError::RuleNotApplicable),
60
//     }
61
// }
62

            
63
/**
64
 * Convert a Geq to a SumGeq if the left hand side is a sum:
65
 * ```text
66
 * sum([a, b, c]) >= d => sum_geq([a, b, c], d)
67
 * ```
68
 */
69
#[register_rule(("Minion", 100))]
70
fn flatten_sum_geq(expr: &Expr, _: &Model) -> ApplicationResult {
71
    match expr {
72
        Expr::Geq(metadata, a, b) => {
73
            let exprs = sum_to_vector(a)?;
74
            Ok(Reduction::pure(Expr::SumGeq(
75
                metadata.clone_dirty(),
76
                exprs,
77
                b.clone(),
78
            )))
79
        }
80
        _ => Err(ApplicationError::RuleNotApplicable),
81
    }
82
}
83

            
84
/**
85
 * Convert a Leq to a SumLeq if the left hand side is a sum:
86
 * ```text
87
 * sum([a, b, c]) <= d => sum_leq([a, b, c], d)
88
 * ```
89
 */
90
#[register_rule(("Minion", 100))]
91
fn sum_leq_to_sumleq(expr: &Expr, _: &Model) -> ApplicationResult {
92
    match expr {
93
        Expr::Leq(metadata, a, b) => {
94
            let exprs = sum_to_vector(a)?;
95
            Ok(Reduction::pure(Expr::SumLeq(
96
                metadata.clone_dirty(),
97
                exprs,
98
                b.clone(),
99
            )))
100
        }
101
        _ => Err(ApplicationError::RuleNotApplicable),
102
    }
103
}
104

            
105
/**
106
 * Convert a 'Eq(Sum([...]))' to a SumEq
107
 * ```text
108
 * eq(sum([a, b]), c) => sumeq([a, b], c)
109
 * ```
110
*/
111
#[register_rule(("Minion", 100))]
112
fn sum_eq_to_sumeq(expr: &Expr, _: &Model) -> ApplicationResult {
113
    match expr {
114
        Expr::Eq(metadata, a, b) => {
115
            if let Ok(exprs) = sum_to_vector(a) {
116
                Ok(Reduction::pure(Expr::SumEq(
117
                    metadata.clone_dirty(),
118
                    exprs,
119
                    b.clone(),
120
                )))
121
            } else if let Ok(exprs) = sum_to_vector(b) {
122
                Ok(Reduction::pure(Expr::SumEq(
123
                    metadata.clone_dirty(),
124
                    exprs,
125
                    a.clone(),
126
                )))
127
            } else {
128
                Err(ApplicationError::RuleNotApplicable)
129
            }
130
        }
131
        _ => Err(ApplicationError::RuleNotApplicable),
132
    }
133
}
134

            
135
/**
136
 * Convert a `SumEq` to an `And(SumGeq, SumLeq)`
137
 * This is a workaround for Minion not having support for a flat "equals" operation on sums
138
 * ```text
139
 * sumeq([a, b], c) -> watched_and({
140
 *   sumleq([a, b], c),
141
 *   sumgeq([a, b], c)
142
 * })
143
 * ```
144
 * I. e.
145
 * ```text
146
 * ((a + b) >= c) && ((a + b) <= c)
147
 * a + b = c
148
 * ```
149
 */
150
#[register_rule(("Minion", 100))]
151
fn sumeq_to_minion(expr: &Expr, _: &Model) -> ApplicationResult {
152
    match expr {
153
        Expr::SumEq(metadata, exprs, eq_to) => Ok(Reduction::pure(Expr::And(
154
            Metadata::new(),
155
            vec![
156
                Expr::SumGeq(Metadata::new(), exprs.clone(), Box::from(*eq_to.clone())),
157
                Expr::SumLeq(Metadata::new(), exprs.clone(), Box::from(*eq_to.clone())),
158
            ],
159
        ))),
160
        _ => Err(ApplicationError::RuleNotApplicable),
161
    }
162
}
163

            
164
/**
165
* Convert a Lt to an Ineq:
166

            
167
* ```text
168
* a < b => a - b < -1
169
* ```
170
*/
171
#[register_rule(("Minion", 100))]
172
fn lt_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult {
173
    match expr {
174
        Expr::Lt(metadata, a, b) => Ok(Reduction::pure(Expr::Ineq(
175
            metadata.clone_dirty(),
176
            a.clone(),
177
            b.clone(),
178
            Box::new(Expr::Constant(Metadata::new(), Const::Int(-1))),
179
        ))),
180
        _ => Err(ApplicationError::RuleNotApplicable),
181
    }
182
}
183

            
184
/**
185
* Convert a Gt to an Ineq:
186
*
187
* ```text
188
* a > b => b - a < -1
189
* ```
190
*/
191
#[register_rule(("Minion", 100))]
192
fn gt_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult {
193
    match expr {
194
        Expr::Gt(metadata, a, b) => Ok(Reduction::pure(Expr::Ineq(
195
            metadata.clone_dirty(),
196
            b.clone(),
197
            a.clone(),
198
            Box::new(Expr::Constant(Metadata::new(), Const::Int(-1))),
199
        ))),
200
        _ => Err(ApplicationError::RuleNotApplicable),
201
    }
202
}
203

            
204
/**
205
* Convert a Geq to an Ineq:
206
*
207
* ```text
208
* a >= b => b - a < 0
209
* ```
210
*/
211
#[register_rule(("Minion", 100))]
212
fn geq_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult {
213
    match expr {
214
        Expr::Geq(metadata, a, b) => Ok(Reduction::pure(Expr::Ineq(
215
            metadata.clone_dirty(),
216
            b.clone(),
217
            a.clone(),
218
            Box::new(Expr::Constant(Metadata::new(), Const::Int(0))),
219
        ))),
220
        _ => Err(ApplicationError::RuleNotApplicable),
221
    }
222
}
223

            
224
/**
225
* Convert a Leq to an Ineq:
226
*
227
* ```text
228
* a <= b => a - b < 0
229
* ```
230
*/
231
#[register_rule(("Minion", 100))]
232
fn leq_to_ineq(expr: &Expr, _: &Model) -> ApplicationResult {
233
    match expr {
234
        Expr::Leq(metadata, a, b) => Ok(Reduction::pure(Expr::Ineq(
235
            metadata.clone_dirty(),
236
            a.clone(),
237
            b.clone(),
238
            Box::new(Expr::Constant(Metadata::new(), Const::Int(0))),
239
        ))),
240
        _ => Err(ApplicationError::RuleNotApplicable),
241
    }
242
}
243

            
244
// #[register_rule(("Minion", 99))]
245
// fn eq_to_leq_geq(expr: &Expr, _: &Model) -> ApplicationResult {
246
//     match expr {
247
//         Expr::Eq(metadata, a, b) => {
248
//             return Ok(Reduction::pure(Expr::And(
249
//                 metadata.clone(),
250
//                 vec![
251
//                     Expr::Leq(metadata.clone(), a.clone(), b.clone()),
252
//                     Expr::Geq(metadata.clone(), a.clone(), b.clone()),
253
//                 ],
254
//             )));
255
//         }
256
//         _ => Err(ApplicationError::RuleNotApplicable),
257
//     }
258
// }
259

            
260
/**
261
 * Since Minion doesn't support some constraints with div (e.g. leq, neq), we add an auxiliary variable to represent the division result.
262
*/
263
#[register_rule(("Minion", 101))]
264
fn flatten_safediv(expr: &Expr, mdl: &Model) -> ApplicationResult {
265
    if expr.is_eq() || expr.is_leq() || expr.is_geq() || expr.is_neq() {
266
        let mut sub = expr.children();
267

            
268
        let mut new_vars = SymbolTable::new();
269
        let mut new_top = vec![];
270

            
271
        // replace every safe div child with a reference to a new variable
272
        for c in sub.iter_mut() {
273
            if let Expr::SafeDiv(_, a, b) = c.clone() {
274
                let new_name = mdl.gensym();
275
                let domain = c
276
                    .domain_of(&mdl.variables)
277
                    .ok_or(ApplicationError::DomainError)?;
278
                new_vars.insert(new_name.clone(), DecisionVariable::new(domain));
279

            
280
                new_top.push(Expr::DivEq(
281
                    Metadata::new(),
282
                    a.clone(),
283
                    b.clone(),
284
                    Box::new(Expr::Reference(Metadata::new(), new_name.clone())),
285
                ));
286

            
287
                *c = Expr::Reference(Metadata::new(), new_name.clone());
288
            }
289
        }
290
        if !new_top.is_empty() {
291
            return Ok(Reduction::new(
292
                expr.with_children(sub),
293
                Expr::And(Metadata::new(), new_top),
294
                new_vars,
295
            ));
296
        }
297
    }
298
    Err(ApplicationError::RuleNotApplicable)
299
}
300

            
301
#[register_rule(("Minion", 100))]
302
fn div_eq_to_diveq(expr: &Expr, _: &Model) -> ApplicationResult {
303
    match expr {
304
        Expr::Eq(metadata, a, b) => {
305
            if let Expr::SafeDiv(_, x, y) = a.as_ref() {
306
                if !(b.is_reference() || b.is_constant()) {
307
                    return Err(ApplicationError::RuleNotApplicable);
308
                }
309
                Ok(Reduction::pure(Expr::DivEq(
310
                    metadata.clone_dirty(),
311
                    x.clone(),
312
                    y.clone(),
313
                    b.clone(),
314
                )))
315
            } else if let Expr::SafeDiv(_, x, y) = b.as_ref() {
316
                if !(a.is_reference() || a.is_constant()) {
317
                    return Err(ApplicationError::RuleNotApplicable);
318
                }
319
                Ok(Reduction::pure(Expr::DivEq(
320
                    metadata.clone_dirty(),
321
                    x.clone(),
322
                    y.clone(),
323
                    a.clone(),
324
                )))
325
            } else {
326
                Err(ApplicationError::RuleNotApplicable)
327
            }
328
        }
329
        _ => Err(ApplicationError::RuleNotApplicable),
330
    }
331
}
332

            
333
#[register_rule(("Minion", 100))]
334
fn negated_neq_to_eq(expr: &Expr, _: &Model) -> ApplicationResult {
335
    match expr {
336
        Expr::Not(_, a) => match a.as_ref() {
337
            Expr::Neq(_, b, c) => {
338
                if !b.can_be_undefined() && !c.can_be_undefined() {
339
                    Ok(Reduction::pure(Expr::Eq(
340
                        Metadata::new(),
341
                        b.clone(),
342
                        c.clone(),
343
                    )))
344
                } else {
345
                    Err(ApplicationError::RuleNotApplicable)
346
                }
347
            }
348
            _ => Err(ApplicationError::RuleNotApplicable),
349
        },
350
        _ => Err(ApplicationError::RuleNotApplicable),
351
    }
352
}
353

            
354
#[register_rule(("Minion", 100))]
355
fn negated_eq_to_neq(expr: &Expr, _: &Model) -> ApplicationResult {
356
    match expr {
357
        Expr::Not(_, a) => match a.as_ref() {
358
            Expr::Eq(_, b, c) => {
359
                if !b.can_be_undefined() && !c.can_be_undefined() {
360
                    Ok(Reduction::pure(Expr::Neq(
361
                        Metadata::new(),
362
                        b.clone(),
363
                        c.clone(),
364
                    )))
365
                } else {
366
                    Err(ApplicationError::RuleNotApplicable)
367
                }
368
            }
369
            _ => Err(ApplicationError::RuleNotApplicable),
370
        },
371
        _ => Err(ApplicationError::RuleNotApplicable),
372
    }
373
}