1
#![allow(unreachable_patterns)]
2
#![allow(unsafe_op_in_unsafe_fn)]
3

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

            
11
use anyhow::anyhow;
12

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

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

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

            
118
// the current callback function
119
static CALLBACK: Mutex<Option<Callback>> = Mutex::new(None);
120

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

            
124
static LOCK: (Mutex<bool>, Condvar) = (Mutex::new(false), Condvar::new());
125

            
126
#[unsafe(no_mangle)]
127
717876
unsafe extern "C" fn run_callback() -> bool {
128
    // get printvars from static PRINT_VARS if they exist.
129
    // if not, return true and continue search.
130

            
131
    // Mutex poisoning is probably panic worthy.
132
    #[allow(clippy::unwrap_used)]
133
717876
    let mut guard: MutexGuard<'_, Option<Vec<VarName>>> = PRINT_VARS.lock().unwrap();
134

            
135
717876
    if guard.is_none() {
136
        return true;
137
717876
    }
138

            
139
717876
    let print_vars = match &mut *guard {
140
717876
        Some(x) => x,
141
        None => unreachable!(),
142
    };
143

            
144
717876
    if print_vars.is_empty() {
145
1512
        return true;
146
716364
    }
147

            
148
    // build nice solutions view to be used by callback
149
716364
    let mut solutions: HashMap<VarName, Constant> = HashMap::new();
150

            
151
5644476
    for (i, var) in print_vars.iter().enumerate() {
152
5644476
        let solution_int: i32 = ffi::printMatrix_getValue(i as _);
153
5644476
        let solution: Constant = Constant::Integer(solution_int);
154
5644476
        solutions.insert(var.to_string(), solution);
155
5644476
    }
156

            
157
    #[allow(clippy::unwrap_used)]
158
716364
    match *CALLBACK.lock().unwrap() {
159
        None => true,
160
716364
        Some(func) => func(solutions),
161
    }
162
717876
}
163

            
164
/// Run Minion on the given [Model].
165
///
166
/// The given [callback](Callback) is ran whenever a new solution set is found.
167
// Turn it into a warning for this function, cant unwarn it directly above callback wierdness
168
#[allow(clippy::unwrap_used)]
169
30750
pub fn run_minion(model: Model, callback: Callback) -> Result<(), MinionError> {
170
    // Mutex poisoning is probably panic worthy.
171
30750
    *CALLBACK.lock().unwrap() = Some(callback);
172

            
173
30750
    let (lock, condvar) = &LOCK;
174
30750
    let mut _lock_guard = condvar
175
30750
        .wait_while(lock.lock().unwrap(), |locked| *locked)
176
30750
        .unwrap();
177

            
178
30750
    *_lock_guard = true;
179

            
180
    unsafe {
181
        // TODO: something better than a manual spinlock
182
30750
        let search_opts = ffi::searchOptions_new();
183
30750
        let search_method = ffi::searchMethod_new();
184
30750
        let search_instance = ffi::instance_new();
185

            
186
30750
        convert_model_to_raw(search_instance, &model)?;
187

            
188
30750
        let res = ffi::runMinion(
189
30750
            search_opts,
190
30750
            search_method,
191
30750
            search_instance,
192
30750
            Some(run_callback),
193
        );
194

            
195
30750
        ffi::searchMethod_free(search_method);
196
30750
        ffi::searchOptions_free(search_opts);
197
30750
        ffi::instance_free(search_instance);
198

            
199
30750
        *_lock_guard = false;
200
30750
        std::mem::drop(_lock_guard);
201

            
202
30750
        condvar.notify_one();
203

            
204
30750
        match res {
205
30750
            0 => Ok(()),
206
            x => Err(MinionError::from(RuntimeError::from(x))),
207
        }
208
    }
209
30750
}
210

            
211
30750
unsafe fn convert_model_to_raw(
212
30750
    instance: *mut ffi::ProbSpec_CSPInstance,
213
30750
    model: &Model,
214
30750
) -> Result<(), MinionError> {
215
    /*******************************/
216
    /*        Add variables        */
217
    /*******************************/
218

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

            
228
30750
    let search_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
229

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

            
235
    // initialise all variables, and add all variables to the print order
236
198722
    for var_name in model.named_variables.get_variable_order() {
237
198722
        let c_str = CString::new(var_name.clone()).map_err(|_| {
238
            anyhow!(
239
                "Variable name {:?} contains a null character.",
240
                var_name.clone()
241
            )
242
        })?;
243

            
244
198722
        let vartype = model
245
198722
            .named_variables
246
198722
            .get_vartype(var_name.clone())
247
198722
            .ok_or(anyhow!("Could not get var type for {:?}", var_name.clone()))?;
248

            
249
198722
        let (vartype_raw, domain_low, domain_high) = match vartype {
250
14532
            VarDomain::Bound(a, b) => Ok((ffi::VariableType_VAR_BOUND, a, b)),
251
164780
            VarDomain::Discrete(a, b) => Ok((ffi::VariableType_VAR_DISCRETE, a, b)),
252
19410
            VarDomain::Bool => Ok((ffi::VariableType_VAR_BOOL, 0, 1)), // TODO: will this work?
253
            x => Err(MinionError::NotImplemented(format!("{x:?}"))),
254
        }?;
255

            
256
198722
        ffi::newVar_ffi(
257
198722
            instance,
258
198722
            c_str.as_ptr() as _,
259
198722
            vartype_raw,
260
198722
            domain_low,
261
198722
            domain_high,
262
        );
263

            
264
198722
        let var = ffi::getVarByName(instance, c_str.as_ptr() as _);
265

            
266
198722
        ffi::printMatrix_addVar(instance, var);
267

            
268
        // add to the print vars stored in rust so to remember
269
        // the order for callback function.
270

            
271
        #[allow(clippy::unwrap_used)]
272
198722
        (*print_vars_guard).as_mut().unwrap().push(var_name.clone());
273
    }
274

            
275
    // only add search variables to search order
276
70958
    for search_var_name in model.named_variables.get_search_variable_order() {
277
70958
        let c_str = CString::new(search_var_name.clone()).map_err(|_| {
278
            anyhow!(
279
                "Variable name {:?} contains a null character.",
280
                search_var_name.clone()
281
            )
282
        })?;
283
70958
        let var = ffi::getVarByName(instance, c_str.as_ptr() as _);
284
70958
        ffi::vec_var_push_back(search_vars.ptr, var);
285
    }
286

            
287
30750
    let search_order = Scoped::new(
288
30750
        ffi::searchOrder_new(search_vars.ptr, ffi::VarOrderEnum_ORDER_STATIC, false),
289
30750
        |x| ffi::searchOrder_free(x as _),
290
    );
291

            
292
30750
    ffi::instance_addSearchOrder(instance, search_order.ptr);
293

            
294
    /*********************************/
295
    /*        Add constraints        */
296
    /*********************************/
297

            
298
117102
    for constraint in &model.constraints {
299
        // 1. get constraint type and create C++ constraint object
300
        // 2. run through arguments and add them to the constraint
301
        // 3. add constraint to instance
302

            
303
117102
        let constraint_type = get_constraint_type(constraint)?;
304
117102
        let raw_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
305
117102
            ffi::constraint_free(x as _)
306
117102
        });
