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

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

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

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

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

            
72
5655
    continue_search
73
5655
}
74

            
75
impl private::Sealed for Minion {}
76

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

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

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

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

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

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

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

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

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

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

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

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

            
206
1500
    let (low, high) = match range {
207
1485
        conjure_ast::Range::Bounded(x, y) => Ok((x.to_owned(), y.to_owned())),
208
15
        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
1500
    _try_add_var(
214
1500
        str_name.to_owned(),
215
1500
        minion_ast::VarDomain::Bound(low, high),
216
1500
        minion_model,
217
1500
    )
218
1500
}
219

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

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

            
246
690
fn parse_exprs(
247
690
    conjure_model: &ConjureModel,
248
690
    minion_model: &mut MinionModel,
249
690
) -> Result<(), SolverError> {
250
4965
    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
645
        use crate::metadata::Metadata;
254
645
        use conjure_ast::Expression as Expr;
255
645
        use conjure_ast::Factor;
256
645
        use conjure_ast::Literal::*;
257

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

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

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

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

            
323
225
        conjure_ast::Expression::WatchedLiteral(_metadata, name, k) => {
324
225
            Ok(minion_ast::Constraint::WLiteral(
325
225
                minion_ast::Var::NameRef(_name_to_string(name)),
326
225
                minion_ast::Constant::Integer(read_const_1(k)?),
327
            ))
328
        }
329
30
        conjure_ast::Expression::Reify(_metadata, e, v) => Ok(minion_ast::Constraint::Reify(
330
30
            Box::new(read_expr(*e)?),
331
30
            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
18150
}
346
8775
fn read_vars(exprs: Vec<conjure_ast::Expression>) -> Result<Vec<minion_ast::Var>, SolverError> {
347
8775
    let mut minion_vars: Vec<minion_ast::Var> = vec![];
348
34920
    for expr in exprs {
349
26145
        let minion_var = read_var(expr)?;
350
26145
        minion_vars.push(minion_var);
351
    }
352
8775
    Ok(minion_vars)
353
8775
}
354

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

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

            
375
36645
    let str_name = _name_to_string(name);
376
36645
    Ok(str_name)
377
45750
}
378

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

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

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

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