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
        x => Err(ModelFeatureNotSupported(format!("{:?}", x))),
334
    }
335
18150
}
336
8775
fn read_vars(exprs: Vec<conjure_ast::Expression>) -> Result<Vec<minion_ast::Var>, SolverError> {
337
8775
    let mut minion_vars: Vec<minion_ast::Var> = vec![];
338
34920
    for expr in exprs {
339
26145
        let minion_var = read_var(expr)?;
340
26145
        minion_vars.push(minion_var);
341
    }
342
8775
    Ok(minion_vars)
343
8775
}
344

            
345
45750
fn read_var(e: conjure_ast::Expression) -> Result<minion_ast::Var, SolverError> {
346
45750
    // a minion var is either a reference or a "var as const"
347
45750
    match _read_ref(e.clone()) {
348
36645
        Ok(name) => Ok(minion_ast::Var::NameRef(name)),
349
9105
        Err(_) => match read_const(e) {
350
9105
            Ok(n) => Ok(minion_ast::Var::ConstantAsVar(n)),
351
            Err(x) => Err(x),
352
        },
353
    }
354
45750
}
355

            
356
45750
fn _read_ref(e: conjure_ast::Expression) -> Result<String, SolverError> {
357
45750
    let name = match e {
358
36645
        conjure_ast::Expression::FactorE(_metadata, conjure_ast::Factor::Reference(n)) => Ok(n),
359
9105
        x => Err(ModelInvalid(format!(
360
9105
            "expected a reference, but got `{0:?}`",
361
9105
            x
362
9105
        ))),
363
9105
    }?;
364

            
365
36645
    let str_name = _name_to_string(name);
366
36645
    Ok(str_name)
367
45750
}
368

            
369
13890
fn read_const(e: conjure_ast::Expression) -> Result<i32, SolverError> {
370
13890
    match e {
371
13890
        conjure_ast::Expression::FactorE(_, conjure_ast::Factor::Literal(x)) => {
372
13890
            Ok(read_const_1(x)?)
373
        }
374
        x => Err(ModelInvalid(format!(
375
            "expected a constant, but got `{0:?}`",
376
            x
377
        ))),
378
    }
379
13890
}
380

            
381
14115
fn read_const_1(k: conjure_ast::Literal) -> Result<i32, SolverError> {
382
14115
    match k {
383
13830
        conjure_ast::Literal::Int(n) => Ok(n),
384
210
        conjure_ast::Literal::Bool(true) => Ok(1),
385
75
        conjure_ast::Literal::Bool(false) => Ok(0),
386
        x => Err(ModelInvalid(format!(
387
            "expected a constant, but got `{0:?}`",
388
            x
389
        ))),
390
    }
391
14115
}
392

            
393
38655
fn _name_to_string(name: conjure_ast::Name) -> String {
394
38655
    match name {
395
37755
        conjure_ast::Name::UserName(x) => x,
396
900
        conjure_ast::Name::MachineName(x) => format!("__conjure_machine_name_{}", x),
397
    }
398
38655
}
399

            
400
#[allow(clippy::unwrap_used)]
401
690
fn get_solver_stats() -> SolverStats {
402
690
    SolverStats {
403
690
        nodes: get_from_table("Nodes".into()).map(|x| x.parse::<u64>().unwrap()),
404
690
        ..Default::default()
405
690
    }
406
690
}