1
#![allow(unreachable_patterns)]
2

            
3
use std::{
4
    collections::HashMap,
5
    ffi::CString,
6
    sync::Condvar,
7
    sync::{Mutex, MutexGuard},
8
};
9

            
10
use anyhow::anyhow;
11

            
12
use crate::ffi::{self};
13
use crate::{
14
    ast::{Constant, Constraint, Model, Var, VarDomain, VarName},
15
    error::{MinionError, RuntimeError},
16
    scoped_ptr::Scoped,
17
};
18

            
19
/// The callback function used to capture results from Minion as they are generated.
20
///
21
/// This function is called by Minion whenever a solution is found. The input to this function is
22
/// a`HashMap` of all named variables along with their value.
23
///
24
/// Callbacks should return `true` if search is to continue, `false` otherwise.
25
///
26
/// # Examples
27
///
28
/// Consider using a global mutex (or other static variable) to use returned solutions elsewhere.
29
///
30
/// For example:
31
///
32
/// ```
33
1
///   use minion_rs::ast::*;
34
///   use minion_rs::run_minion;
35
///   use std::{
36
///       collections::HashMap,
37
///       sync::{Mutex, MutexGuard},
38
///   };
39
///
40
///   // More elaborate data-structures are possible, but for sake of example store
41
///   // a vector of solution sets.
42
///   static ALL_SOLUTIONS: Mutex<Vec<HashMap<VarName,Constant>>>  = Mutex::new(vec![]);
43
///   
44
///   fn callback(solutions: HashMap<VarName,Constant>) -> bool {
45
1
///       let mut guard = ALL_SOLUTIONS.lock().unwrap();
46
1
///       guard.push(solutions);
47
1
///       true
48
1
///   }
49
1
///    
50
///   // Build and run the model.
51
///   let mut model = Model::new();
52
1
///
53
1
///   // ... omitted for brevity ...
54
1
/// # model
55
1
/// #     .named_variables
56
1
/// #     .add_var("x".to_owned(), VarDomain::Bound(1, 3));
57
1
/// # model
58
1
/// #     .named_variables
59
1
/// #     .add_var("y".to_owned(), VarDomain::Bound(2, 4));
60
1
/// # model
61
1
/// #     .named_variables
62
1
/// #     .add_var("z".to_owned(), VarDomain::Bound(1, 5));
63
1
/// #
64
1
/// # let leq = Constraint::SumLeq(
65
1
/// #     vec![
66
1
/// #         Var::NameRef("x".to_owned()),
67
1
/// #         Var::NameRef("y".to_owned()),
68
1
/// #         Var::NameRef("z".to_owned()),
69
1
/// #     ],
70
1
/// #     Var::ConstantAsVar(4),
71
1
/// # );
72
1
/// #
73
1
/// # let geq = Constraint::SumGeq(
74
1
/// #     vec![
75
1
/// #         Var::NameRef("x".to_owned()),
76
1
/// #         Var::NameRef("y".to_owned()),
77
1
/// #         Var::NameRef("z".to_owned()),
78
1
/// #     ],
79
1
/// #     Var::ConstantAsVar(4),
80
1
/// # );
81
1
/// #
82
1
/// # let ineq = Constraint::Ineq(
83
1
/// #     Var::NameRef("x".to_owned()),
84
1
/// #     Var::NameRef("y".to_owned()),
85
1
/// #     Constant::Integer(-1),
86
1
/// # );
87
1
/// #
88
1
/// # model.constraints.push(leq);
89
1
/// # model.constraints.push(geq);
90
1
/// # model.constraints.push(ineq);
91
1
///  
92
1
///   let res = run_minion(model, callback);
93
1
///   res.expect("Error occurred");
94
1
///
95
1
///   // Get solutions
96
1
///   let guard = ALL_SOLUTIONS.lock().unwrap();
97
1
///   let solution_set_1 = &(guard.get(0).unwrap());
98
1
///
99
1
///   let x1 = solution_set_1.get("x").unwrap();
100
1
///   let y1 = solution_set_1.get("y").unwrap();
101
1
///   let z1 = solution_set_1.get("z").unwrap();
102
1
/// #
103
1
/// # // TODO: this test would be better with an example with >1 solution.
104
1
/// # assert_eq!(guard.len(),1);
105
1
/// # assert_eq!(*x1,Constant::Integer(1));
106
1
/// # assert_eq!(*y1,Constant::Integer(2));
107
1
/// # assert_eq!(*z1,Constant::Integer(1));
108
1
/// ```
109
1
pub type Callback = fn(solution_set: HashMap<VarName, Constant>) -> bool;
110

            
111
// Use globals to pass things between run_minion and the callback function.
112
// Minion is (currently) single threaded anyways so the Mutexs' don't matter.
113

            
114
// the current callback function
115
static CALLBACK: Mutex<Option<Callback>> = Mutex::new(None);
116

            
117
// the variables we want to return, and their ordering in the print matrix
118
static PRINT_VARS: Mutex<Option<Vec<VarName>>> = Mutex::new(None);
119

            
120
static LOCK: (Mutex<bool>, Condvar) = (Mutex::new(false), Condvar::new());
121

            
122
#[no_mangle]
123
8106
unsafe extern "C" fn run_callback() -> bool {
124
8106
    // get printvars from static PRINT_VARS if they exist.
125
8106
    // if not, return true and continue search.
126
8106

            
127
8106
    // Mutex poisoning is probably panic worthy.
128
8106
    #[allow(clippy::unwrap_used)]
129
8106
    let mut guard: MutexGuard<'_, Option<Vec<VarName>>> = PRINT_VARS.lock().unwrap();
130
8106

            
131
8106
    if guard.is_none() {
132
        return true;
133
8106
    }
134

            
135
8106
    let print_vars = match &mut *guard {
136
8106
        Some(x) => x,
137
        None => unreachable!(),
138
    };
139

            
140
8106
    if print_vars.is_empty() {
141
        return true;
142
8106
    }
143
8106

            
144
8106
    // build nice solutions view to be used by callback
145
8106
    let mut solutions: HashMap<VarName, Constant> = HashMap::new();
146

            
147
21903
    for (i, var) in print_vars.iter().enumerate() {
148
21903
        let solution_int: i32 = ffi::printMatrix_getValue(i as _);
149
21903
        let solution: Constant = Constant::Integer(solution_int);
150
21903
        solutions.insert(var.to_string(), solution);
151
21903
    }
152

            
153
    #[allow(clippy::unwrap_used)]
154
8106
    match *CALLBACK.lock().unwrap() {
155
        None => true,
156
8106
        Some(func) => func(solutions),
157
    }
158
8106
}
159

            
160
/// Run Minion on the given [Model].
161
///
162
/// The given [callback](Callback) is ran whenever a new solution set is found.
163

            
164
// Turn it into a warning for this function, cant unwarn it directly above callback wierdness
165
#[allow(clippy::unwrap_used)]
166
1029
pub fn run_minion(model: Model, callback: Callback) -> Result<(), MinionError> {
167
1029
    // Mutex poisoning is probably panic worthy.
168
1029
    *CALLBACK.lock().unwrap() = Some(callback);
169
1029

            
170
1029
    let (lock, condvar) = &LOCK;
171
1029
    let mut _lock_guard = condvar
172
1029
        .wait_while(lock.lock().unwrap(), |locked| *locked)
173
1029
        .unwrap();
174
1029

            
175
1029
    *_lock_guard = true;
176
1029

            
177
1029
    unsafe {
178
1029
        // TODO: something better than a manual spinlock
179
1029
        let search_opts = ffi::searchOptions_new();
180
1029
        let search_method = ffi::searchMethod_new();
181
1029
        let search_instance = ffi::instance_new();
182
1029

            
183
1029
        convert_model_to_raw(search_instance, &model)?;
184

            
185
1029
        let res = ffi::runMinion(
186
1029
            search_opts,
187
1029
            search_method,
188
1029
            search_instance,
189
1029
            Some(run_callback),
190
1029
        );
191
1029

            
192
1029
        ffi::searchMethod_free(search_method);
193
1029
        ffi::searchOptions_free(search_opts);
194
1029
        ffi::instance_free(search_instance);
195
1029

            
196
1029
        *_lock_guard = false;
197
1029
        std::mem::drop(_lock_guard);
198
1029

            
199
1029
        condvar.notify_one();
200
1029

            
201
1029
        match res {
202
1029
            0 => Ok(()),
203
            x => Err(MinionError::from(RuntimeError::from(x))),
204
        }
205
    }
206
1029
}
207

            
208
1029
unsafe fn convert_model_to_raw(
209
1029
    instance: *mut ffi::ProbSpec_CSPInstance,
210
1029
    model: &Model,
211
1029
) -> Result<(), MinionError> {
212
1029
    /*******************************/
213
1029
    /*        Add variables        */
214
1029
    /*******************************/
215
1029

            
216
1029
    /*
217
1029
     * Add variables to:
218
1029
     * 1. symbol table
219
1029
     * 2. print matrix
220
1029
     * 3. search vars
221
1029
     *
222
1029
     * These are all done in the order saved in the SymbolTable.
223
1029
     */
224
1029

            
225
1029
    let search_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
226
1029

            
227
1029
    // store variables and the order they will be returned inside rust for later use.
228
1029
    #[allow(clippy::unwrap_used)]
229
1029
    let mut print_vars_guard = PRINT_VARS.lock().unwrap();
230
1029
    *print_vars_guard = Some(vec![]);
231

            
232
2688
    for var_name in model.named_variables.get_variable_order() {
233
2688
        let c_str = CString::new(var_name.clone()).map_err(|_| {
234
            anyhow!(
235
                "Variable name {:?} contains a null character.",
236
                var_name.clone()
237
            )
238
2688
        })?;
239

            
240
2688
        let vartype = model
241
2688
            .named_variables
242
2688
            .get_vartype(var_name.clone())
243
2688
            .ok_or(anyhow!("Could not get var type for {:?}", var_name.clone()))?;
244

            
245
2688
        let (vartype_raw, domain_low, domain_high) = match vartype {
246
2226
            VarDomain::Bound(a, b) => Ok((ffi::VariableType_VAR_BOUND, a, b)),
247
462
            VarDomain::Bool => Ok((ffi::VariableType_VAR_BOOL, 0, 1)), // TODO: will this work?
248
            x => Err(MinionError::NotImplemented(format!("{:?}", x))),
249
        }?;
250

            
251
2688
        ffi::newVar_ffi(
252
2688
            instance,
253
2688
            c_str.as_ptr() as _,
254
2688
            vartype_raw,
255
2688
            domain_low,
256
2688
            domain_high,
257
2688
        );
258
2688

            
259
2688
        let var = ffi::getVarByName(instance, c_str.as_ptr() as _);
260
2688

            
261
2688
        ffi::printMatrix_addVar(instance, var);
262
2688

            
263
2688
        // add to the print vars stored in rust so to remember
264
2688
        // the order for callback function.
265
2688

            
266
2688
        #[allow(clippy::unwrap_used)]
267
2688
        (*print_vars_guard).as_mut().unwrap().push(var_name.clone());
268
2688

            
269
2688
        ffi::vec_var_push_back(search_vars.ptr, var);
270
    }
271

            
272
1029
    let search_order = Scoped::new(
273
1029
        ffi::searchOrder_new(search_vars.ptr, ffi::VarOrderEnum_ORDER_STATIC, false),
274
1029
        |x| ffi::searchOrder_free(x as _),
275
1029
    );
276
1029

            
277
1029
    ffi::instance_addSearchOrder(instance, search_order.ptr);
278

            
279
    /*********************************/
280
    /*        Add constraints        */
281
    /*********************************/
282

            
283
8127
    for constraint in &model.constraints {
284
        // 1. get constraint type and create C++ constraint object
285
        // 2. run through arguments and add them to the constraint
286
        // 3. add constraint to instance
287

            
288
7098
        let constraint_type = get_constraint_type(constraint)?;
289
7098
        let raw_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
290
7098
            ffi::constraint_free(x as _)
291
7098
        });