307

            
308
117102
        constraint_add_args(instance, raw_constraint.ptr, constraint)?;
309
117102
        ffi::instance_addConstraint(instance, raw_constraint.ptr);
310
    }
311

            
312
30750
    Ok(())
313
30750
}
314

            
315
148434
unsafe fn get_constraint_type(constraint: &Constraint) -> Result<u32, MinionError> {
316
148434
    match constraint {
317
17612
        Constraint::SumGeq(_, _) => Ok(ffi::ConstraintType_CT_GEQSUM),
318
17276
        Constraint::SumLeq(_, _) => Ok(ffi::ConstraintType_CT_LEQSUM),
319
21560
        Constraint::Ineq(_, _, _) => Ok(ffi::ConstraintType_CT_INEQ),
320
16520
        Constraint::Eq(_, _) => Ok(ffi::ConstraintType_CT_EQ),
321
        Constraint::Difference(_, _) => Ok(ffi::ConstraintType_CT_DIFFERENCE),
322
        Constraint::Div(_, _) => Ok(ffi::ConstraintType_CT_DIV),
323
2772
        Constraint::DivUndefZero(_, _) => Ok(ffi::ConstraintType_CT_DIV_UNDEFZERO),
324
        Constraint::Modulo(_, _) => Ok(ffi::ConstraintType_CT_MODULO),
325
1512
        Constraint::ModuloUndefZero(_, _) => Ok(ffi::ConstraintType_CT_MODULO_UNDEFZERO),
326
1092
        Constraint::Pow(_, _) => Ok(ffi::ConstraintType_CT_POW),
327
1512
        Constraint::Product(_, _) => Ok(ffi::ConstraintType_CT_PRODUCT2),
328
4284
        Constraint::WeightedSumGeq(_, _, _) => Ok(ffi::ConstraintType_CT_WEIGHTGEQSUM),
329
4200
        Constraint::WeightedSumLeq(_, _, _) => Ok(ffi::ConstraintType_CT_WEIGHTLEQSUM),
330
        Constraint::CheckAssign(_) => Ok(ffi::ConstraintType_CT_CHECK_ASSIGN),
331
        Constraint::CheckGsa(_) => Ok(ffi::ConstraintType_CT_CHECK_GSA),
332
        Constraint::ForwardChecking(_) => Ok(ffi::ConstraintType_CT_FORWARD_CHECKING),
333
10416
        Constraint::Reify(_, _) => Ok(ffi::ConstraintType_CT_REIFY),
334
3276
        Constraint::ReifyImply(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY),
335
        Constraint::ReifyImplyQuick(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY_QUICK),
336
2184
        Constraint::WatchedAnd(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_AND),
337
5712
        Constraint::WatchedOr(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_OR),
338
        Constraint::GacAllDiff(_) => Ok(ffi::ConstraintType_CT_GACALLDIFF),
339
1848
        Constraint::AllDiff(_) => Ok(ffi::ConstraintType_CT_ALLDIFF),
340
        Constraint::AllDiffMatrix(_, _) => Ok(ffi::ConstraintType_CT_ALLDIFFMATRIX),
341
        Constraint::WatchSumGeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_GEQSUM),
342
        Constraint::WatchSumLeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LEQSUM),
