conjure_core/solver/adaptors/minion/
parse_model.rs

Help
1//! Parse / `load_model` step of running Minion.
2
3use std::cell::Ref;
4
5use itertools::Itertools as _;
6use minion_ast::Model as MinionModel;
7use minion_rs::ast as minion_ast;
8use minion_rs::error::MinionError;
9use minion_rs::{get_from_table, run_minion};
10
11use crate::ast as conjure_ast;
12use crate::ast::Declaration;
13use crate::solver::SolverError::*;
14use crate::solver::SolverFamily;
15use crate::solver::SolverMutCallback;
16use crate::solver::{SolverCallback, SolverError};
17use crate::stats::SolverStats;
18use crate::Model as ConjureModel;
19
20/// Converts a conjure-oxide model to a `minion_rs` model.
21pub fn model_to_minion(model: ConjureModel) -> Result<MinionModel, SolverError> {
22    let mut minion_model = MinionModel::new();
23    load_symbol_table(&model, &mut minion_model)?;
24    load_constraints(&model, &mut minion_model)?;
25    Ok(minion_model)
26}
27
28/// Loads the symbol table into `minion_model`.
29fn load_symbol_table(
30    conjure_model: &ConjureModel,
31    minion_model: &mut MinionModel,
32) -> Result<(), SolverError> {
33    if let Some(ref vars) = conjure_model.search_order {
34        // add search vars in order first
35        for name in vars {
36            let decl = conjure_model
37                .as_submodel()
38                .symbols()
39                .lookup(name)
40                .expect("search var should exist");
41            let var = decl.as_var().expect("search var should be a var");
42
43            load_var(name, var, true, minion_model)?;
44        }
45
46        // then add the rest as non-search vars
47        for (name, decl) in conjure_model
48            .as_submodel()
49            .symbols()
50            .clone()
51            .into_iter_local()
52        {
53            // search var - already added
54            if vars.contains(&name) {
55                continue;
56            };
57
58            let Some(var) = decl.as_var() else {
59                continue;
60            }; // ignore lettings, etc.
61               //
62
63            // this variable has representations, so ignore it
64            if !conjure_model
65                .as_submodel()
66                .symbols()
67                .representations_for(&name)
68                .is_none_or(|x| x.is_empty())
69            {
70                continue;
71            };
72
73            load_var(&name, var, false, minion_model)?;
74        }
75    } else {
76        for (name, decl) in conjure_model
77            .as_submodel()
78            .symbols()
79            .clone()
80            .into_iter_local()
81        {
82            let Some(var) = decl.as_var() else {
83                continue;
84            }; // ignore lettings, etc.
85               //
86
87            // this variable has representations, so ignore it
88            if !conjure_model
89                .as_submodel()
90                .symbols()
91                .representations_for(&name)
92                .is_none_or(|x| x.is_empty())
93            {
94                continue;
95            };
96
97            let is_search_var = !matches!(name, conjure_ast::Name::MachineName(_));
98
99            load_var(&name, var, is_search_var, minion_model)?;
100        }
101    }
102    Ok(())
103}
104
105/// Loads a single variable into `minion_model`
106fn load_var(
107    name: &conjure_ast::Name,
108    var: &conjure_ast::DecisionVariable,
109    search_var: bool,
110    minion_model: &mut MinionModel,
111) -> Result<(), SolverError> {
112    match &var.domain {
113        conjure_ast::Domain::IntDomain(ranges) => {
114            load_intdomain_var(name, ranges, search_var, minion_model)
115        }
116        conjure_ast::Domain::BoolDomain => load_booldomain_var(name, search_var, minion_model),
117        x => Err(ModelFeatureNotSupported(format!("{:?}", x))),
118    }
119}
120
121/// Loads a variable with domain IntDomain into `minion_model`
122fn load_intdomain_var(
123    name: &conjure_ast::Name,
124    ranges: &[conjure_ast::Range<i32>],
125    search_var: bool,
126    minion_model: &mut MinionModel,
127) -> Result<(), SolverError> {
128    let str_name = name_to_string(name.to_owned());
129
130    if ranges.len() != 1 {
131        return Err(ModelFeatureNotImplemented(format!(
132            "variable {:?} has {:?} ranges. Multiple ranges / SparseBound is not yet supported.",
133            str_name,
134            ranges.len()
135        )));
136    }
137
138    let range = ranges.first().ok_or(ModelInvalid(format!(
139        "variable {:?} has no range",
140        str_name
141    )))?;
142
143    let (low, high) = match range {
144        conjure_ast::Range::Bounded(x, y) => Ok((x.to_owned(), y.to_owned())),
145        conjure_ast::Range::Single(x) => Ok((x.to_owned(), x.to_owned())),
146        #[allow(unreachable_patterns)]
147        x => Err(ModelFeatureNotSupported(format!("{:?}", x))),
148    }?;
149
150    let domain = minion_ast::VarDomain::Bound(low, high);
151    let str_name = str_name.to_owned();
152
153    if search_var {
154        _try_add_var(str_name, domain, minion_model)
155    } else {
156        _try_add_aux_var(str_name, domain, minion_model)
157    }
158}
159
160/// Loads a variable with domain BoolDomain into `minion_model`
161fn load_booldomain_var(
162    name: &conjure_ast::Name,
163    search_var: bool,
164    minion_model: &mut MinionModel,
165) -> Result<(), SolverError> {
166    let str_name = name_to_string(name.to_owned());
167    let domain = minion_ast::VarDomain::Bool;
168    if search_var {
169        _try_add_var(str_name, domain, minion_model)
170    } else {
171        _try_add_aux_var(str_name, domain, minion_model)
172    }
173}
174
175fn _try_add_var(
176    name: minion_ast::VarName,
177    domain: minion_ast::VarDomain,
178    minion_model: &mut MinionModel,
179) -> Result<(), SolverError> {
180    minion_model
181        .named_variables
182        .add_var(name.clone(), domain)
183        .ok_or(ModelInvalid(format!(
184            "variable {:?} is defined twice",
185            name
186        )))
187}
188
189fn _try_add_aux_var(
190    name: minion_ast::VarName,
191    domain: minion_ast::VarDomain,
192    minion_model: &mut MinionModel,
193) -> Result<(), SolverError> {
194    minion_model
195        .named_variables
196        .add_aux_var(name.clone(), domain)
197        .ok_or(ModelInvalid(format!(
198            "variable {:?} is defined twice",
199            name
200        )))
201}
202
203fn name_to_string(name: conjure_ast::Name) -> String {
204    match name {
205        // print machine names in a custom, easier to regex, way.
206        conjure_ast::Name::MachineName(x) => format!("__conjure_machine_name_{}", x),
207        conjure_ast::Name::RepresentedName(name, rule, suffix) => {
208            let name = name_to_string(*name);
209            format!("__conjure_represented_name##{name}##{rule}___{suffix}")
210        }
211        x => format!("{x}"),
212    }
213}
214
215/// Loads the constraints into `minion_model`.
216fn load_constraints(
217    conjure_model: &ConjureModel,
218    minion_model: &mut MinionModel,
219) -> Result<(), SolverError> {
220    for expr in conjure_model.as_submodel().constraints().iter() {
221        // TODO: top level false / trues should not go to the solver to begin with
222        // ... but changing this at this stage would require rewriting the tester
223        use crate::metadata::Metadata;
224        use conjure_ast::Atom;
225        use conjure_ast::Expression as Expr;
226        use conjure_ast::Literal::*;
227
228        match expr {
229            // top level false
230            Expr::Atomic(_, Atom::Literal(Bool(false))) => {
231                minion_model.constraints.push(minion_ast::Constraint::False);
232            }
233            // top level true
234            Expr::Atomic(_, Atom::Literal(Bool(true))) => {
235                minion_model.constraints.push(minion_ast::Constraint::True);
236            }
237
238            _ => {
239                load_expr(expr.to_owned(), minion_model)?;
240            }
241        }
242    }
243    Ok(())
244}
245
246/// Adds `expr` to `minion_model`
247fn load_expr(
248    expr: conjure_ast::Expression,
249    minion_model: &mut MinionModel,
250) -> Result<(), SolverError> {
251    minion_model.constraints.push(parse_expr(expr)?);
252    Ok(())
253}
254
255/// Parses a Conjure Oxide expression into a `minion_rs` constraint.
256fn parse_expr(expr: conjure_ast::Expression) -> Result<minion_ast::Constraint, SolverError> {
257    match expr {
258        conjure_ast::Expression::Atomic(_metadata, atom) => Ok(minion_ast::Constraint::WLiteral(
259            parse_atom(atom)?,
260            minion_ast::Constant::Integer(1),
261        )),
262        conjure_ast::Expression::FlatAllDiff(_metadata, atoms) => {
263            Ok(minion_ast::Constraint::AllDiff(parse_atoms(atoms)?))
264        }
265        conjure_ast::Expression::FlatSumLeq(_metadata, lhs, rhs) => Ok(
266            minion_ast::Constraint::SumLeq(parse_atoms(lhs)?, parse_atom(rhs)?),
267        ),
268        conjure_ast::Expression::FlatSumGeq(_metadata, lhs, rhs) => Ok(
269            minion_ast::Constraint::SumGeq(parse_atoms(lhs)?, parse_atom(rhs)?),
270        ),
271        conjure_ast::Expression::FlatIneq(_metadata, a, b, c) => Ok(minion_ast::Constraint::Ineq(
272            parse_atom(a)?,
273            parse_atom(b)?,
274            parse_literal(c)?,
275        )),
276        conjure_ast::Expression::Neq(_metadata, a, b) => Ok(minion_ast::Constraint::DisEq(
277            parse_atomic_expr(*a)?,
278            parse_atomic_expr(*b)?,
279        )),
280        conjure_ast::Expression::MinionDivEqUndefZero(_metadata, a, b, c) => Ok(
281            minion_ast::Constraint::DivUndefZero((parse_atom(a)?, parse_atom(b)?), parse_atom(c)?),
282        ),
283        conjure_ast::Expression::MinionModuloEqUndefZero(_metadata, a, b, c) => {
284            Ok(minion_ast::Constraint::ModuloUndefZero(
285                (parse_atom(a)?, parse_atom(b)?),
286                parse_atom(c)?,
287            ))
288        }
289        conjure_ast::Expression::MinionWInIntervalSet(_metadata, a, xs) => {
290            Ok(minion_ast::Constraint::WInIntervalSet(
291                parse_atom(a)?,
292                xs.into_iter()
293                    .map(minion_ast::Constant::Integer)
294                    .collect_vec(),
295            ))
296        }
297
298        conjure_ast::Expression::MinionElementOne(_, vec, i, e) => Ok(
299            minion_ast::Constraint::ElementOne(parse_atoms(vec)?, parse_atom(i)?, parse_atom(e)?),
300        ),
301
302        conjure_ast::Expression::Or(_metadata, e) => Ok(minion_ast::Constraint::WatchedOr(
303            e.unwrap_matrix_unchecked()
304                .ok_or_else(|| {
305                    SolverError::ModelFeatureNotSupported(
306                        "The inside of an or expression is not a matrix.".to_string(),
307                    )
308                })?
309                .0
310                .iter()
311                .map(|x| parse_expr(x.to_owned()))
312                .collect::<Result<Vec<minion_ast::Constraint>, SolverError>>()?,
313        )),
314        conjure_ast::Expression::And(_metadata, e) => Ok(minion_ast::Constraint::WatchedAnd(
315            e.unwrap_matrix_unchecked()
316                .ok_or_else(|| {
317                    SolverError::ModelFeatureNotSupported(
318                        "The inside of an and expression is not a matrix.".to_string(),
319                    )
320                })?
321                .0
322                .iter()
323                .map(|x| parse_expr(x.to_owned()))
324                .collect::<Result<Vec<minion_ast::Constraint>, SolverError>>()?,
325        )),
326        conjure_ast::Expression::Eq(_metadata, a, b) => Ok(minion_ast::Constraint::Eq(
327            parse_atomic_expr(*a)?,
328            parse_atomic_expr(*b)?,
329        )),
330
331        conjure_ast::Expression::FlatWatchedLiteral(_metadata, name, k) => Ok(
332            minion_ast::Constraint::WLiteral(parse_name(name)?, parse_literal(k)?),
333        ),
334        conjure_ast::Expression::MinionReify(_metadata, e, v) => Ok(minion_ast::Constraint::Reify(
335            Box::new(parse_expr(*e)?),
336            parse_atom(v)?,
337        )),
338
339        conjure_ast::Expression::MinionReifyImply(_metadata, e, v) => Ok(
340            minion_ast::Constraint::ReifyImply(Box::new(parse_expr(*e)?), parse_atom(v)?),
341        ),
342
343        conjure_ast::Expression::AuxDeclaration(_metadata, name, expr) => Ok(
344            minion_ast::Constraint::Eq(parse_name(name)?, parse_atomic_expr(*expr)?),
345        ),
346
347        conjure_ast::Expression::FlatMinusEq(_metadata, a, b) => Ok(
348            minion_ast::Constraint::MinusEq(parse_atom(a)?, parse_atom(b)?),
349        ),
350
351        conjure_ast::Expression::FlatProductEq(_metadata, a, b, c) => Ok(
352            minion_ast::Constraint::Product((parse_atom(a)?, parse_atom(b)?), parse_atom(c)?),
353        ),
354        conjure_ast::Expression::FlatWeightedSumLeq(_metadata, coeffs, vars, total) => {
355            Ok(minion_ast::Constraint::WeightedSumLeq(
356                parse_literals(coeffs)?,
357                parse_atoms(vars)?,
358                parse_atom(total)?,
359            ))
360        }
361        conjure_ast::Expression::FlatWeightedSumGeq(_metadata, coeffs, vars, total) => {
362            Ok(minion_ast::Constraint::WeightedSumGeq(
363                parse_literals(coeffs)?,
364                parse_atoms(vars)?,
365                parse_atom(total)?,
366            ))
367        }
368        conjure_ast::Expression::FlatAbsEq(_metadata, x, y) => {
369            Ok(minion_ast::Constraint::Abs(parse_atom(x)?, parse_atom(y)?))
370        }
371        conjure_ast::Expression::MinionPow(_, x, y, z) => Ok(minion_ast::Constraint::Pow(
372            (parse_atom(x)?, parse_atom(y)?),
373            parse_atom(z)?,
374        )),
375        x => Err(ModelFeatureNotSupported(format!("{:?}", x))),
376    }
377}
378
379fn parse_atomic_expr(expr: conjure_ast::Expression) -> Result<minion_ast::Var, SolverError> {
380    let conjure_ast::Expression::Atomic(_, atom) = expr else {
381        return Err(ModelInvalid(format!(
382            "expected atomic expression, got {:?}",
383            expr
384        )));
385    };
386
387    parse_atom(atom)
388}
389
390fn parse_atoms(exprs: Vec<conjure_ast::Atom>) -> Result<Vec<minion_ast::Var>, SolverError> {
391    let mut minion_vars: Vec<minion_ast::Var> = vec![];
392    for expr in exprs {
393        let minion_var = parse_atom(expr)?;
394        minion_vars.push(minion_var);
395    }
396    Ok(minion_vars)
397}
398
399fn parse_atom(atom: conjure_ast::Atom) -> Result<minion_ast::Var, SolverError> {
400    match atom {
401        conjure_ast::Atom::Literal(l) => {
402            Ok(minion_ast::Var::ConstantAsVar(parse_literal_as_int(l)?))
403        }
404        conjure_ast::Atom::Reference(name) => Ok(parse_name(name))?,
405
406        x => Err(ModelFeatureNotSupported(format!(
407            "expected a literal or a reference but got `{0}`",
408            x
409        ))),
410    }
411}
412
413fn parse_literal_as_int(k: conjure_ast::Literal) -> Result<i32, SolverError> {
414    match k {
415        conjure_ast::Literal::Int(n) => Ok(n),
416        conjure_ast::Literal::Bool(true) => Ok(1),
417        conjure_ast::Literal::Bool(false) => Ok(0),
418        x => Err(ModelInvalid(format!(
419            "expected a literal but got `{0:?}`",
420            x
421        ))),
422    }
423}
424
425fn parse_literals(
426    literals: Vec<conjure_ast::Literal>,
427) -> Result<Vec<minion_ast::Constant>, SolverError> {
428    let mut minion_constants: Vec<minion_ast::Constant> = vec![];
429    for literal in literals {
430        let minion_constant = parse_literal(literal)?;
431        minion_constants.push(minion_constant);
432    }
433    Ok(minion_constants)
434}
435
436fn parse_literal(k: conjure_ast::Literal) -> Result<minion_ast::Constant, SolverError> {
437    Ok(minion_ast::Constant::Integer(parse_literal_as_int(k)?))
438}
439
440fn parse_name(name: conjure_ast::Name) -> Result<minion_ast::Var, SolverError> {
441    Ok(minion_ast::Var::NameRef(name_to_string(name)))
442}
conjure_core/solver/adaptors/minion/parse_model.rs

conjure_core/solver/adaptors/minion/
parse_model.rs