292
7098

            
293
7098
        constraint_add_args(instance, raw_constraint.ptr, constraint)?;
294
7098
        ffi::instance_addConstraint(instance, raw_constraint.ptr);
295
    }
296

            
297
1029
    Ok(())
298
1029
}
299

            
300
25683
unsafe fn get_constraint_type(constraint: &Constraint) -> Result<u32, MinionError> {
301
25683
    match constraint {
302
6153
        Constraint::SumGeq(_, _) => Ok(ffi::ConstraintType_CT_GEQSUM),
303
6216
        Constraint::SumLeq(_, _) => Ok(ffi::ConstraintType_CT_LEQSUM),
304
6741
        Constraint::Ineq(_, _, _) => Ok(ffi::ConstraintType_CT_INEQ),
305
462
        Constraint::Eq(_, _) => Ok(ffi::ConstraintType_CT_EQ),
306
        Constraint::Difference(_, _) => Ok(ffi::ConstraintType_CT_DIFFERENCE),
307
        Constraint::Div(_, _) => Ok(ffi::ConstraintType_CT_DIV),
308
126
        Constraint::DivUndefZero(_, _) => Ok(ffi::ConstraintType_CT_DIV_UNDEFZERO),
309
        Constraint::Modulo(_, _) => Ok(ffi::ConstraintType_CT_MODULO),
310
        Constraint::ModuloUndefZero(_, _) => Ok(ffi::ConstraintType_CT_MODULO_UNDEFZERO),
311
        Constraint::Pow(_, _) => Ok(ffi::ConstraintType_CT_POW),
312
        Constraint::Product(_, _) => Ok(ffi::ConstraintType_CT_PRODUCT2),
313
        Constraint::WeightedSumGeq(_, _, _) => Ok(ffi::ConstraintType_CT_WEIGHTGEQSUM),
314
        Constraint::WeightedSumLeq(_, _, _) => Ok(ffi::ConstraintType_CT_WEIGHTLEQSUM),
315
        Constraint::CheckAssign(_) => Ok(ffi::ConstraintType_CT_CHECK_ASSIGN),
316
        Constraint::CheckGsa(_) => Ok(ffi::ConstraintType_CT_CHECK_GSA),
317
        Constraint::ForwardChecking(_) => Ok(ffi::ConstraintType_CT_FORWARD_CHECKING),
318
42
        Constraint::Reify(_, _) => Ok(ffi::ConstraintType_CT_REIFY),
319
21
        Constraint::ReifyImply(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY),
320
        Constraint::ReifyImplyQuick(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY_QUICK),
321
21
        Constraint::WatchedAnd(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_AND),
322
5271
        Constraint::WatchedOr(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_OR),
323
        Constraint::GacAllDiff(_) => Ok(ffi::ConstraintType_CT_GACALLDIFF),
324
        Constraint::AllDiff(_) => Ok(ffi::ConstraintType_CT_ALLDIFF),
325
        Constraint::AllDiffMatrix(_, _) => Ok(ffi::ConstraintType_CT_ALLDIFFMATRIX),
326
        Constraint::WatchSumGeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_GEQSUM),
327
        Constraint::WatchSumLeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LEQSUM),