343
        Constraint::OccurrenceGeq(_, _, _) => Ok(ffi::ConstraintType_CT_GEQ_OCCURRENCE),
344
        Constraint::OccurrenceLeq(_, _, _) => Ok(ffi::ConstraintType_CT_LEQ_OCCURRENCE),
345
        Constraint::Occurrence(_, _, _) => Ok(ffi::ConstraintType_CT_OCCURRENCE),
346
        Constraint::LitSumGeq(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_LITSUM),
347
        Constraint::Gcc(_, _, _) => Ok(ffi::ConstraintType_CT_GCC),
348
        Constraint::GccWeak(_, _, _) => Ok(ffi::ConstraintType_CT_GCCWEAK),
349
        Constraint::LexLeqRv(_, _) => Ok(ffi::ConstraintType_CT_GACLEXLEQ),
350
336
        Constraint::LexLeq(_, _) => Ok(ffi::ConstraintType_CT_LEXLEQ),
351
168
        Constraint::LexLess(_, _) => Ok(ffi::ConstraintType_CT_LEXLESS),
352
        Constraint::LexLeqQuick(_, _) => Ok(ffi::ConstraintType_CT_QUICK_LEXLEQ),
353
        Constraint::LexLessQuick(_, _) => Ok(ffi::ConstraintType_CT_QUICK_LEXLEQ),
354
        Constraint::WatchVecNeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_VECNEQ),
355
        Constraint::WatchVecExistsLess(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_VEC_OR_LESS),
356
        Constraint::Hamming(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_HAMMING),
357
        Constraint::NotHamming(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_HAMMING),
358
        Constraint::FrameUpdate(_, _, _, _, _) => Ok(ffi::ConstraintType_CT_FRAMEUPDATE),
359
84
        Constraint::NegativeTable(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NEGATIVE_TABLE),
360
252
        Constraint::Table(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_TABLE),
361
        Constraint::GacSchema(_, _) => Ok(ffi::ConstraintType_CT_GACSCHEMA),
362
        Constraint::LightTable(_, _) => Ok(ffi::ConstraintType_CT_LIGHTTABLE),
363
        Constraint::Mddc(_, _) => Ok(ffi::ConstraintType_CT_MDDC),
364
        Constraint::NegativeMddc(_, _) => Ok(ffi::ConstraintType_CT_NEGATIVEMDDC),
365
        Constraint::Str2Plus(_, _) => Ok(ffi::ConstraintType_CT_STR),
366
        Constraint::Max(_, _) => Ok(ffi::ConstraintType_CT_MAX),
367
        Constraint::Min(_, _) => Ok(ffi::ConstraintType_CT_MIN),
368
        Constraint::NvalueGeq(_, _) => Ok(ffi::ConstraintType_CT_GEQNVALUE),
