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
22593
fn minion_rs_callback(solutions: HashMap<minion_ast::VarName, minion_ast::Constant>) -> bool {
43
22593
    *(ANY_SOLUTIONS.lock().unwrap()) = true;
44
22593
    let callback = USER_CALLBACK
45
22593
        .get_or_init(|| Mutex::new(Box::new(|x| true)))
46
22593
        .lock()
47
22593
        .unwrap();
48
22593

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

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

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

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

            
72
22593
    continue_search
73
22593
}
74

            
75
impl private::Sealed for Minion {}
76

            
77
impl Minion {
78
850
    pub fn new() -> Minion {
79
850
        Minion {
80
850
            __non_constructable: private::Internal,
81
850
            model: None,
82
850
        }
83
850
    }
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
850
    fn solve(
95
850
        &mut self,
96
850
        callback: SolverCallback,
97
850
        _: private::Internal,
98
850
    ) -> Result<SolveSuccess, SolverError> {
99
850
        // our minion callback is global state, so single threading the adaptor as a whole is
100
850
        // probably a good move...
101
850
        #[allow(clippy::unwrap_used)]
102
850
        let mut minion_lock = MINION_LOCK.lock().unwrap();
103
850

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

            
113
850
        run_minion(
114
850
            self.model.clone().expect("STATE MACHINE ERR"),
115
850
            minion_rs_callback,
116
850
        )
117
850
        .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
850
        })?;
123

            
124
850
        let mut status = Complete(HasSolutions);
125
850
        if *(USER_TERMINATED.lock()).unwrap() {
126
            status = Incomplete(UserTerminated);
127
850
        } else if *(ANY_SOLUTIONS.lock()).unwrap() {
128
850
            status = Complete(NoSolutions);
129
850
        }
130
850
        Ok(SolveSuccess {
131
850
            stats: get_solver_stats(),
132
850
            status,
133
850
        })
134
850
    }
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
850
    fn load_model(&mut self, model: ConjureModel, _: private::Internal) -> Result<(), SolverError> {
145
850
        let mut minion_model = MinionModel::new();
146
850
        parse_vars(&model, &mut minion_model)?;
147
850
        parse_exprs(&model, &mut minion_model)?;
148
850
        self.model = Some(minion_model);
149
850
        Ok(())
150
850
    }
151

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

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

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

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

            
174
2397
fn parse_var(
175
2397
    name: &conjure_ast::Name,
176
2397
    var: &conjure_ast::DecisionVariable,
177
2397
    minion_model: &mut MinionModel,
178
2397
) -> Result<(), SolverError> {
179
2397
    match &var.domain {
180
2074
        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
2397
}
185

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

            
193
2074
    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
2074
    }
200

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

            
206
2074
    let (low, high) = match range {
207
2057
        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
2074
    _try_add_var(
214
2074
        str_name.to_owned(),
215
2074
        minion_ast::VarDomain::Bound(low, high),
216
2074
        minion_model,
217
2074
    )
218
2074
}
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
2397
fn _try_add_var(
233
2397
    name: minion_ast::VarName,
234
2397
    domain: minion_ast::VarDomain,
235
2397
    minion_model: &mut MinionModel,
236
2397
) -> Result<(), SolverError> {
237
2397
    minion_model
238
2397
        .named_variables
239
2397
        .add_var(name.clone(), domain)
240
2397
        .ok_or(ModelInvalid(format!(
241
2397
            "variable {:?} is defined twice",
242
2397
            name
243
2397
        )))
244
2397
}
245

            
246
850
fn parse_exprs(
247
850
    conjure_model: &ConjureModel,
248
850
    minion_model: &mut MinionModel,
249
850
) -> Result<(), SolverError> {
250
5933
    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
799
        use crate::metadata::Metadata;
254
799
        use conjure_ast::Expression as Expr;
255
799
        use conjure_ast::Factor;
256
799
        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
5882
                parse_expr(expr.to_owned(), minion_model)?;
272
            }
273
        }
274
    }
275
799
    Ok(())
276
850
}
277

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

            
286
20927
fn read_expr(expr: conjure_ast::Expression) -> Result<minion_ast::Constraint, SolverError> {
287
20927
    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
306
        conjure_ast::Expression::Neq(_metadata, a, b) => {
302
306
            Ok(minion_ast::Constraint::DisEq(read_var(*a)?, read_var(*b)?))
303
        }
304
272
        conjure_ast::Expression::DivEq(_metadata, a, b, c) => {
305
272
            Ok(minion_ast::Constraint::DivUndefZero(
306
272
                (read_var(a.into())?, read_var(b.into())?),
307
272
                read_var(c.into())?,
308
            ))
309
        }
310
4301
        conjure_ast::Expression::Or(_metadata, exprs) => Ok(minion_ast::Constraint::WatchedOr(
311
4301
            exprs
312
4301
                .iter()
313
15045
                .map(|x| read_expr(x.to_owned()))
314
4301
                .collect::<Result<Vec<minion_ast::Constraint>, SolverError>>()?,
315
        )),
316
        conjure_ast::Expression::And(_metadata, exprs) => Ok(minion_ast::Constraint::WatchedAnd(
317
            exprs
318
                .iter()
319
                .map(|x| read_expr(x.to_owned()))
320
                .collect::<Result<Vec<minion_ast::Constraint>, SolverError>>()?,
321
        )),
322
425
        conjure_ast::Expression::Eq(_metadata, a, b) => {
323
425
            Ok(minion_ast::Constraint::Eq(read_var(*a)?, read_var(*b)?))
324
        }
325

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

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

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

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

            
378
42245
    let str_name = _name_to_string(name);
379
42245
    Ok(str_name)
380
52700
}
381

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

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

            
406
44897
fn _name_to_string(name: conjure_ast::Name) -> String {
407
44897
    match name {
408
43367
        conjure_ast::Name::UserName(x) => x,
409
1530
        conjure_ast::Name::MachineName(x) => format!("__conjure_machine_name_{}", x),
410
    }
411
44897
}
412

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