328
        Constraint::OccurrenceGeq(_, _, _) => Ok(ffi::ConstraintType_CT_GEQ_OCCURRENCE),
329
        Constraint::OccurrenceLeq(_, _, _) => Ok(ffi::ConstraintType_CT_LEQ_OCCURRENCE),
330
        Constraint::Occurrence(_, _, _) => Ok(ffi::ConstraintType_CT_OCCURRENCE),
331
        Constraint::LitSumGeq(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_LITSUM),
332
        Constraint::Gcc(_, _, _) => Ok(ffi::ConstraintType_CT_GCC),
333
        Constraint::GccWeak(_, _, _) => Ok(ffi::ConstraintType_CT_GCCWEAK),
334
        Constraint::LexLeqRv(_, _) => Ok(ffi::ConstraintType_CT_GACLEXLEQ),
335
        Constraint::LexLeq(_, _) => Ok(ffi::ConstraintType_CT_LEXLEQ),
336
        Constraint::LexLess(_, _) => Ok(ffi::ConstraintType_CT_LEXLESS),
337
        Constraint::LexLeqQuick(_, _) => Ok(ffi::ConstraintType_CT_QUICK_LEXLEQ),
338
        Constraint::LexLessQuick(_, _) => Ok(ffi::ConstraintType_CT_QUICK_LEXLEQ),