369
        Constraint::NvalueLeq(_, _) => Ok(ffi::ConstraintType_CT_LEQNVALUE),
370
        Constraint::Element(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT),
371
7896
        Constraint::ElementOne(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT_ONE),
372
        Constraint::ElementUndefZero(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT_UNDEFZERO),
373
        Constraint::WatchElement(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT),
374
        Constraint::WatchElementOne(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_ONE),
375
        Constraint::WatchElementOneUndefZero(_, _, _) => {
376
            Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_ONE_UNDEFZERO)
377
        }
378
        Constraint::WatchElementUndefZero(_, _, _) => {
379
            Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_UNDEFZERO)
380
        }
381
8232
        Constraint::WLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LIT),
382
        Constraint::WNotLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOTLIT),
383
336
        Constraint::WInIntervalSet(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_ININTERVALSET),
384
        Constraint::WInRange(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_INRANGE),
385
1848
        Constraint::WInset(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_INSET),
386
        Constraint::WNotInRange(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_INRANGE),
387
        Constraint::WNotInset(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_INSET),
388
840
        Constraint::Abs(_, _) => Ok(ffi::ConstraintType_CT_ABS),
389
11172
        Constraint::DisEq(_, _) => Ok(ffi::ConstraintType_CT_DISEQ),
390
868
        Constraint::MinusEq(_, _) => Ok(ffi::ConstraintType_CT_MINUSEQ),
391
        Constraint::GacEq(_, _) => Ok(ffi::ConstraintType_CT_GACEQ),
392
        Constraint::WatchLess(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LESS),
393
        Constraint::WatchNeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NEQ),
394
4122
        Constraint::True => Ok(ffi::ConstraintType_CT_TRUE),
395
504
        Constraint::False => Ok(ffi::ConstraintType_CT_FALSE),
396

            
397
        #[allow(unreachable_patterns)]
398
        x => Err(MinionError::NotImplemented(format!(
399
            "Constraint not implemented {x:?}",
400
        ))),
401
    }
