conjure_core/solver/adaptors/minion/
parse_model.rs

1//! Parse / `load_model` step of running Minion.
2
3use std::cell::Ref;
4
5use minion_ast::Model as MinionModel;
6use minion_rs::ast as minion_ast;
7use minion_rs::error::MinionError;
8use minion_rs::{get_from_table, run_minion};
9
10use crate::ast as conjure_ast;
11use crate::ast::Declaration;
12use crate::solver::SolverError::*;
13use crate::solver::SolverFamily;
14use crate::solver::SolverMutCallback;
15use crate::solver::{SolverCallback, SolverError};
16use crate::stats::SolverStats;
17use crate::Model as ConjureModel;
18
19/// Converts a conjure-oxide model to a `minion_rs` model.
20pub fn model_to_minion(model: ConjureModel) -> Result<MinionModel, SolverError> {
21    let mut minion_model = MinionModel::new();
22    load_symbol_table(&model, &mut minion_model)?;
23    load_constraints(&model, &mut minion_model)?;
24    Ok(minion_model)
25}
26
27/// Loads the symbol table into `minion_model`.
28fn load_symbol_table(
29    conjure_model: &ConjureModel,
30    minion_model: &mut MinionModel,
31) -> Result<(), SolverError> {
32    for (name, decl) in conjure_model
33        .as_submodel()
34        .symbols()
35        .clone()
36        .into_iter_local()
37    {
38        let Some(var) = decl.as_var() else {
39            continue;
40        }; // ignore lettings, etc.
41
42        load_var(&name, var, minion_model)?;
43    }
44    Ok(())
45}
46
47/// Loads a single variable into `minion_model`
48fn load_var(
49    name: &conjure_ast::Name,
50    var: &conjure_ast::DecisionVariable,
51    minion_model: &mut MinionModel,
52) -> Result<(), SolverError> {
53    match &var.domain {
54        conjure_ast::Domain::IntDomain(ranges) => load_intdomain_var(name, ranges, minion_model),
55        conjure_ast::Domain::BoolDomain => load_booldomain_var(name, minion_model),
56        x => Err(ModelFeatureNotSupported(format!("{:?}", x))),
57    }
58}
59
60/// Loads a variable with domain IntDomain into `minion_model`
61fn load_intdomain_var(
62    name: &conjure_ast::Name,
63    ranges: &[conjure_ast::Range<i32>],
64    minion_model: &mut MinionModel,
65) -> Result<(), SolverError> {
66    let str_name = name_to_string(name.to_owned());
67
68    if ranges.len() != 1 {
69        return Err(ModelFeatureNotImplemented(format!(
70            "variable {:?} has {:?} ranges. Multiple ranges / SparseBound is not yet supported.",
71            str_name,
72            ranges.len()
73        )));
74    }
75
76    let range = ranges.first().ok_or(ModelInvalid(format!(
77        "variable {:?} has no range",
78        str_name
79    )))?;
80
81    let (low, high) = match range {
82        conjure_ast::Range::Bounded(x, y) => Ok((x.to_owned(), y.to_owned())),
83        conjure_ast::Range::Single(x) => Ok((x.to_owned(), x.to_owned())),
84        #[allow(unreachable_patterns)]
85        x => Err(ModelFeatureNotSupported(format!("{:?}", x))),
86    }?;
87
88    _try_add_var(
89        str_name.to_owned(),
90        minion_ast::VarDomain::Bound(low, high),
91        minion_model,
92    )
93}
94
95/// Loads a variable with domain BoolDomain into `minion_model`
96fn load_booldomain_var(
97    name: &conjure_ast::Name,
98    minion_model: &mut MinionModel,
99) -> Result<(), SolverError> {
100    let str_name = name_to_string(name.to_owned());
101    _try_add_var(
102        str_name.to_owned(),
103        minion_ast::VarDomain::Bool,
104        minion_model,
105    )
106}
107
108fn _try_add_var(
109    name: minion_ast::VarName,
110    domain: minion_ast::VarDomain,
111    minion_model: &mut MinionModel,
112) -> Result<(), SolverError> {
113    minion_model
114        .named_variables
115        .add_var(name.clone(), domain)
116        .ok_or(ModelInvalid(format!(
117            "variable {:?} is defined twice",
118            name
119        )))
120}
121
122fn name_to_string(name: conjure_ast::Name) -> String {
123    match name {
124        conjure_ast::Name::UserName(x) => x,
125        conjure_ast::Name::MachineName(x) => format!("__conjure_machine_name_{}", x),
126    }
127}
128
129/// Loads the constraints into `minion_model`.
130fn load_constraints(
131    conjure_model: &ConjureModel,
132    minion_model: &mut MinionModel,
133) -> Result<(), SolverError> {
134    for expr in conjure_model.as_submodel().constraints().iter() {
135        // TODO: top level false / trues should not go to the solver to begin with
136        // ... but changing this at this stage would require rewriting the tester
137        use crate::metadata::Metadata;
138        use conjure_ast::Atom;
139        use conjure_ast::Expression as Expr;
140        use conjure_ast::Literal::*;
141
142        match expr {
143            // top level false
144            Expr::Atomic(_, Atom::Literal(Bool(false))) => {
145                minion_model.constraints.push(minion_ast::Constraint::False);
146            }
147            // top level true
148            Expr::Atomic(_, Atom::Literal(Bool(true))) => {
149                minion_model.constraints.push(minion_ast::Constraint::True);
150            }
151
152            _ => {
153                load_expr(expr.to_owned(), minion_model)?;
154            }
155        }
156    }
157    Ok(())
158}
159
160/// Adds `expr` to `minion_model`
161fn load_expr(
162    expr: conjure_ast::Expression,
163    minion_model: &mut MinionModel,
164) -> Result<(), SolverError> {
165    minion_model.constraints.push(parse_expr(expr)?);
166    Ok(())
167}
168
169/// Parses a Conjure Oxide expression into a `minion_rs` constraint.
170fn parse_expr(expr: conjure_ast::Expression) -> Result<minion_ast::Constraint, SolverError> {
171    match expr {
172        conjure_ast::Expression::Atomic(_metadata, atom) => Ok(minion_ast::Constraint::WLiteral(
173            parse_atom(atom)?,
174            minion_ast::Constant::Integer(1),
175        )),
176        conjure_ast::Expression::FlatSumLeq(_metadata, lhs, rhs) => Ok(
177            minion_ast::Constraint::SumLeq(parse_atoms(lhs)?, parse_atom(rhs)?),
178        ),
179        conjure_ast::Expression::FlatSumGeq(_metadata, lhs, rhs) => Ok(
180            minion_ast::Constraint::SumGeq(parse_atoms(lhs)?, parse_atom(rhs)?),
181        ),
182        conjure_ast::Expression::FlatIneq(_metadata, a, b, c) => Ok(minion_ast::Constraint::Ineq(
183            parse_atom(a)?,
184            parse_atom(b)?,
185            parse_literal(c)?,
186        )),
187        conjure_ast::Expression::Neq(_metadata, a, b) => Ok(minion_ast::Constraint::DisEq(
188            parse_atomic_expr(*a)?,
189            parse_atomic_expr(*b)?,
190        )),
191        conjure_ast::Expression::MinionDivEqUndefZero(_metadata, a, b, c) => Ok(
192            minion_ast::Constraint::DivUndefZero((parse_atom(a)?, parse_atom(b)?), parse_atom(c)?),
193        ),
194        conjure_ast::Expression::MinionModuloEqUndefZero(_metadata, a, b, c) => {
195            Ok(minion_ast::Constraint::ModuloUndefZero(
196                (parse_atom(a)?, parse_atom(b)?),
197                parse_atom(c)?,
198            ))
199        }
200        conjure_ast::Expression::Or(_metadata, exprs) => Ok(minion_ast::Constraint::WatchedOr(
201            exprs
202                .iter()
203                .map(|x| parse_expr(x.to_owned()))
204                .collect::<Result<Vec<minion_ast::Constraint>, SolverError>>()?,
205        )),
206        conjure_ast::Expression::And(_metadata, exprs) => Ok(minion_ast::Constraint::WatchedAnd(
207            exprs
208                .iter()
209                .map(|x| parse_expr(x.to_owned()))
210                .collect::<Result<Vec<minion_ast::Constraint>, SolverError>>()?,
211        )),
212        conjure_ast::Expression::Eq(_metadata, a, b) => Ok(minion_ast::Constraint::Eq(
213            parse_atomic_expr(*a)?,
214            parse_atomic_expr(*b)?,
215        )),
216
217        conjure_ast::Expression::FlatWatchedLiteral(_metadata, name, k) => Ok(
218            minion_ast::Constraint::WLiteral(parse_name(name)?, parse_literal(k)?),
219        ),
220        conjure_ast::Expression::MinionReify(_metadata, e, v) => Ok(minion_ast::Constraint::Reify(
221            Box::new(parse_expr(*e)?),
222            parse_atom(v)?,
223        )),
224
225        conjure_ast::Expression::MinionReifyImply(_metadata, e, v) => Ok(
226            minion_ast::Constraint::ReifyImply(Box::new(parse_expr(*e)?), parse_atom(v)?),
227        ),
228
229        conjure_ast::Expression::AuxDeclaration(_metadata, name, expr) => Ok(
230            minion_ast::Constraint::Eq(parse_name(name)?, parse_atomic_expr(*expr)?),
231        ),
232
233        conjure_ast::Expression::FlatMinusEq(_metadata, a, b) => Ok(
234            minion_ast::Constraint::MinusEq(parse_atom(a)?, parse_atom(b)?),
235        ),
236
237        conjure_ast::Expression::FlatProductEq(_metadata, a, b, c) => Ok(
238            minion_ast::Constraint::Product((parse_atom(a)?, parse_atom(b)?), parse_atom(c)?),
239        ),
240        conjure_ast::Expression::FlatWeightedSumLeq(_metadata, coeffs, vars, total) => {
241            Ok(minion_ast::Constraint::WeightedSumLeq(
242                parse_literals(coeffs)?,
243                parse_atoms(vars)?,
244                parse_atom(total)?,
245            ))
246        }
247        conjure_ast::Expression::FlatWeightedSumGeq(_metadata, coeffs, vars, total) => {
248            Ok(minion_ast::Constraint::WeightedSumGeq(
249                parse_literals(coeffs)?,
250                parse_atoms(vars)?,
251                parse_atom(total)?,
252            ))
253        }
254        conjure_ast::Expression::FlatAbsEq(_metadata, x, y) => {
255            Ok(minion_ast::Constraint::Abs(parse_atom(x)?, parse_atom(y)?))
256        }
257        conjure_ast::Expression::MinionPow(_, x, y, z) => Ok(minion_ast::Constraint::Pow(
258            (parse_atom(x)?, parse_atom(y)?),
259            parse_atom(z)?,
260        )),
261        x => Err(ModelFeatureNotSupported(format!("{:?}", x))),
262    }
263}
264
265fn parse_atomic_expr(expr: conjure_ast::Expression) -> Result<minion_ast::Var, SolverError> {
266    let conjure_ast::Expression::Atomic(_, atom) = expr else {
267        return Err(ModelInvalid(format!(
268            "expected atomic expression, got {:?}",
269            expr
270        )));
271    };
272
273    parse_atom(atom)
274}
275
276fn parse_atoms(exprs: Vec<conjure_ast::Atom>) -> Result<Vec<minion_ast::Var>, SolverError> {
277    let mut minion_vars: Vec<minion_ast::Var> = vec![];
278    for expr in exprs {
279        let minion_var = parse_atom(expr)?;
280        minion_vars.push(minion_var);
281    }
282    Ok(minion_vars)
283}
284
285fn parse_atom(atom: conjure_ast::Atom) -> Result<minion_ast::Var, SolverError> {
286    match atom {
287        conjure_ast::Atom::Literal(l) => {
288            Ok(minion_ast::Var::ConstantAsVar(parse_literal_as_int(l)?))
289        }
290        conjure_ast::Atom::Reference(name) => Ok(parse_name(name))?,
291    }
292}
293
294fn parse_literal_as_int(k: conjure_ast::Literal) -> Result<i32, SolverError> {
295    match k {
296        conjure_ast::Literal::Int(n) => Ok(n),
297        conjure_ast::Literal::Bool(true) => Ok(1),
298        conjure_ast::Literal::Bool(false) => Ok(0),
299        x => Err(ModelInvalid(format!(
300            "expected a literal but got `{0:?}`",
301            x
302        ))),
303    }
304}
305
306fn parse_literals(
307    literals: Vec<conjure_ast::Literal>,
308) -> Result<Vec<minion_ast::Constant>, SolverError> {
309    let mut minion_constants: Vec<minion_ast::Constant> = vec![];
310    for literal in literals {
311        let minion_constant = parse_literal(literal)?;
312        minion_constants.push(minion_constant);
313    }
314    Ok(minion_constants)
315}
316
317fn parse_literal(k: conjure_ast::Literal) -> Result<minion_ast::Constant, SolverError> {
318    Ok(minion_ast::Constant::Integer(parse_literal_as_int(k)?))
319}
320
321fn parse_name(name: conjure_ast::Name) -> Result<minion_ast::Var, SolverError> {
322    Ok(minion_ast::Var::NameRef(name_to_string(name)))
323}
conjure_core/solver/adaptors/minion/parse_model.rs

conjure_core/solver/adaptors/minion/
parse_model.rs