339
        Constraint::WatchVecNeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_VECNEQ),
340
        Constraint::WatchVecExistsLess(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_VEC_OR_LESS),
341
        Constraint::Hamming(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_HAMMING),
342
        Constraint::NotHamming(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_HAMMING),
343
        Constraint::FrameUpdate(_, _, _, _, _) => Ok(ffi::ConstraintType_CT_FRAMEUPDATE),
344
        Constraint::NegativeTable(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NEGATIVE_TABLE),
345
        Constraint::Table(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_TABLE),
346
        Constraint::GacSchema(_, _) => Ok(ffi::ConstraintType_CT_GACSCHEMA),
347
        Constraint::LightTable(_, _) => Ok(ffi::ConstraintType_CT_LIGHTTABLE),
348
        Constraint::Mddc(_, _) => Ok(ffi::ConstraintType_CT_MDDC),
349
        Constraint::NegativeMddc(_, _) => Ok(ffi::ConstraintType_CT_NEGATIVEMDDC),
350
        Constraint::Str2Plus(_, _) => Ok(ffi::ConstraintType_CT_STR),
351
        Constraint::Max(_, _) => Ok(ffi::ConstraintType_CT_MAX),
352
        Constraint::Min(_, _) => Ok(ffi::ConstraintType_CT_MIN),
353
        Constraint::NvalueGeq(_, _) => Ok(ffi::ConstraintType_CT_GEQNVALUE),
354
        Constraint::NvalueLeq(_, _) => Ok(ffi::ConstraintType_CT_LEQNVALUE),
355
        Constraint::Element(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT),
356
        Constraint::ElementOne(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT_ONE),
357
        Constraint::ElementUndefZero(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT_UNDEFZERO),
358
        Constraint::WatchElement(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT),
359
        Constraint::WatchElementOne(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_ONE),