402
148434
}
403

            
404
148434
unsafe fn constraint_add_args(
405
148434
    i: *mut ffi::ProbSpec_CSPInstance,
406
148434
    r_constr: *mut ffi::ProbSpec_ConstraintBlob,
407
148434
    constr: &Constraint,
408
148434
) -> Result<(), MinionError> {
409
148434
    match constr {
410
17612
        Constraint::SumGeq(lhs_vars, rhs_var) => {
411
17612
            read_list(i, r_constr, lhs_vars)?;
412
17612
            read_var(i, r_constr, rhs_var)?;
413
17612
            Ok(())
414
        }
415
17276
        Constraint::SumLeq(lhs_vars, rhs_var) => {
416
17276
            read_list(i, r_constr, lhs_vars)?;
417
17276
            read_var(i, r_constr, rhs_var)?;
418
17276
            Ok(())
419
        }
420
21560
        Constraint::Ineq(var1, var2, c) => {
421
21560
            read_var(i, r_constr, var1)?;
422
21560
            read_var(i, r_constr, var2)?;
423
21560
            read_constant(r_constr, c)?;
424
21560
            Ok(())
425
        }
426
16520
        Constraint::Eq(var1, var2) => {
427
16520
            read_var(i, r_constr, var1)?;
428
16520
            read_var(i, r_constr, var2)?;
429
16520
            Ok(())
430
        }
431
        Constraint::Difference((a, b), c) => {
432
            read_2_vars(i, r_constr, a, b)?;
433
            read_var(i, r_constr, c)?;
434
            Ok(())
435
        }
436
        Constraint::Div((a, b), c) => {
437
            read_2_vars(i, r_constr, a, b)?;
438
            read_var(i, r_constr, c)?;
439
            Ok(())
440
        }
441
2772
        Constraint::DivUndefZero((a, b), c) => {
442
2772
            read_2_vars(i, r_constr, a, b)?;
443
2772
            read_var(i, r_constr, c)?;
444
2772
            Ok(())
445
        }
446
        Constraint::Modulo((a, b), c) => {
447
            read_2_vars(i, r_constr, a, b)?;
448
            read_var(i, r_constr, c)?;
449
            Ok(())
450
        }
451
1512
        Constraint::ModuloUndefZero((a, b), c) => {
452
1512
            read_2_vars(i, r_constr, a, b)?;
453
1512
            read_var(i, r_constr, c)?;
454
1512
            Ok(())
455
        }
456
1092
        Constraint::Pow((a, b), c) => {
457
1092
            read_2_vars(i, r_constr, a, b)?;
458
1092
            read_var(i, r_constr, c)?;
459
1092
            Ok(())
460
        }
461
1512
        Constraint::Product((a, b), c) => {
462
1512
            read_2_vars(i, r_constr, a, b)?;
463
1512
            read_var(i, r_constr, c)?;
464
1512
            Ok(())
465
        }
466
4284
        Constraint::WeightedSumGeq(a, b, c) => {
467
4284
            read_constant_list(r_constr, a)?;
468
4284
            read_list(i, r_constr, b)?;
469
4284
            read_var(i, r_constr, c)?;
470
4284
            Ok(())
471
        }
472
4200
        Constraint::WeightedSumLeq(a, b, c) => {
473
4200
            read_constant_list(r_constr, a)?;
474
4200
            read_list(i, r_constr, b)?;
475
4200
            read_var(i, r_constr, c)?;
476
4200
            Ok(())
477
        }
478
        Constraint::CheckAssign(a) => {
479
            read_constraint(i, r_constr, (**a).clone())?;
480
            Ok(())
481
        }
482
        Constraint::CheckGsa(a) => {
483
            read_constraint(i, r_constr, (**a).clone())?;
484
            Ok(())
485
        }
486
        Constraint::ForwardChecking(a) => {
487
            read_constraint(i, r_constr, (**a).clone())?;
488
            Ok(())
489
        }
490
10416
        Constraint::Reify(a, b) => {
491
10416
            read_constraint(i, r_constr, (**a).clone())?;
492
10416
            read_var(i, r_constr, b)?;
493
10416
            Ok(())
494
        }
495
3276
        Constraint::ReifyImply(a, b) => {
496
3276
            read_constraint(i, r_constr, (**a).clone())?;
497
3276
            read_var(i, r_constr, b)?;
498
3276
            Ok(())
499
        }
500
        Constraint::ReifyImplyQuick(a, b) => {
501
            read_constraint(i, r_constr, (**a).clone())?;
502
            read_var(i, r_constr, b)?;
503
            Ok(())
504
        }
505
2184
        Constraint::WatchedAnd(a) => {
506
2184
            read_constraint_list(i, r_constr, a)?;
507
2184
            Ok(())
508
        }
509
5712
        Constraint::WatchedOr(a) => {
510
5712
            read_constraint_list(i, r_constr, a)?;
511
5712
            Ok(())
512
        }
513
        Constraint::GacAllDiff(a) => {
514
            read_list(i, r_constr, a)?;
515
            Ok(())
516
        }
517
1848
        Constraint::AllDiff(a) => {
518
1848
            read_list(i, r_constr, a)?;
519
1848
            Ok(())
520
        }
521
        Constraint::AllDiffMatrix(a, b) => {
522
            read_list(i, r_constr, a)?;
523
            read_constant(r_constr, b)?;
524
            Ok(())
525
        }
526
        Constraint::WatchSumGeq(a, b) => {
527
            read_list(i, r_constr, a)?;
528
            read_constant(r_constr, b)?;
529
            Ok(())
530
        }
531
        Constraint::WatchSumLeq(a, b) => {
532
            read_list(i, r_constr, a)?;
533
            read_constant(r_constr, b)?;
534
            Ok(())
535
        }
536
        Constraint::OccurrenceGeq(a, b, c) => {
537
            read_list(i, r_constr, a)?;
538
            read_constant(r_constr, b)?;
539
            read_constant(r_constr, c)?;
540
            Ok(())
541
        }
542
        Constraint::OccurrenceLeq(a, b, c) => {
543
            read_list(i, r_constr, a)?;
544
            read_constant(r_constr, b)?;
545
            read_constant(r_constr, c)?;
546
            Ok(())
547
        }
548
        Constraint::Occurrence(a, b, c) => {
549
            read_list(i, r_constr, a)?;
550
            read_constant(r_constr, b)?;
551
            read_var(i, r_constr, c)?;
552
            Ok(())
553
        }
554
168
        Constraint::LexLess(a, b) => {
555
168
            read_list(i, r_constr, a)?;
556
168
            read_list(i, r_constr, b)?;
557
168
            Ok(())
558
        }
559
336
        Constraint::LexLeq(a, b) => {
560
336
            read_list(i, r_constr, a)?;
561
336
            read_list(i, r_constr, b)?;
562
336
            Ok(())
563
        }
564
        //Constraint::LitSumGeq(_, _, _) => todo!(),
565
        //Constraint::Gcc(_, _, _) => todo!(),
566
        //Constraint::GccWeak(_, _, _) => todo!(),
567
        //Constraint::LexLeqRv(_, _) => todo!(),
568
        //Constraint::LexLeqQuick(_, _) => todo!(),
569
        //Constraint::LexLessQuick(_, _) => todo!(),
570
        //Constraint::WatchVecNeq(_, _) => todo!(),
571
        //Constraint::WatchVecExistsLess(_, _) => todo!(),
572
        //Constraint::Hamming(_, _, _) => todo!(),
573
        //Constraint::NotHamming(_, _, _) => todo!(),
574
        //Constraint::FrameUpdate(_, _, _, _, _) => todo!(),
575
252
        Constraint::NegativeTable(vars, tuple_list) | Constraint::Table(vars, tuple_list) => {
576
336
            read_list(i, r_constr, vars)?;
577
336
            read_tuple_list(r_constr, tuple_list)?;
578
336
            Ok(())
579
        }
580
        //Constraint::GacSchema(_, _) => todo!(),
581
        //Constraint::LightTable(_, _) => todo!(),
582
        //Constraint::Mddc(_, _) => todo!(),
583
        //Constraint::NegativeMddc(_, _) => todo!(),
584
        //Constraint::Str2Plus(_, _) => todo!(),
585
        //Constraint::Max(_, _) => todo!(),
586
        //Constraint::Min(_, _) => todo!(),
587
        //Constraint::NvalueGeq(_, _) => todo!(),
588
        //Constraint::NvalueLeq(_, _) => todo!(),
589
        //Constraint::Element(_, _, _) => todo!(),
590
        //Constraint::ElementUndefZero(_, _, _) => todo!(),
591
        //Constraint::WatchElement(_, _, _) => todo!(),
592
        //Constraint::WatchElementOne(_, _, _) => todo!(),
593
7896
        Constraint::ElementOne(vec, j, e) => {
594
7896
            read_list(i, r_constr, vec)?;
595
7896
            read_var(i, r_constr, j)?;
596
7896
            read_var(i, r_constr, e)?;
597
7896
            Ok(())
598
        }
599
        //Constraint::WatchElementOneUndefZero(_, _, _) => todo!(),
600
        //Constraint::WatchElementUndefZero(_, _, _) => todo!(),
601
8232
        Constraint::WLiteral(a, b) => {
602
8232
            read_var(i, r_constr, a)?;
603
8232
            read_constant(r_constr, b)?;
604
8232
            Ok(())
605
        }
606
        //Constraint::WNotLiteral(_, _) => todo!(),
607
336
        Constraint::WInIntervalSet(var, consts) => {
608
336
            read_var(i, r_constr, var)?;
609
336
            read_constant_list(r_constr, consts)?;
610
336
            Ok(())
611
        }
612
        //Constraint::WInRange(_, _) => todo!(),
613
1848
        Constraint::WInset(a, b) => {
614
1848
            read_var(i, r_constr, a)?;
615
1848
            read_constant_list(r_constr, b)?;
616
1848
            Ok(())
617
        }
618
        //Constraint::WNotInRange(_, _) => todo!(),
619
        //Constraint::WNotInset(_, _) => todo!(),
620
840
        Constraint::Abs(a, b) => {
621
840
            read_var(i, r_constr, a)?;
622
840
            read_var(i, r_constr, b)?;
623
840
            Ok(())
624
        }
625
11172
        Constraint::DisEq(a, b) => {
626
11172
            read_var(i, r_constr, a)?;
627
11172
            read_var(i, r_constr, b)?;
628
11172
            Ok(())
629
        }
630
868
        Constraint::MinusEq(a, b) => {
631
868
            read_var(i, r_constr, a)?;
632
868
            read_var(i, r_constr, b)?;
633
868
            Ok(())
634
        }
635
        //Constraint::GacEq(_, _) => todo!(),
636
        //Constraint::WatchLess(_, _) => todo!(),
637
        // TODO: ensure that this is a bool?
638
        Constraint::WatchNeq(a, b) => {
639
            read_var(i, r_constr, a)?;
640
            read_var(i, r_constr, b)?;
641
            Ok(())
642
        }
643

            
644
4122
        Constraint::True => Ok(()),
645
504
        Constraint::False => Ok(()),
646
        #[allow(unreachable_patterns)]
647
        x => Err(MinionError::NotImplemented(format!("{x:?}"))),
648
    }
649
148434
}
650

            
651
// DO NOT call manually - this assumes that all needed vars are already in the symbol table.
652
// TODO not happy with this just assuming the name is in the symbol table
653
54460
unsafe fn read_list(
654
54460
    instance: *mut ffi::ProbSpec_CSPInstance,
655
54460
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
656
54460
    vars: &Vec<Var>,
657
54460
) -> Result<(), MinionError> {
658
54460
    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
659
156436
    for var in vars {
660
156436
        let raw_var = match var {
661
125020
            Var::NameRef(name) => {
662
125020
                let c_str = CString::new(name.clone()).map_err(|_| {
663
                    anyhow!(
664
                        "Variable name {:?} contains a null character.",
665
                        name.clone()
666
                    )
667
                })?;
668
125020
                ffi::getVarByName(instance, c_str.as_ptr() as _)
669
            }
670
31416
            Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
671
        };
672

            
673
156436
        ffi::vec_var_push_back(raw_vars.ptr, raw_var);
674
    }
675

            
676
54460
    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
677

            
678
54460
    Ok(())
679
54460
}
680

            
681
192080
unsafe fn read_var(
682
192080
    instance: *mut ffi::ProbSpec_CSPInstance,
683
192080
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
684
192080
    var: &Var,
685
192080
) -> Result<(), MinionError> {
686
192080
    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
687
192080
    let raw_var = match var {
688
143864
        Var::NameRef(name) => {
689
143864
            let c_str = CString::new(name.clone()).map_err(|_| {
690
                anyhow!(
691
                    "Variable name {:?} contains a null character.",
692
                    name.clone()
693
                )
694
            })?;
695
143864
            ffi::getVarByName(instance, c_str.as_ptr() as _)
696
        }
697
48216
        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
698
    };
699

            
700
192080
    ffi::vec_var_push_back(raw_vars.ptr, raw_var);
701
192080
    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
702

            
703
192080
    Ok(())
704
192080
}
705

            
706
6888
unsafe fn read_2_vars(
707
6888
    instance: *mut ffi::ProbSpec_CSPInstance,
708
6888
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
709
6888
    var1: &Var,
710
6888
    var2: &Var,
711
6888
) -> Result<(), MinionError> {
712
6888
    let mut raw_var = match var1 {
713
6720
        Var::NameRef(name) => {
714
6720
            let c_str = CString::new(name.clone()).map_err(|_| {
715
                anyhow!(
716
                    "Variable name {:?} contains a null character.",
717
                    name.clone()
718
                )
719
            })?;
720
6720
            ffi::getVarByName(instance, c_str.as_ptr() as _)
721
        }
722
168
        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
723
    };
724
6888
    let mut raw_var2 = match var2 {
725
5208
        Var::NameRef(name) => {
726
5208
            let c_str = CString::new(name.clone()).map_err(|_| {
727
                anyhow!(
728
                    "Variable name {:?} contains a null character.",
729
                    name.clone()
730
                )
731
            })?;
732
5208
            ffi::getVarByName(instance, c_str.as_ptr() as _)
733
        }
734
1680
        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
735
    };
736
    // todo: does this move or copy? I am confus!
737
    // TODO need to mkae the semantics of move vs copy / ownership clear in libminion!!
738
    // This shouldve leaked everywhere by now but i think libminion copies stuff??
739
6888
    ffi::constraint_addTwoVars(raw_constraint, &mut raw_var, &mut raw_var2);
740
6888
    Ok(())
741
6888
}
742

            
743
29792
unsafe fn read_constant(
744
29792
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
745
29792
    constant: &Constant,
746
29792
) -> Result<(), MinionError> {
747
29792
    let val: i32 = match constant {
748
29792
        Constant::Integer(n) => Ok(*n),
749
        Constant::Bool(true) => Ok(1),
750
        Constant::Bool(false) => Ok(0),
751
        x => Err(MinionError::NotImplemented(format!("{x:?}"))),
752
    }?;
753

            
754
29792
    ffi::constraint_addConstant(raw_constraint, val);
755

            
756
29792
    Ok(())
757
29792
}
758

            
759
10668
unsafe fn read_constant_list(
760
10668
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
761
10668
    constants: &[Constant],
762
10668
) -> Result<(), MinionError> {
763
10668
    let raw_consts = Scoped::new(ffi::vec_int_new(), |x| ffi::vec_int_free(x as _));
764

            
765
41832
    for constant in constants.iter() {
766
41832
        let val = match constant {
767
41664
            Constant::Integer(n) => Ok(*n),
768
84
            Constant::Bool(true) => Ok(1),
769
84
            Constant::Bool(false) => Ok(0),
770
            #[allow(unreachable_patterns)] // TODO: can there be other types?
771
            x => Err(MinionError::NotImplemented(format!("{x:?}"))),
772
        }?;
773

            
774
41832
        ffi::vec_int_push_back(raw_consts.ptr, val);
775
    }
776

            
777
10668
    ffi::constraint_addConstantList(raw_constraint, raw_consts.ptr);
778
10668
    Ok(())
779
10668
}
780

            
781
//TODO: check if the inner constraint is listed in the model or not?
782
//Does this matter?
783
// TODO: type-check inner constraints vars and tuples and so on?
784
13692
unsafe fn read_constraint(
785
13692
    instance: *mut ffi::ProbSpec_CSPInstance,
786
13692
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
787
13692
    inner_constraint: Constraint,
788
13692
) -> Result<(), MinionError> {
789
13692
    let constraint_type = get_constraint_type(&inner_constraint)?;
790
13692
    let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
791
13692
        ffi::constraint_free(x as _)
792
13692
    });
