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::ffi::{self};
14
use crate::{
15
    ast::{Constant, Constraint, Model, Var, VarDomain, VarName},
16
    error::{MinionError, RuntimeError},
17
    scoped_ptr::Scoped,
18
};
19

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

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

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

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

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

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

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

            
132
150860
    if guard.is_none() {
133
        return true;
134
150860
    }
135

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

            
141
150860
    if print_vars.is_empty() {
142
468
        return true;
143
150392
    }
144

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

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

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

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

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

            
175
7284
    *_lock_guard = true;
176

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

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

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

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

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

            
199
7284
        condvar.notify_one();
200

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

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

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

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

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

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

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

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

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

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

            
262
22702
        ffi::printMatrix_addVar(instance, var);
263

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

            
267
        #[allow(clippy::unwrap_used)]
268
22702
        (*print_vars_guard).as_mut().unwrap().push(var_name.clone());
269
    }
270

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

            
283
7284
    let search_order = Scoped::new(
284
7284
        ffi::searchOrder_new(search_vars.ptr, ffi::VarOrderEnum_ORDER_STATIC, false),
285
7284
        |x| ffi::searchOrder_free(x as _),
286
    );
287

            
288
7284
    ffi::instance_addSearchOrder(instance, search_order.ptr);
289

            
290
    /*********************************/
291
    /*        Add constraints        */
292
    /*********************************/
293

            
294
21220
    for constraint in &model.constraints {
295
        // 1. get constraint type and create C++ constraint object
296
        // 2. run through arguments and add them to the constraint
297
        // 3. add constraint to instance
298

            
299
21220
        let constraint_type = get_constraint_type(constraint)?;
300
21220
        let raw_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
301
21220
            ffi::constraint_free(x as _)
302
21220
        });
303

            
304
21220
        constraint_add_args(instance, raw_constraint.ptr, constraint)?;
305
21220
        ffi::instance_addConstraint(instance, raw_constraint.ptr);
306
    }
307

            
308
7284
    Ok(())
309
7284
}
310

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

            
393
        #[allow(unreachable_patterns)]
394
        x => Err(MinionError::NotImplemented(format!(
395
            "Constraint not implemented {x:?}",
396
        ))),
397
    }
398
28110
}
399

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

            
637
940
        Constraint::True => Ok(()),
638
156
        Constraint::False => Ok(()),
639
        #[allow(unreachable_patterns)]
640
        x => Err(MinionError::NotImplemented(format!("{x:?}"))),
641
    }
642
28110
}
643

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

            
666
19240
        ffi::vec_var_push_back(raw_vars.ptr, raw_var);
667
    }
668

            
669
7644
    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
670

            
671
7644
    Ok(())
672
7644
}
673

            
674
34788
unsafe fn read_var(
675
34788
    instance: *mut ffi::ProbSpec_CSPInstance,
676
34788
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
677
34788
    var: &Var,
678
34788
) -> Result<(), MinionError> {
679
34788
    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
680
34788
    let raw_var = match var {
681
25532
        Var::NameRef(name) => {
682
25532
            let c_str = CString::new(name.clone()).map_err(|_| {
683
                anyhow!(
684
                    "Variable name {:?} contains a null character.",
685
                    name.clone()
686
                )
687
            })?;
688
25532
            ffi::getVarByName(instance, c_str.as_ptr() as _)
689
        }
690
9256
        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
691
    };
692

            
693
34788
    ffi::vec_var_push_back(raw_vars.ptr, raw_var);
694
34788
    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
695

            
696
34788
    Ok(())
697
34788
}
698

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

            
736
6006
unsafe fn read_constant(
737
6006
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
738
6006
    constant: &Constant,
739
6006
) -> Result<(), MinionError> {
740
6006
    let val: i32 = match constant {
741
6006
        Constant::Integer(n) => Ok(*n),
742
        Constant::Bool(true) => Ok(1),
743
        Constant::Bool(false) => Ok(0),
744
        x => Err(MinionError::NotImplemented(format!("{x:?}"))),
745
    }?;
746

            
747
6006
    ffi::constraint_addConstant(raw_constraint, val);
748

            
749
6006
    Ok(())
750
6006
}
751

            
752
1508
unsafe fn read_constant_list(
753
1508
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
754
1508
    constants: &[Constant],
755
1508
) -> Result<(), MinionError> {
756
1508
    let raw_consts = Scoped::new(ffi::vec_int_new(), |x| ffi::vec_var_free(x as _));
757

            
758
9516
    for constant in constants.iter() {
759
9516
        let val = match constant {
760
9464
            Constant::Integer(n) => Ok(*n),
761
26
            Constant::Bool(true) => Ok(1),
762
26
            Constant::Bool(false) => Ok(0),
763
            #[allow(unreachable_patterns)] // TODO: can there be other types?
764
            x => Err(MinionError::NotImplemented(format!("{x:?}"))),
765
        }?;
766

            
767
9516
        ffi::vec_int_push_back(raw_consts.ptr, val);
768
    }
769

            
770
1508
    ffi::constraint_addConstantList(raw_constraint, raw_consts.ptr);
771
1508
    Ok(())
772
1508
}
773

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

            
787
2600
    constraint_add_args(instance, raw_inner_constraint.ptr, &inner_constraint)?;
788

            
789
2600
    ffi::constraint_addConstraint(raw_constraint, raw_inner_constraint.ptr);
790
2600
    Ok(())
791
2600
}
792

            
793
1846
unsafe fn read_constraint_list(
794
1846
    instance: *mut ffi::ProbSpec_CSPInstance,
795
1846
    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
796
1846
    inner_constraints: &[Constraint],
797
1846
) -> Result<(), MinionError> {
798
1846
    let raw_inners = Scoped::new(ffi::vec_constraints_new(), |x| {
799
1846
        ffi::vec_constraints_free(x as _)
800
1846
    });
801
4290
    for inner_constraint in inner_constraints.iter() {
802
4290
        let constraint_type = get_constraint_type(inner_constraint)?;
803
4290
        let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
804
4290
            ffi::constraint_free(x as _)
805
4290
        });
806

            
807
4290
        constraint_add_args(instance, raw_inner_constraint.ptr, inner_constraint)?;
808
4290
        ffi::vec_constraints_push_back(raw_inners.ptr, raw_inner_constraint.ptr);
809
    }
810

            
811
1846
    ffi::constraint_addConstraintList(raw_constraint, raw_inners.ptr);
812
1846
    Ok(())
813
1846
}