360
        Constraint::WatchElementOneUndefZero(_, _, _) => {
361
            Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_ONE_UNDEFZERO)
362
        }
363
        Constraint::WatchElementUndefZero(_, _, _) => {
364
            Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_UNDEFZERO)
365
        }
366
315
        Constraint::WLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LIT),
367
        Constraint::WNotLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOTLIT),
368
        Constraint::WInIntervalSet(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_ININTERVALSET),
369
        Constraint::WInRange(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_INRANGE),
370
42
        Constraint::WInset(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_INSET),
371
        Constraint::WNotInRange(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_INRANGE),
372
        Constraint::WNotInset(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_INSET),
373
        Constraint::Abs(_, _) => Ok(ffi::ConstraintType_CT_ABS),
374
210
        Constraint::DisEq(_, _) => Ok(ffi::ConstraintType_CT_DISEQ),
375
        Constraint::MinusEq(_, _) => Ok(ffi::ConstraintType_CT_MINUSEQ),
376
        Constraint::GacEq(_, _) => Ok(ffi::ConstraintType_CT_GACEQ),
377
        Constraint::WatchLess(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LESS),
378
        Constraint::WatchNeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NEQ),
379
42
        Constraint::True => Ok(ffi::ConstraintType_CT_TRUE),
380
21
        Constraint::False => Ok(ffi::ConstraintType_CT_FALSE),
381

            
382
        #[allow(unreachable_patterns)]
383
        x => Err(MinionError::NotImplemented(format!(
384
            "Constraint not implemented {:?}",
385
            x,
386
        ))),
387
    }