793

            
794
13692
    constraint_add_args(instance, raw_inner_constraint.ptr, &inner_constraint)?;
795

            
796
13692
    ffi::constraint_addConstraint(raw_constraint, raw_inner_constraint.ptr);
797
13692
    Ok(())
798
13692
}
799

            
800
7896
unsafe fn read_constraint_list(
801
7896
    instance: *mut ffi::ProbSpec_CSPInstance,
802
7896
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
803
7896
    inner_constraints: &[Constraint],
804
7896
) -> Result<(), MinionError> {
805
7896
    let raw_inners = Scoped::new(ffi::vec_constraints_new(), |x| {
806
7896
        ffi::vec_constraints_free(x as _)
807
7896
    });
808
17640
    for inner_constraint in inner_constraints.iter() {
809
17640
        let constraint_type = get_constraint_type(inner_constraint)?;
810
17640
        let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
811
17640
            ffi::constraint_free(x as _)
812
17640
        });
813

            
814
17640
        constraint_add_args(instance, raw_inner_constraint.ptr, inner_constraint)?;
815
17640
        ffi::vec_constraints_push_back(raw_inners.ptr, raw_inner_constraint.ptr);
816
    }
817

            
818
7896
    ffi::constraint_addConstraintList(raw_constraint, raw_inners.ptr);
