1
use std::collections::HashMap;
2
use std::sync::{Mutex, OnceLock};
3

            
4
use regex::Regex;
5

            
6
use minion_ast::Model as MinionModel;
7
use minion_rs::ast as minion_ast;
8
use minion_rs::error::MinionError;
9
use minion_rs::{get_from_table, run_minion};
10

            
11
use crate::ast as conjure_ast;
12
use crate::solver::SolverCallback;
13
use crate::solver::SolverFamily;
14
use crate::solver::SolverMutCallback;
15
use crate::stats::SolverStats;
16
use crate::Model as ConjureModel;
17

            
18
use super::super::model_modifier::NotModifiable;
19
use super::super::private;
20
use super::super::SearchComplete::*;
21
use super::super::SearchIncomplete::*;
22
use super::super::SearchStatus::*;
23
use super::super::SolveSuccess;
24
use super::super::SolverAdaptor;
25
use super::super::SolverError;
26
use super::super::SolverError::*;
27

            
28
/// A [SolverAdaptor] for interacting with Minion.
29
///
30
/// This adaptor uses the `minion_rs` crate to talk to Minion over FFI.
31
pub struct Minion {
32
    __non_constructable: private::Internal,
33
    model: Option<MinionModel>,
34
}
35

            
36
static MINION_LOCK: Mutex<()> = Mutex::new(());
37
static USER_CALLBACK: OnceLock<Mutex<SolverCallback>> = OnceLock::new();
38
static ANY_SOLUTIONS: Mutex<bool> = Mutex::new(false);
39
static USER_TERMINATED: Mutex<bool> = Mutex::new(false);
40

            
41
#[allow(clippy::unwrap_used)]
42
6409
fn minion_rs_callback(solutions: HashMap<minion_ast::VarName, minion_ast::Constant>) -> bool {
43
6409
    *(ANY_SOLUTIONS.lock().unwrap()) = true;
44
6409
    let callback = USER_CALLBACK
45
6409
        .get_or_init(|| Mutex::new(Box::new(|x| true)))
46
6409
        .lock()
47
6409
        .unwrap();
48
6409

            
49
6409
    let mut conjure_solutions: HashMap<conjure_ast::Name, conjure_ast::Literal> = HashMap::new();
50
17272
    for (minion_name, minion_const) in solutions.into_iter() {
51
17272
        let conjure_const = match minion_const {
52
            minion_ast::Constant::Bool(x) => conjure_ast::Literal::Bool(x),
53
17272
            minion_ast::Constant::Integer(x) => conjure_ast::Literal::Int(x),
54
            _ => todo!(),
55
        };
56

            
57
17272
        let machine_name_re = Regex::new(r"__conjure_machine_name_([0-9]+)").unwrap();
58
17272
        let conjure_name = if let Some(caps) = machine_name_re.captures(&minion_name) {
59
1564
            conjure_ast::Name::MachineName(caps[1].parse::<i32>().unwrap())
60
        } else {
61
15708
            conjure_ast::Name::UserName(minion_name)
62
        };
63

            
64
17272
        conjure_solutions.insert(conjure_name, conjure_const);
65
    }
66

            
67
6409
    let continue_search = (**callback)(conjure_solutions);
68
6409
    if !continue_search {
69
        *(USER_TERMINATED.lock().unwrap()) = true;
70
6409
    }
71

            
72
6409
    continue_search
73
6409
}
74

            
75
impl private::Sealed for Minion {}
76

            
77
impl Minion {
78
782
    pub fn new() -> Minion {
79
782
        Minion {
80
782
            __non_constructable: private::Internal,
81
782
            model: None,
82
782
        }
83
782
    }
84
}
85

            
86
impl Default for Minion {
87
    fn default() -> Self {
88
        Minion::new()
89
    }
90
}
91

            
92
impl SolverAdaptor for Minion {
93
    #[allow(clippy::unwrap_used)]
94
782
    fn solve(
95
782
        &mut self,
96
782
        callback: SolverCallback,
97
782
        _: private::Internal,
98
782
    ) -> Result<SolveSuccess, SolverError> {
99
782
        // our minion callback is global state, so single threading the adaptor as a whole is
100
782
        // probably a good move...
101
782
        #[allow(clippy::unwrap_used)]
102
782
        let mut minion_lock = MINION_LOCK.lock().unwrap();
103
782

            
104
782
        #[allow(clippy::unwrap_used)]
105
782
        let mut user_callback = USER_CALLBACK
106
782
            .get_or_init(|| Mutex::new(Box::new(|x| true)))
107
782
            .lock()
108
782
            .unwrap();
109
782
        *user_callback = callback;
110
782
        drop(user_callback); // release mutex. REQUIRED so that run_minion can use the
111
782
                             // user callback and not deadlock.
112
782

            
113
782
        run_minion(
114
782
            self.model.clone().expect("STATE MACHINE ERR"),
115
782
            minion_rs_callback,
116
782
        )
117
782
        .map_err(|err| match err {
118
            MinionError::RuntimeError(x) => Runtime(format!("{:#?}", x)),
119
            MinionError::Other(x) => Runtime(format!("{:#?}", x)),
120
            MinionError::NotImplemented(x) => RuntimeNotImplemented(x),
121
            x => Runtime(format!("unknown minion_rs error: {:#?}", x)),
122
782
        })?;
123

            
124
782
        let mut status = Complete(HasSolutions);
125
782
        if *(USER_TERMINATED.lock()).unwrap() {
126
            status = Incomplete(UserTerminated);
127
782
        } else if *(ANY_SOLUTIONS.lock()).unwrap() {
128
782
            status = Complete(NoSolutions);
129
782
        }
130
782
        Ok(SolveSuccess {
131
782
            stats: get_solver_stats(),
132
782
            status,
133
782
        })
134
782
    }
135

            
136
    fn solve_mut(
137
        &mut self,
138
        callback: SolverMutCallback,
139
        _: private::Internal,
140
    ) -> Result<SolveSuccess, SolverError> {
141
        Err(OpNotImplemented("solve_mut".into()))
142
    }
143

            
144
782
    fn load_model(&mut self, model: ConjureModel, _: private::Internal) -> Result<(), SolverError> {
145
782
        let mut minion_model = MinionModel::new();
146
782
        parse_vars(&model, &mut minion_model)?;
147
782
        parse_exprs(&model, &mut minion_model)?;
148
782
        self.model = Some(minion_model);
149
782
        Ok(())
150
782
    }
151

            
152
782
    fn get_family(&self) -> SolverFamily {
153
782
        SolverFamily::Minion
154
782
    }
155

            
156
782
    fn get_name(&self) -> Option<String> {
157
782
        Some("Minion".to_owned())
158
782
    }
159
}
160

            
161
782
fn parse_vars(
162
782
    conjure_model: &ConjureModel,
163
782
    minion_model: &mut MinionModel,
164
782
) -> Result<(), SolverError> {
165
    // TODO (niklasdewally): remove unused vars?
166
    // TODO (niklasdewally): ensure all vars references are used.
167

            
168
2023
    for (name, variable) in conjure_model.variables.iter() {
169
2023
        parse_var(name, variable, minion_model)?;
170
    }
171
782
    Ok(())
172
782
}
173

            
174
2023
fn parse_var(
175
2023
    name: &conjure_ast::Name,
176
2023
    var: &conjure_ast::DecisionVariable,
177
2023
    minion_model: &mut MinionModel,
178
2023
) -> Result<(), SolverError> {
179
2023
    match &var.domain {
180
1700
        conjure_ast::Domain::IntDomain(ranges) => _parse_intdomain_var(name, ranges, minion_model),
181
323
        conjure_ast::Domain::BoolDomain => _parse_booldomain_var(name, minion_model),
182
        x => Err(ModelFeatureNotSupported(format!("{:?}", x))),
183
    }
184
2023
}
185

            
186
1700
fn _parse_intdomain_var(
187
1700
    name: &conjure_ast::Name,
188
1700
    ranges: &[conjure_ast::Range<i32>],
189
1700
    minion_model: &mut MinionModel,
190
1700
) -> Result<(), SolverError> {
191
1700
    let str_name = _name_to_string(name.to_owned());
192
1700

            
193
1700
    if ranges.len() != 1 {
194
        return Err(ModelFeatureNotImplemented(format!(
195
            "variable {:?} has {:?} ranges. Multiple ranges / SparseBound is not yet supported.",
196
            str_name,
197
            ranges.len()
198
        )));
199
1700
    }
200

            
201
1700
    let range = ranges.first().ok_or(ModelInvalid(format!(
202
1700
        "variable {:?} has no range",
203
1700
        str_name
204
1700
    )))?;
205

            
206
1700
    let (low, high) = match range {
207
1683
        conjure_ast::Range::Bounded(x, y) => Ok((x.to_owned(), y.to_owned())),
208
17
        conjure_ast::Range::Single(x) => Ok((x.to_owned(), x.to_owned())),
209
        #[allow(unreachable_patterns)]
210
        x => Err(ModelFeatureNotSupported(format!("{:?}", x))),
211
    }?;
212

            
213
1700
    _try_add_var(
214
1700
        str_name.to_owned(),
215
1700
        minion_ast::VarDomain::Bound(low, high),
216
1700
        minion_model,
217
1700
    )
218
1700
}
219

            
220
323
fn _parse_booldomain_var(
221
323
    name: &conjure_ast::Name,
222
323
    minion_model: &mut MinionModel,
223
323
) -> Result<(), SolverError> {
224
323
    let str_name = _name_to_string(name.to_owned());
225
323
    _try_add_var(
226
323
        str_name.to_owned(),
227
323
        minion_ast::VarDomain::Bool,
228
323
        minion_model,
229
323
    )
230
323
}
231

            
232
2023
fn _try_add_var(
233
2023
    name: minion_ast::VarName,
234
2023
    domain: minion_ast::VarDomain,
235
2023
    minion_model: &mut MinionModel,
236
2023
) -> Result<(), SolverError> {
237
2023
    minion_model
238
2023
        .named_variables
239
2023
        .add_var(name.clone(), domain)
240
2023
        .ok_or(ModelInvalid(format!(
241
2023
            "variable {:?} is defined twice",
242
2023
            name
243
2023
        )))
244
2023
}
245

            
246
782
fn parse_exprs(
247
782
    conjure_model: &ConjureModel,
248
782
    minion_model: &mut MinionModel,
249
782
) -> Result<(), SolverError> {
250
5627
    for expr in conjure_model.get_constraints_vec().iter() {
251
        // TODO: top level false / trues should not go to the solver to begin with
252
        // ... but changing this at this stage would require rewriting the tester
253
731
        use crate::metadata::Metadata;
254
731
        use conjure_ast::Expression as Expr;
255
731
        use conjure_ast::Factor;
256
731
        use conjure_ast::Literal::*;
257

            
258
51
        match expr {
259
            // top level false
260
            Expr::FactorE(_, Factor::Literal(Bool(false))) => {
261
17
                minion_model.constraints.push(minion_ast::Constraint::False);
262
17
                return Ok(());
263
            }
264
            // top level true
265
            Expr::FactorE(_, Factor::Literal(Bool(true))) => {
266
34
                minion_model.constraints.push(minion_ast::Constraint::True);
267
34
                return Ok(());
268
            }
269

            
270
            _ => {
271
5576
                parse_expr(expr.to_owned(), minion_model)?;
272
            }
273
        }
274
    }
275
731
    Ok(())
276
782
}
277

            
278
5576
fn parse_expr(
279
5576
    expr: conjure_ast::Expression,
280
5576
    minion_model: &mut MinionModel,
281
5576
) -> Result<(), SolverError> {
282
5576
    minion_model.constraints.push(read_expr(expr)?);
283
5576
    Ok(())
284
5576
}
285

            
286
20570
fn read_expr(expr: conjure_ast::Expression) -> Result<minion_ast::Constraint, SolverError> {
287
20570
    match expr {
288
4998
        conjure_ast::Expression::SumLeq(_metadata, lhs, rhs) => Ok(minion_ast::Constraint::SumLeq(
289
4998
            read_vars(lhs)?,
290
4998
            read_var(*rhs)?,
291
        )),
292
4947
        conjure_ast::Expression::SumGeq(_metadata, lhs, rhs) => Ok(minion_ast::Constraint::SumGeq(
293
4947
            read_vars(lhs)?,
294
4947
            read_var(*rhs)?,
295
        )),
296
5423
        conjure_ast::Expression::Ineq(_metadata, a, b, c) => Ok(minion_ast::Constraint::Ineq(
297
5423
            read_var(*a)?,
298
5423
            read_var(*b)?,
299
5423
            minion_ast::Constant::Integer(read_const(*c)?),
300
        )),
301
170
        conjure_ast::Expression::Neq(_metadata, a, b) => {
302
170
            Ok(minion_ast::Constraint::DisEq(read_var(*a)?, read_var(*b)?))
303
        }
304
102
        conjure_ast::Expression::DivEq(_metadata, a, b, c) => Ok(
305
102
            minion_ast::Constraint::DivUndefZero((read_var(*a)?, read_var(*b)?), read_var(*c)?),
306
        ),
307
4250
        conjure_ast::Expression::Or(_metadata, exprs) => Ok(minion_ast::Constraint::WatchedOr(
308
4250
            exprs
309
4250
                .iter()
310
14926
                .map(|x| read_expr(x.to_owned()))
311
4250
                .collect::<Result<Vec<minion_ast::Constraint>, SolverError>>()?,
312
        )),
313
17
        conjure_ast::Expression::And(_metadata, exprs) => Ok(minion_ast::Constraint::WatchedAnd(
314
17
            exprs
315
17
                .iter()
316
34
                .map(|x| read_expr(x.to_owned()))
317
17
                .collect::<Result<Vec<minion_ast::Constraint>, SolverError>>()?,
318
        )),
319
374
        conjure_ast::Expression::Eq(_metadata, a, b) => {
320
374
            Ok(minion_ast::Constraint::Eq(read_var(*a)?, read_var(*b)?))
321
        }
322

            
323
255
        conjure_ast::Expression::WatchedLiteral(_metadata, name, k) => {
324
255
            Ok(minion_ast::Constraint::WLiteral(
325
255
                minion_ast::Var::NameRef(_name_to_string(name)),
326
255
                minion_ast::Constant::Integer(read_const_1(k)?),
327
            ))
328
        }
329
34
        conjure_ast::Expression::Reify(_metadata, e, v) => Ok(minion_ast::Constraint::Reify(
330
34
            Box::new(read_expr(*e)?),
331
34
            read_var(*v)?,
332
        )),
333

            
334
        conjure_ast::Expression::AuxDeclaration(_metadata, name, expr) => {
335
            Ok(minion_ast::Constraint::Eq(
336
                read_var(conjure_ast::Expression::FactorE(
337
                    _metadata,
338
                    conjure_ast::Factor::Reference(name),
339
                ))?,
340
                read_var(*expr)?,
341
            ))
342
        }
343
        x => Err(ModelFeatureNotSupported(format!("{:?}", x))),
344
    }
345
20570
}
346
9945
fn read_vars(exprs: Vec<conjure_ast::Expression>) -> Result<Vec<minion_ast::Var>, SolverError> {
347
9945
    let mut minion_vars: Vec<minion_ast::Var> = vec![];
348
39576
    for expr in exprs {
349
29631
        let minion_var = read_var(expr)?;
350
29631
        minion_vars.push(minion_var);
351
    }
352
9945
    Ok(minion_vars)
353
9945
}
354

            
355
51850
fn read_var(e: conjure_ast::Expression) -> Result<minion_ast::Var, SolverError> {
356
51850
    // a minion var is either a reference or a "var as const"
357
51850
    match _read_ref(e.clone()) {
358
41531
        Ok(name) => Ok(minion_ast::Var::NameRef(name)),
359
10319
        Err(_) => match read_const(e) {
360
10319
            Ok(n) => Ok(minion_ast::Var::ConstantAsVar(n)),
361
            Err(x) => Err(x),
362
        },
363
    }
364
51850
}
365

            
366
51850
fn _read_ref(e: conjure_ast::Expression) -> Result<String, SolverError> {
367
51850
    let name = match e {
368
41531
        conjure_ast::Expression::FactorE(_metadata, conjure_ast::Factor::Reference(n)) => Ok(n),
369
10319
        x => Err(ModelInvalid(format!(
370
10319
            "expected a reference, but got `{0:?}`",
371
10319
            x
372
10319
        ))),
373
10319
    }?;
374

            
375
41531
    let str_name = _name_to_string(name);
376
41531
    Ok(str_name)
377
51850
}
378

            
379
15742
fn read_const(e: conjure_ast::Expression) -> Result<i32, SolverError> {
380
15742
    match e {
381
15742
        conjure_ast::Expression::FactorE(_, conjure_ast::Factor::Literal(x)) => {
382
15742
            Ok(read_const_1(x)?)
383
        }
384
        x => Err(ModelInvalid(format!(
385
            "expected a constant, but got `{0:?}`",
386
            x
387
        ))),
388
    }
389
15742
}
390

            
391
15997
fn read_const_1(k: conjure_ast::Literal) -> Result<i32, SolverError> {
392
15997
    match k {
393
15674
        conjure_ast::Literal::Int(n) => Ok(n),
394
238
        conjure_ast::Literal::Bool(true) => Ok(1),
395
85
        conjure_ast::Literal::Bool(false) => Ok(0),
396
        x => Err(ModelInvalid(format!(
397
            "expected a constant, but got `{0:?}`",
398
            x
399
        ))),
400
    }
401
15997
}
402

            
403
43809
fn _name_to_string(name: conjure_ast::Name) -> String {
404
43809
    match name {
405
42789
        conjure_ast::Name::UserName(x) => x,
406
1020
        conjure_ast::Name::MachineName(x) => format!("__conjure_machine_name_{}", x),
407
    }
408
43809
}
409

            
410
#[allow(clippy::unwrap_used)]
411
782
fn get_solver_stats() -> SolverStats {
412
782
    SolverStats {
413
782
        nodes: get_from_table("Nodes".into()).map(|x| x.parse::<u64>().unwrap()),
414
782
        ..Default::default()
415
782
    }
416
782
}