388
25683
}
389

            
390
25683
unsafe fn constraint_add_args(
391
25683
    i: *mut ffi::ProbSpec_CSPInstance,
392
25683
    r_constr: *mut ffi::ProbSpec_ConstraintBlob,
393
25683
    constr: &Constraint,
394
25683
) -> Result<(), MinionError> {
395
25683
    match constr {
396
6153
        Constraint::SumGeq(lhs_vars, rhs_var) => {
397
6153
            read_list(i, r_constr, lhs_vars)?;
398
6153
            read_var(i, r_constr, rhs_var)?;
399
6153
            Ok(())
400
        }
401
6216
        Constraint::SumLeq(lhs_vars, rhs_var) => {
402
6216
            read_list(i, r_constr, lhs_vars)?;
403
6216
            read_var(i, r_constr, rhs_var)?;
404
6216
            Ok(())
405
        }
406
6741
        Constraint::Ineq(var1, var2, c) => {
407
6741
            read_var(i, r_constr, var1)?;
408
6741
            read_var(i, r_constr, var2)?;
409
6741
            read_constant(r_constr, c)?;
410
6741
            Ok(())
411
        }
412
462
        Constraint::Eq(var1, var2) => {
413
462
            read_var(i, r_constr, var1)?;
414
462
            read_var(i, r_constr, var2)?;
415
462
            Ok(())
416
        }
417
        Constraint::Difference((a, b), c) => {
418
            read_2_vars(i, r_constr, a, b)?;
419
            read_var(i, r_constr, c)?;
420
            Ok(())
421
        }
422
        Constraint::Div((a, b), c) => {
423
            read_2_vars(i, r_constr, a, b)?;
424
            read_var(i, r_constr, c)?;
425
            Ok(())
426
        }
427
126
        Constraint::DivUndefZero((a, b), c) => {
428
126
            read_2_vars(i, r_constr, a, b)?;
429
126
            read_var(i, r_constr, c)?;
430
126
            Ok(())
431
        }
432
        Constraint::Modulo((a, b), c) => {
433
            read_2_vars(i, r_constr, a, b)?;
434
            read_var(i, r_constr, c)?;
435
            Ok(())
436
        }
437
        Constraint::ModuloUndefZero((a, b), c) => {
438
            read_2_vars(i, r_constr, a, b)?;
439
            read_var(i, r_constr, c)?;
440
            Ok(())
441
        }
442
        Constraint::Pow((a, b), c) => {
443
            read_2_vars(i, r_constr, a, b)?;
444
            read_var(i, r_constr, c)?;
445
            Ok(())
446
        }
447
        Constraint::Product((a, b), c) => {
448
            read_2_vars(i, r_constr, a, b)?;
449
            read_var(i, r_constr, c)?;
450
            Ok(())
451
        }
452
        Constraint::WeightedSumGeq(a, b, c) => {
453
            read_constant_list(r_constr, a)?;
454
            read_list(i, r_constr, b)?;
455
            read_var(i, r_constr, c)?;
456
            Ok(())
457
        }
458
        Constraint::WeightedSumLeq(a, b, c) => {
459
            read_constant_list(r_constr, a)?;
460
            read_list(i, r_constr, b)?;
461
            read_var(i, r_constr, c)?;
462
            Ok(())
463
        }
464
        Constraint::CheckAssign(a) => {
465
            read_constraint(i, r_constr, (**a).clone())?;
466
            Ok(())
467
        }
468
        Constraint::CheckGsa(a) => {
469
            read_constraint(i, r_constr, (**a).clone())?;
470
            Ok(())
471
        }
472
        Constraint::ForwardChecking(a) => {
473
            read_constraint(i, r_constr, (**a).clone())?;
474
            Ok(())
475
        }
476
42
        Constraint::Reify(a, b) => {
477
42
            read_constraint(i, r_constr, (**a).clone())?;
478
42
            read_var(i, r_constr, b)?;
479
42
            Ok(())
480
        }
481
21
        Constraint::ReifyImply(a, b) => {
482
21
            read_constraint(i, r_constr, (**a).clone())?;
483
21
            read_var(i, r_constr, b)?;
484
21
            Ok(())
485
        }
486
        Constraint::ReifyImplyQuick(a, b) => {
487
            read_constraint(i, r_constr, (**a).clone())?;
488
            read_var(i, r_constr, b)?;
489
            Ok(())
490
        }
491
21
        Constraint::WatchedAnd(a) => {
492
21
            read_constraint_list(i, r_constr, a)?;
493
21
            Ok(())
494
        }
495
5271
        Constraint::WatchedOr(a) => {
496
5271
            read_constraint_list(i, r_constr, a)?;
497
5271
            Ok(())
498
        }
499
        Constraint::GacAllDiff(a) => {
500
            read_list(i, r_constr, a)?;
501
            Ok(())
502
        }
503
        Constraint::AllDiff(a) => {
504
            read_list(i, r_constr, a)?;
505
            Ok(())
506
        }
507
        Constraint::AllDiffMatrix(a, b) => {
508
            read_list(i, r_constr, a)?;
509
            read_constant(r_constr, b)?;
510
            Ok(())
511
        }
512
        Constraint::WatchSumGeq(a, b) => {
513
            read_list(i, r_constr, a)?;
514
            read_constant(r_constr, b)?;
515
            Ok(())
516
        }
517
        Constraint::WatchSumLeq(a, b) => {
518
            read_list(i, r_constr, a)?;
519
            read_constant(r_constr, b)?;
520
            Ok(())
521
        }
522
        Constraint::OccurrenceGeq(a, b, c) => {
523
            read_list(i, r_constr, a)?;
524
            read_constant(r_constr, b)?;
525
            read_constant(r_constr, c)?;
526
            Ok(())
527
        }
528
        Constraint::OccurrenceLeq(a, b, c) => {
529
            read_list(i, r_constr, a)?;
530
            read_constant(r_constr, b)?;
531
            read_constant(r_constr, c)?;
532
            Ok(())
533
        }
534
        Constraint::Occurrence(a, b, c) => {
535
            read_list(i, r_constr, a)?;
536
            read_constant(r_constr, b)?;
537
            read_var(i, r_constr, c)?;
538
            Ok(())
539
        }
540
        //Constraint::LitSumGeq(_, _, _) => todo!(),
541
        //Constraint::Gcc(_, _, _) => todo!(),
542
        //Constraint::GccWeak(_, _, _) => todo!(),
543
        //Constraint::LexLeqRv(_, _) => todo!(),
544
        //Constraint::LexLeq(_, _) => todo!(),
545
        //Constraint::LexLess(_, _) => todo!(),
546
        //Constraint::LexLeqQuick(_, _) => todo!(),
547
        //Constraint::LexLessQuick(_, _) => todo!(),
548
        //Constraint::WatchVecNeq(_, _) => todo!(),
549
        //Constraint::WatchVecExistsLess(_, _) => todo!(),
550
        //Constraint::Hamming(_, _, _) => todo!(),
551
        //Constraint::NotHamming(_, _, _) => todo!(),
552
        //Constraint::FrameUpdate(_, _, _, _, _) => todo!(),
553
        //Constraint::NegativeTable(_, _) => todo!(),
554
        //Constraint::Table(_, _) => todo!(),
555
        //Constraint::GacSchema(_, _) => todo!(),
556
        //Constraint::LightTable(_, _) => todo!(),
557
        //Constraint::Mddc(_, _) => todo!(),
558
        //Constraint::NegativeMddc(_, _) => todo!(),
559
        //Constraint::Str2Plus(_, _) => todo!(),
560
        //Constraint::Max(_, _) => todo!(),
561
        //Constraint::Min(_, _) => todo!(),
562
        //Constraint::NvalueGeq(_, _) => todo!(),
563
        //Constraint::NvalueLeq(_, _) => todo!(),
564
        //Constraint::Element(_, _, _) => todo!(),
565
        //Constraint::ElementOne(_, _, _) => todo!(),
566
        //Constraint::ElementUndefZero(_, _, _) => todo!(),
567
        //Constraint::WatchElement(_, _, _) => todo!(),
568
        //Constraint::WatchElementOne(_, _, _) => todo!(),
569
        //Constraint::WatchElementOneUndefZero(_, _, _) => todo!(),
570
        //Constraint::WatchElementUndefZero(_, _, _) => todo!(),
571
315
        Constraint::WLiteral(a, b) => {
572
315
            read_var(i, r_constr, a)?;
573
315
            read_constant(r_constr, b)?;
574
315
            Ok(())
575
        }
576
        //Constraint::WNotLiteral(_, _) => todo!(),
577
        //Constraint::WInIntervalSet(_, _) => todo!(),
578
        //Constraint::WInRange(_, _) => todo!(),
579
42
        Constraint::WInset(a, b) => {
580
42
            read_var(i, r_constr, a)?;
581
42
            read_constant_list(r_constr, b)?;
582
42
            Ok(())
583
        }
584
        //Constraint::WNotInRange(_, _) => todo!(),
585
        //Constraint::WNotInset(_, _) => todo!(),
586
        //Constraint::Abs(_, _) => todo!(),
587
210
        Constraint::DisEq(a, b) => {
588
210
            read_var(i, r_constr, a)?;
589
210
            read_var(i, r_constr, b)?;
590
210
            Ok(())
591
        }
592
        //Constraint::MinusEq(_, _) => todo!(),
593
        //Constraint::GacEq(_, _) => todo!(),
594
        //Constraint::WatchLess(_, _) => todo!(),
595
        // TODO: ensure that this is a bool?
596
        Constraint::WatchNeq(a, b) => {
597
            read_var(i, r_constr, a)?;
598
            read_var(i, r_constr, b)?;
599
            Ok(())
600
        }
601

            
602
42
        Constraint::True => Ok(()),
603
21
        Constraint::False => Ok(()),
604
        #[allow(unreachable_patterns)]
605
        x => Err(MinionError::NotImplemented(format!("{:?}", x))),
606
    }
607
25683
}
608

            
609
// DO NOT call manually - this assumes that all needed vars are already in the symbol table.
610
// TODO not happy with this just assuming the name is in the symbol table
611
12369
unsafe fn read_list(
612
12369
    instance: *mut ffi::ProbSpec_CSPInstance,
613
12369
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
614
12369
    vars: &Vec<Var>,
615
12369
) -> Result<(), MinionError> {
616
12369
    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
617
49224
    for var in vars {
618
36855
        let raw_var = match var {
619
36813
            Var::NameRef(name) => {
620
36813
                let c_str = CString::new(name.clone()).map_err(|_| {
621
                    anyhow!(
622
                        "Variable name {:?} contains a null character.",
623
                        name.clone()
624
                    )
625
36813
                })?;
626
36813
                ffi::getVarByName(instance, c_str.as_ptr() as _)
627
            }
628
42
            Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
629
        };
630

            
631
36855
        ffi::vec_var_push_back(raw_vars.ptr, raw_var);
632
    }
633

            
634
12369
    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
635
12369

            
636
12369
    Ok(())
637
12369
}
638

            
639
27741
unsafe fn read_var(
640
27741
    instance: *mut ffi::ProbSpec_CSPInstance,
641
27741
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
642
27741
    var: &Var,
643
27741
) -> Result<(), MinionError> {
644
27741
    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
645
27741
    let raw_var = match var {
646
14973
        Var::NameRef(name) => {
647
14973
            let c_str = CString::new(name.clone()).map_err(|_| {
648
                anyhow!(
649
                    "Variable name {:?} contains a null character.",
650
                    name.clone()
651
                )
652
14973
            })?;
653
14973
            ffi::getVarByName(instance, c_str.as_ptr() as _)
654
        }
655
12768
        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
656
    };
657

            
658
27741
    ffi::vec_var_push_back(raw_vars.ptr, raw_var);
659
27741
    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
660
27741

            
661
27741
    Ok(())
662
27741
}
663

            
664
126
unsafe fn read_2_vars(
665
126
    instance: *mut ffi::ProbSpec_CSPInstance,
666
126
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
667
126
    var1: &Var,
668
126
    var2: &Var,
669
126
) -> Result<(), MinionError> {
670
126
    let mut raw_var = match var1 {
671
105
        Var::NameRef(name) => {
672
105
            let c_str = CString::new(name.clone()).map_err(|_| {
673
                anyhow!(
674
                    "Variable name {:?} contains a null character.",
675
                    name.clone()
676
                )
677
105
            })?;
678
105
            ffi::getVarByName(instance, c_str.as_ptr() as _)
679
        }
680
21
        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
681
    };
682
126
    let mut raw_var2 = match var2 {
683
126
        Var::NameRef(name) => {
684
126
            let c_str = CString::new(name.clone()).map_err(|_| {
685
                anyhow!(
686
                    "Variable name {:?} contains a null character.",
687
                    name.clone()
688
                )
689
126
            })?;
690
126
            ffi::getVarByName(instance, c_str.as_ptr() as _)
691
        }
692
        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
693
    };
694
    // todo: does this move or copy? I am confus!
695
    // TODO need to mkae the semantics of move vs copy / ownership clear in libminion!!
696
    // This shouldve leaked everywhere by now but i think libminion copies stuff??
697
126
    ffi::constraint_addTwoVars(raw_constraint, &mut raw_var, &mut raw_var2);
698
126
    Ok(())
699
126
}
700

            
701
7056
unsafe fn read_constant(
702
7056
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
703
7056
    constant: &Constant,
704
7056
) -> Result<(), MinionError> {
705
7056
    let val: i32 = match constant {
706
7056
        Constant::Integer(n) => Ok(*n),
707
        Constant::Bool(true) => Ok(1),
708
        Constant::Bool(false) => Ok(0),
709
        x => Err(MinionError::NotImplemented(format!("{:?}", x))),
710
    }?;
711

            
712
7056
    ffi::constraint_addConstant(raw_constraint, val);
713
7056

            
714
7056
    Ok(())
715
7056
}
716

            
717
42
unsafe fn read_constant_list(
718
42
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
719
42
    constants: &[Constant],
720
42
) -> Result<(), MinionError> {
721
42
    let raw_consts = Scoped::new(ffi::vec_int_new(), |x| ffi::vec_var_free(x as _));
722

            
723
42
    for constant in constants.iter() {
724
42
        let val = match constant {
725
            Constant::Integer(n) => Ok(*n),
726
21
            Constant::Bool(true) => Ok(1),
727
21
            Constant::Bool(false) => Ok(0),
728
            #[allow(unreachable_patterns)] // TODO: can there be other types?
729
            x => Err(MinionError::NotImplemented(format!("{:?}", x))),
730
        }?;
731

            
732
42
        ffi::vec_int_push_back(raw_consts.ptr, val);
733
    }
734

            
735
42
    ffi::constraint_addConstantList(raw_constraint, raw_consts.ptr);
736
42
    Ok(())
737
42
}
738

            
739
//TODO: check if the inner constraint is listed in the model or not?
740
//Does this matter?
741
// TODO: type-check inner constraints vars and tuples and so on?
742
63
unsafe fn read_constraint(
743
63
    instance: *mut ffi::ProbSpec_CSPInstance,
744
63
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
745
63
    inner_constraint: Constraint,
746
63
) -> Result<(), MinionError> {
747
63
    let constraint_type = get_constraint_type(&inner_constraint)?;
748
63
    let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
749
63
        ffi::constraint_free(x as _)
750
63
    });