819
7896
    Ok(())
820
7896
}
821

            
822
336
unsafe fn read_tuple_list(
823
336
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
824
336
    tuples: &Vec<Tuple>,
825
336
) -> Result<(), MinionError> {
826
    // a tuple list is just a vec<vec<int>>, where each inner vec is a tuple
827
336
    let raw_tuples = Scoped::new(ffi::vec_vec_int_new(), |x| ffi::vec_vec_int_free(x as _));
828
868
    for tuple in tuples {
829
868
        let raw_tuple = Scoped::new(ffi::vec_int_new(), |x| ffi::vec_int_free(x as _));
830
2436
        for constant in tuple.iter() {
831
2436
            let val = match constant {
832
2436
                Constant::Integer(n) => Ok(*n),
833
                Constant::Bool(true) => Ok(1),
834
                Constant::Bool(false) => Ok(0),
835
                #[allow(unreachable_patterns)] // TODO: can there be other types?
836
                x => Err(MinionError::NotImplemented(format!("{:?}", x))),
837
            }?;
838

            
839
2436
            ffi::vec_int_push_back(raw_tuple.ptr, val);
840
        }
841

            
842
868
        ffi::vec_vec_int_push_back_ptr(raw_tuples.ptr, raw_tuple.ptr);
843
    }
844

            
845
    // `constraint_setTuples` transfers ownership of `TupleList` into Minion via shared_ptr.
846
    // Do not wrap this pointer in `Scoped` or it will be freed too early.
847
336
    let raw_tuple_list = ffi::tupleList_new(raw_tuples.ptr);
848
336
    ffi::constraint_setTuples(raw_constraint, raw_tuple_list);
849

            
850
336
    Ok(())
851
336
}