751
63

            
752
63
    constraint_add_args(instance, raw_inner_constraint.ptr, &inner_constraint)?;
753

            
754
63
    ffi::constraint_addConstraint(raw_constraint, raw_inner_constraint.ptr);
755
63
    Ok(())
756
63
}
757

            
758
5292
unsafe fn read_constraint_list(
759
5292
    instance: *mut ffi::ProbSpec_CSPInstance,
760
5292
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
761
5292
    inner_constraints: &[Constraint],
762
5292
) -> Result<(), MinionError> {
763
5292
    let raw_inners = Scoped::new(ffi::vec_constraints_new(), |x| {
764
5292
        ffi::vec_constraints_free(x as _)
765
5292
    });
766
18522
    for inner_constraint in inner_constraints.iter() {
767
18522
        let constraint_type = get_constraint_type(inner_constraint)?;
768
18522
        let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
769
18522
            ffi::constraint_free(x as _)
770
18522
        });
771
18522

            
772
18522
        constraint_add_args(instance, raw_inner_constraint.ptr, inner_constraint)?;
773
18522
        ffi::vec_constraints_push_back(raw_inners.ptr, raw_inner_constraint.ptr);
774
    }
775

            
776
5292
    ffi::constraint_addConstraintList(raw_constraint, raw_inners.ptr);
777
5292
    Ok(())
778
5292
}