minion_rs/
run.rs

1#![allow(unreachable_patterns)]
2
3use std::{
4    collections::HashMap,
5    ffi::CString,
6    sync::Condvar,
7    sync::{Mutex, MutexGuard},
8};
9
10use anyhow::anyhow;
11
12use crate::ffi::{self};
13use 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///   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///       let mut guard = ALL_SOLUTIONS.lock().unwrap();
46///       guard.push(solutions);
47///       true
48///   }
49///    
50///   // Build and run the model.
51///   let mut model = Model::new();
52///
53///   // ... omitted for brevity ...
54/// # model
55/// #     .named_variables
56/// #     .add_var("x".to_owned(), VarDomain::Bound(1, 3));
57/// # model
58/// #     .named_variables
59/// #     .add_var("y".to_owned(), VarDomain::Bound(2, 4));
60/// # model
61/// #     .named_variables
62/// #     .add_var("z".to_owned(), VarDomain::Bound(1, 5));
63/// #
64/// # let leq = Constraint::SumLeq(
65/// #     vec![
66/// #         Var::NameRef("x".to_owned()),
67/// #         Var::NameRef("y".to_owned()),
68/// #         Var::NameRef("z".to_owned()),
69/// #     ],
70/// #     Var::ConstantAsVar(4),
71/// # );
72/// #
73/// # let geq = Constraint::SumGeq(
74/// #     vec![
75/// #         Var::NameRef("x".to_owned()),
76/// #         Var::NameRef("y".to_owned()),
77/// #         Var::NameRef("z".to_owned()),
78/// #     ],
79/// #     Var::ConstantAsVar(4),
80/// # );
81/// #
82/// # let ineq = Constraint::Ineq(
83/// #     Var::NameRef("x".to_owned()),
84/// #     Var::NameRef("y".to_owned()),
85/// #     Constant::Integer(-1),
86/// # );
87/// #
88/// # model.constraints.push(leq);
89/// # model.constraints.push(geq);
90/// # model.constraints.push(ineq);
91///  
92///   let res = run_minion(model, callback);
93///   res.expect("Error occurred");
94///
95///   // Get solutions
96///   let guard = ALL_SOLUTIONS.lock().unwrap();
97///   let solution_set_1 = &(guard.get(0).unwrap());
98///
99///   let x1 = solution_set_1.get("x").unwrap();
100///   let y1 = solution_set_1.get("y").unwrap();
101///   let z1 = solution_set_1.get("z").unwrap();
102/// #
103/// # // TODO: this test would be better with an example with >1 solution.
104/// # assert_eq!(guard.len(),1);
105/// # assert_eq!(*x1,Constant::Integer(1));
106/// # assert_eq!(*y1,Constant::Integer(2));
107/// # assert_eq!(*z1,Constant::Integer(1));
108/// ```
109pub 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
115static CALLBACK: Mutex<Option<Callback>> = Mutex::new(None);
116
117// the variables we want to return, and their ordering in the print matrix
118static PRINT_VARS: Mutex<Option<Vec<VarName>>> = Mutex::new(None);
119
120static LOCK: (Mutex<bool>, Condvar) = (Mutex::new(false), Condvar::new());
121
122#[no_mangle]
123unsafe extern "C" fn run_callback() -> bool {
124    // get printvars from static PRINT_VARS if they exist.
125    // if not, return true and continue search.
126
127    // Mutex poisoning is probably panic worthy.
128    #[allow(clippy::unwrap_used)]
129    let mut guard: MutexGuard<'_, Option<Vec<VarName>>> = PRINT_VARS.lock().unwrap();
130
131    if guard.is_none() {
132        return true;
133    }
134
135    let print_vars = match &mut *guard {
136        Some(x) => x,
137        None => unreachable!(),
138    };
139
140    if print_vars.is_empty() {
141        return true;
142    }
143
144    // build nice solutions view to be used by callback
145    let mut solutions: HashMap<VarName, Constant> = HashMap::new();
146
147    for (i, var) in print_vars.iter().enumerate() {
148        let solution_int: i32 = ffi::printMatrix_getValue(i as _);
149        let solution: Constant = Constant::Integer(solution_int);
150        solutions.insert(var.to_string(), solution);
151    }
152
153    #[allow(clippy::unwrap_used)]
154    match *CALLBACK.lock().unwrap() {
155        None => true,
156        Some(func) => func(solutions),
157    }
158}
159
160/// Run Minion on the given [Model].
161///
162/// The given [callback](Callback) is ran whenever a new solution set is found.
163// Turn it into a warning for this function, cant unwarn it directly above callback wierdness
164#[allow(clippy::unwrap_used)]
165pub fn run_minion(model: Model, callback: Callback) -> Result<(), MinionError> {
166    // Mutex poisoning is probably panic worthy.
167    *CALLBACK.lock().unwrap() = Some(callback);
168
169    let (lock, condvar) = &LOCK;
170    let mut _lock_guard = condvar
171        .wait_while(lock.lock().unwrap(), |locked| *locked)
172        .unwrap();
173
174    *_lock_guard = true;
175
176    unsafe {
177        // TODO: something better than a manual spinlock
178        let search_opts = ffi::searchOptions_new();
179        let search_method = ffi::searchMethod_new();
180        let search_instance = ffi::instance_new();
181
182        convert_model_to_raw(search_instance, &model)?;
183
184        let res = ffi::runMinion(
185            search_opts,
186            search_method,
187            search_instance,
188            Some(run_callback),
189        );
190
191        ffi::searchMethod_free(search_method);
192        ffi::searchOptions_free(search_opts);
193        ffi::instance_free(search_instance);
194
195        *_lock_guard = false;
196        std::mem::drop(_lock_guard);
197
198        condvar.notify_one();
199
200        match res {
201            0 => Ok(()),
202            x => Err(MinionError::from(RuntimeError::from(x))),
203        }
204    }
205}
206
207unsafe fn convert_model_to_raw(
208    instance: *mut ffi::ProbSpec_CSPInstance,
209    model: &Model,
210) -> Result<(), MinionError> {
211    /*******************************/
212    /*        Add variables        */
213    /*******************************/
214
215    /*
216     * Add variables to:
217     * 1. symbol table
218     * 2. print matrix
219     * 3. search vars
220     *
221     * These are all done in the order saved in the SymbolTable.
222     */
223
224    let search_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
225
226    // store variables and the order they will be returned inside rust for later use.
227    #[allow(clippy::unwrap_used)]
228    let mut print_vars_guard = PRINT_VARS.lock().unwrap();
229    *print_vars_guard = Some(vec![]);
230
231    for var_name in model.named_variables.get_variable_order() {
232        let c_str = CString::new(var_name.clone()).map_err(|_| {
233            anyhow!(
234                "Variable name {:?} contains a null character.",
235                var_name.clone()
236            )
237        })?;
238
239        let vartype = model
240            .named_variables
241            .get_vartype(var_name.clone())
242            .ok_or(anyhow!("Could not get var type for {:?}", var_name.clone()))?;
243
244        let (vartype_raw, domain_low, domain_high) = match vartype {
245            VarDomain::Bound(a, b) => Ok((ffi::VariableType_VAR_BOUND, a, b)),
246            VarDomain::Bool => Ok((ffi::VariableType_VAR_BOOL, 0, 1)), // TODO: will this work?
247            x => Err(MinionError::NotImplemented(format!("{:?}", x))),
248        }?;
249
250        ffi::newVar_ffi(
251            instance,
252            c_str.as_ptr() as _,
253            vartype_raw,
254            domain_low,
255            domain_high,
256        );
257
258        let var = ffi::getVarByName(instance, c_str.as_ptr() as _);
259
260        ffi::printMatrix_addVar(instance, var);
261
262        // add to the print vars stored in rust so to remember
263        // the order for callback function.
264
265        #[allow(clippy::unwrap_used)]
266        (*print_vars_guard).as_mut().unwrap().push(var_name.clone());
267
268        ffi::vec_var_push_back(search_vars.ptr, var);
269    }
270
271    let search_order = Scoped::new(
272        ffi::searchOrder_new(search_vars.ptr, ffi::VarOrderEnum_ORDER_STATIC, false),
273        |x| ffi::searchOrder_free(x as _),
274    );
275
276    ffi::instance_addSearchOrder(instance, search_order.ptr);
277
278    /*********************************/
279    /*        Add constraints        */
280    /*********************************/
281
282    for constraint in &model.constraints {
283        // 1. get constraint type and create C++ constraint object
284        // 2. run through arguments and add them to the constraint
285        // 3. add constraint to instance
286
287        let constraint_type = get_constraint_type(constraint)?;
288        let raw_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
289            ffi::constraint_free(x as _)
290        });
291
292        constraint_add_args(instance, raw_constraint.ptr, constraint)?;
293        ffi::instance_addConstraint(instance, raw_constraint.ptr);
294    }
295
296    Ok(())
297}
298
299unsafe fn get_constraint_type(constraint: &Constraint) -> Result<u32, MinionError> {
300    match constraint {
301        Constraint::SumGeq(_, _) => Ok(ffi::ConstraintType_CT_GEQSUM),
302        Constraint::SumLeq(_, _) => Ok(ffi::ConstraintType_CT_LEQSUM),
303        Constraint::Ineq(_, _, _) => Ok(ffi::ConstraintType_CT_INEQ),
304        Constraint::Eq(_, _) => Ok(ffi::ConstraintType_CT_EQ),
305        Constraint::Difference(_, _) => Ok(ffi::ConstraintType_CT_DIFFERENCE),
306        Constraint::Div(_, _) => Ok(ffi::ConstraintType_CT_DIV),
307        Constraint::DivUndefZero(_, _) => Ok(ffi::ConstraintType_CT_DIV_UNDEFZERO),
308        Constraint::Modulo(_, _) => Ok(ffi::ConstraintType_CT_MODULO),
309        Constraint::ModuloUndefZero(_, _) => Ok(ffi::ConstraintType_CT_MODULO_UNDEFZERO),
310        Constraint::Pow(_, _) => Ok(ffi::ConstraintType_CT_POW),
311        Constraint::Product(_, _) => Ok(ffi::ConstraintType_CT_PRODUCT2),
312        Constraint::WeightedSumGeq(_, _, _) => Ok(ffi::ConstraintType_CT_WEIGHTGEQSUM),
313        Constraint::WeightedSumLeq(_, _, _) => Ok(ffi::ConstraintType_CT_WEIGHTLEQSUM),
314        Constraint::CheckAssign(_) => Ok(ffi::ConstraintType_CT_CHECK_ASSIGN),
315        Constraint::CheckGsa(_) => Ok(ffi::ConstraintType_CT_CHECK_GSA),
316        Constraint::ForwardChecking(_) => Ok(ffi::ConstraintType_CT_FORWARD_CHECKING),
317        Constraint::Reify(_, _) => Ok(ffi::ConstraintType_CT_REIFY),
318        Constraint::ReifyImply(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY),
319        Constraint::ReifyImplyQuick(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY_QUICK),
320        Constraint::WatchedAnd(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_AND),
321        Constraint::WatchedOr(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_OR),
322        Constraint::GacAllDiff(_) => Ok(ffi::ConstraintType_CT_GACALLDIFF),
323        Constraint::AllDiff(_) => Ok(ffi::ConstraintType_CT_ALLDIFF),
324        Constraint::AllDiffMatrix(_, _) => Ok(ffi::ConstraintType_CT_ALLDIFFMATRIX),
325        Constraint::WatchSumGeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_GEQSUM),
326        Constraint::WatchSumLeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LEQSUM),
327        Constraint::OccurrenceGeq(_, _, _) => Ok(ffi::ConstraintType_CT_GEQ_OCCURRENCE),
328        Constraint::OccurrenceLeq(_, _, _) => Ok(ffi::ConstraintType_CT_LEQ_OCCURRENCE),
329        Constraint::Occurrence(_, _, _) => Ok(ffi::ConstraintType_CT_OCCURRENCE),
330        Constraint::LitSumGeq(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_LITSUM),
331        Constraint::Gcc(_, _, _) => Ok(ffi::ConstraintType_CT_GCC),
332        Constraint::GccWeak(_, _, _) => Ok(ffi::ConstraintType_CT_GCCWEAK),
333        Constraint::LexLeqRv(_, _) => Ok(ffi::ConstraintType_CT_GACLEXLEQ),
334        Constraint::LexLeq(_, _) => Ok(ffi::ConstraintType_CT_LEXLEQ),
335        Constraint::LexLess(_, _) => Ok(ffi::ConstraintType_CT_LEXLESS),
336        Constraint::LexLeqQuick(_, _) => Ok(ffi::ConstraintType_CT_QUICK_LEXLEQ),
337        Constraint::LexLessQuick(_, _) => Ok(ffi::ConstraintType_CT_QUICK_LEXLEQ),
338        Constraint::WatchVecNeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_VECNEQ),
339        Constraint::WatchVecExistsLess(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_VEC_OR_LESS),
340        Constraint::Hamming(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_HAMMING),
341        Constraint::NotHamming(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_HAMMING),
342        Constraint::FrameUpdate(_, _, _, _, _) => Ok(ffi::ConstraintType_CT_FRAMEUPDATE),
343        Constraint::NegativeTable(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NEGATIVE_TABLE),
344        Constraint::Table(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_TABLE),
345        Constraint::GacSchema(_, _) => Ok(ffi::ConstraintType_CT_GACSCHEMA),
346        Constraint::LightTable(_, _) => Ok(ffi::ConstraintType_CT_LIGHTTABLE),
347        Constraint::Mddc(_, _) => Ok(ffi::ConstraintType_CT_MDDC),
348        Constraint::NegativeMddc(_, _) => Ok(ffi::ConstraintType_CT_NEGATIVEMDDC),
349        Constraint::Str2Plus(_, _) => Ok(ffi::ConstraintType_CT_STR),
350        Constraint::Max(_, _) => Ok(ffi::ConstraintType_CT_MAX),
351        Constraint::Min(_, _) => Ok(ffi::ConstraintType_CT_MIN),
352        Constraint::NvalueGeq(_, _) => Ok(ffi::ConstraintType_CT_GEQNVALUE),
353        Constraint::NvalueLeq(_, _) => Ok(ffi::ConstraintType_CT_LEQNVALUE),
354        Constraint::Element(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT),
355        Constraint::ElementOne(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT_ONE),
356        Constraint::ElementUndefZero(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT_UNDEFZERO),
357        Constraint::WatchElement(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT),
358        Constraint::WatchElementOne(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_ONE),
359        Constraint::WatchElementOneUndefZero(_, _, _) => {
360            Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_ONE_UNDEFZERO)
361        }
362        Constraint::WatchElementUndefZero(_, _, _) => {
363            Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_UNDEFZERO)
364        }
365        Constraint::WLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LIT),
366        Constraint::WNotLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOTLIT),
367        Constraint::WInIntervalSet(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_ININTERVALSET),
368        Constraint::WInRange(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_INRANGE),
369        Constraint::WInset(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_INSET),
370        Constraint::WNotInRange(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_INRANGE),
371        Constraint::WNotInset(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_INSET),
372        Constraint::Abs(_, _) => Ok(ffi::ConstraintType_CT_ABS),
373        Constraint::DisEq(_, _) => Ok(ffi::ConstraintType_CT_DISEQ),
374        Constraint::MinusEq(_, _) => Ok(ffi::ConstraintType_CT_MINUSEQ),
375        Constraint::GacEq(_, _) => Ok(ffi::ConstraintType_CT_GACEQ),
376        Constraint::WatchLess(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LESS),
377        Constraint::WatchNeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NEQ),
378        Constraint::True => Ok(ffi::ConstraintType_CT_TRUE),
379        Constraint::False => Ok(ffi::ConstraintType_CT_FALSE),
380
381        #[allow(unreachable_patterns)]
382        x => Err(MinionError::NotImplemented(format!(
383            "Constraint not implemented {:?}",
384            x,
385        ))),
386    }
387}
388
389unsafe fn constraint_add_args(
390    i: *mut ffi::ProbSpec_CSPInstance,
391    r_constr: *mut ffi::ProbSpec_ConstraintBlob,
392    constr: &Constraint,
393) -> Result<(), MinionError> {
394    match constr {
395        Constraint::SumGeq(lhs_vars, rhs_var) => {
396            read_list(i, r_constr, lhs_vars)?;
397            read_var(i, r_constr, rhs_var)?;
398            Ok(())
399        }
400        Constraint::SumLeq(lhs_vars, rhs_var) => {
401            read_list(i, r_constr, lhs_vars)?;
402            read_var(i, r_constr, rhs_var)?;
403            Ok(())
404        }
405        Constraint::Ineq(var1, var2, c) => {
406            read_var(i, r_constr, var1)?;
407            read_var(i, r_constr, var2)?;
408            read_constant(r_constr, c)?;
409            Ok(())
410        }
411        Constraint::Eq(var1, var2) => {
412            read_var(i, r_constr, var1)?;
413            read_var(i, r_constr, var2)?;
414            Ok(())
415        }
416        Constraint::Difference((a, b), c) => {
417            read_2_vars(i, r_constr, a, b)?;
418            read_var(i, r_constr, c)?;
419            Ok(())
420        }
421        Constraint::Div((a, b), c) => {
422            read_2_vars(i, r_constr, a, b)?;
423            read_var(i, r_constr, c)?;
424            Ok(())
425        }
426        Constraint::DivUndefZero((a, b), c) => {
427            read_2_vars(i, r_constr, a, b)?;
428            read_var(i, r_constr, c)?;
429            Ok(())
430        }
431        Constraint::Modulo((a, b), c) => {
432            read_2_vars(i, r_constr, a, b)?;
433            read_var(i, r_constr, c)?;
434            Ok(())
435        }
436        Constraint::ModuloUndefZero((a, b), c) => {
437            read_2_vars(i, r_constr, a, b)?;
438            read_var(i, r_constr, c)?;
439            Ok(())
440        }
441        Constraint::Pow((a, b), c) => {
442            read_2_vars(i, r_constr, a, b)?;
443            read_var(i, r_constr, c)?;
444            Ok(())
445        }
446        Constraint::Product((a, b), c) => {
447            read_2_vars(i, r_constr, a, b)?;
448            read_var(i, r_constr, c)?;
449            Ok(())
450        }
451        Constraint::WeightedSumGeq(a, b, c) => {
452            read_constant_list(r_constr, a)?;
453            read_list(i, r_constr, b)?;
454            read_var(i, r_constr, c)?;
455            Ok(())
456        }
457        Constraint::WeightedSumLeq(a, b, c) => {
458            read_constant_list(r_constr, a)?;
459            read_list(i, r_constr, b)?;
460            read_var(i, r_constr, c)?;
461            Ok(())
462        }
463        Constraint::CheckAssign(a) => {
464            read_constraint(i, r_constr, (**a).clone())?;
465            Ok(())
466        }
467        Constraint::CheckGsa(a) => {
468            read_constraint(i, r_constr, (**a).clone())?;
469            Ok(())
470        }
471        Constraint::ForwardChecking(a) => {
472            read_constraint(i, r_constr, (**a).clone())?;
473            Ok(())
474        }
475        Constraint::Reify(a, b) => {
476            read_constraint(i, r_constr, (**a).clone())?;
477            read_var(i, r_constr, b)?;
478            Ok(())
479        }
480        Constraint::ReifyImply(a, b) => {
481            read_constraint(i, r_constr, (**a).clone())?;
482            read_var(i, r_constr, b)?;
483            Ok(())
484        }
485        Constraint::ReifyImplyQuick(a, b) => {
486            read_constraint(i, r_constr, (**a).clone())?;
487            read_var(i, r_constr, b)?;
488            Ok(())
489        }
490        Constraint::WatchedAnd(a) => {
491            read_constraint_list(i, r_constr, a)?;
492            Ok(())
493        }
494        Constraint::WatchedOr(a) => {
495            read_constraint_list(i, r_constr, a)?;
496            Ok(())
497        }
498        Constraint::GacAllDiff(a) => {
499            read_list(i, r_constr, a)?;
500            Ok(())
501        }
502        Constraint::AllDiff(a) => {
503            read_list(i, r_constr, a)?;
504            Ok(())
505        }
506        Constraint::AllDiffMatrix(a, b) => {
507            read_list(i, r_constr, a)?;
508            read_constant(r_constr, b)?;
509            Ok(())
510        }
511        Constraint::WatchSumGeq(a, b) => {
512            read_list(i, r_constr, a)?;
513            read_constant(r_constr, b)?;
514            Ok(())
515        }
516        Constraint::WatchSumLeq(a, b) => {
517            read_list(i, r_constr, a)?;
518            read_constant(r_constr, b)?;
519            Ok(())
520        }
521        Constraint::OccurrenceGeq(a, b, c) => {
522            read_list(i, r_constr, a)?;
523            read_constant(r_constr, b)?;
524            read_constant(r_constr, c)?;
525            Ok(())
526        }
527        Constraint::OccurrenceLeq(a, b, c) => {
528            read_list(i, r_constr, a)?;
529            read_constant(r_constr, b)?;
530            read_constant(r_constr, c)?;
531            Ok(())
532        }
533        Constraint::Occurrence(a, b, c) => {
534            read_list(i, r_constr, a)?;
535            read_constant(r_constr, b)?;
536            read_var(i, r_constr, c)?;
537            Ok(())
538        }
539        //Constraint::LitSumGeq(_, _, _) => todo!(),
540        //Constraint::Gcc(_, _, _) => todo!(),
541        //Constraint::GccWeak(_, _, _) => todo!(),
542        //Constraint::LexLeqRv(_, _) => todo!(),
543        //Constraint::LexLeq(_, _) => todo!(),
544        //Constraint::LexLess(_, _) => todo!(),
545        //Constraint::LexLeqQuick(_, _) => todo!(),
546        //Constraint::LexLessQuick(_, _) => todo!(),
547        //Constraint::WatchVecNeq(_, _) => todo!(),
548        //Constraint::WatchVecExistsLess(_, _) => todo!(),
549        //Constraint::Hamming(_, _, _) => todo!(),
550        //Constraint::NotHamming(_, _, _) => todo!(),
551        //Constraint::FrameUpdate(_, _, _, _, _) => todo!(),
552        //Constraint::NegativeTable(_, _) => todo!(),
553        //Constraint::Table(_, _) => todo!(),
554        //Constraint::GacSchema(_, _) => todo!(),
555        //Constraint::LightTable(_, _) => todo!(),
556        //Constraint::Mddc(_, _) => todo!(),
557        //Constraint::NegativeMddc(_, _) => todo!(),
558        //Constraint::Str2Plus(_, _) => todo!(),
559        //Constraint::Max(_, _) => todo!(),
560        //Constraint::Min(_, _) => todo!(),
561        //Constraint::NvalueGeq(_, _) => todo!(),
562        //Constraint::NvalueLeq(_, _) => todo!(),
563        //Constraint::Element(_, _, _) => todo!(),
564        //Constraint::ElementOne(_, _, _) => todo!(),
565        //Constraint::ElementUndefZero(_, _, _) => todo!(),
566        //Constraint::WatchElement(_, _, _) => todo!(),
567        //Constraint::WatchElementOne(_, _, _) => todo!(),
568        //Constraint::WatchElementOneUndefZero(_, _, _) => todo!(),
569        //Constraint::WatchElementUndefZero(_, _, _) => todo!(),
570        Constraint::WLiteral(a, b) => {
571            read_var(i, r_constr, a)?;
572            read_constant(r_constr, b)?;
573            Ok(())
574        }
575        //Constraint::WNotLiteral(_, _) => todo!(),
576        //Constraint::WInIntervalSet(_, _) => todo!(),
577        //Constraint::WInRange(_, _) => todo!(),
578        Constraint::WInset(a, b) => {
579            read_var(i, r_constr, a)?;
580            read_constant_list(r_constr, b)?;
581            Ok(())
582        }
583        //Constraint::WNotInRange(_, _) => todo!(),
584        //Constraint::WNotInset(_, _) => todo!(),
585        Constraint::Abs(a, b) => {
586            read_var(i, r_constr, a)?;
587            read_var(i, r_constr, b)?;
588            Ok(())
589        }
590        Constraint::DisEq(a, b) => {
591            read_var(i, r_constr, a)?;
592            read_var(i, r_constr, b)?;
593            Ok(())
594        }
595        Constraint::MinusEq(a, b) => {
596            read_var(i, r_constr, a)?;
597            read_var(i, r_constr, b)?;
598            Ok(())
599        }
600        //Constraint::GacEq(_, _) => todo!(),
601        //Constraint::WatchLess(_, _) => todo!(),
602        // TODO: ensure that this is a bool?
603        Constraint::WatchNeq(a, b) => {
604            read_var(i, r_constr, a)?;
605            read_var(i, r_constr, b)?;
606            Ok(())
607        }
608
609        Constraint::True => Ok(()),
610        Constraint::False => Ok(()),
611        #[allow(unreachable_patterns)]
612        x => Err(MinionError::NotImplemented(format!("{:?}", x))),
613    }
614}
615
616// DO NOT call manually - this assumes that all needed vars are already in the symbol table.
617// TODO not happy with this just assuming the name is in the symbol table
618unsafe fn read_list(
619    instance: *mut ffi::ProbSpec_CSPInstance,
620    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
621    vars: &Vec<Var>,
622) -> Result<(), MinionError> {
623    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
624    for var in vars {
625        let raw_var = match var {
626            Var::NameRef(name) => {
627                let c_str = CString::new(name.clone()).map_err(|_| {
628                    anyhow!(
629                        "Variable name {:?} contains a null character.",
630                        name.clone()
631                    )
632                })?;
633                ffi::getVarByName(instance, c_str.as_ptr() as _)
634            }
635            Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
636        };
637
638        ffi::vec_var_push_back(raw_vars.ptr, raw_var);
639    }
640
641    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
642
643    Ok(())
644}
645
646unsafe fn read_var(
647    instance: *mut ffi::ProbSpec_CSPInstance,
648    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
649    var: &Var,
650) -> Result<(), MinionError> {
651    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
652    let raw_var = match var {
653        Var::NameRef(name) => {
654            let c_str = CString::new(name.clone()).map_err(|_| {
655                anyhow!(
656                    "Variable name {:?} contains a null character.",
657                    name.clone()
658                )
659            })?;
660            ffi::getVarByName(instance, c_str.as_ptr() as _)
661        }
662        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
663    };
664
665    ffi::vec_var_push_back(raw_vars.ptr, raw_var);
666    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
667
668    Ok(())
669}
670
671unsafe fn read_2_vars(
672    instance: *mut ffi::ProbSpec_CSPInstance,
673    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
674    var1: &Var,
675    var2: &Var,
676) -> Result<(), MinionError> {
677    let mut raw_var = match var1 {
678        Var::NameRef(name) => {
679            let c_str = CString::new(name.clone()).map_err(|_| {
680                anyhow!(
681                    "Variable name {:?} contains a null character.",
682                    name.clone()
683                )
684            })?;
685            ffi::getVarByName(instance, c_str.as_ptr() as _)
686        }
687        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
688    };
689    let mut raw_var2 = match var2 {
690        Var::NameRef(name) => {
691            let c_str = CString::new(name.clone()).map_err(|_| {
692                anyhow!(
693                    "Variable name {:?} contains a null character.",
694                    name.clone()
695                )
696            })?;
697            ffi::getVarByName(instance, c_str.as_ptr() as _)
698        }
699        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
700    };
701    // todo: does this move or copy? I am confus!
702    // TODO need to mkae the semantics of move vs copy / ownership clear in libminion!!
703    // This shouldve leaked everywhere by now but i think libminion copies stuff??
704    ffi::constraint_addTwoVars(raw_constraint, &mut raw_var, &mut raw_var2);
705    Ok(())
706}
707
708unsafe fn read_constant(
709    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
710    constant: &Constant,
711) -> Result<(), MinionError> {
712    let val: i32 = match constant {
713        Constant::Integer(n) => Ok(*n),
714        Constant::Bool(true) => Ok(1),
715        Constant::Bool(false) => Ok(0),
716        x => Err(MinionError::NotImplemented(format!("{:?}", x))),
717    }?;
718
719    ffi::constraint_addConstant(raw_constraint, val);
720
721    Ok(())
722}
723
724unsafe fn read_constant_list(
725    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
726    constants: &[Constant],
727) -> Result<(), MinionError> {
728    let raw_consts = Scoped::new(ffi::vec_int_new(), |x| ffi::vec_var_free(x as _));
729
730    for constant in constants.iter() {
731        let val = match constant {
732            Constant::Integer(n) => Ok(*n),
733            Constant::Bool(true) => Ok(1),
734            Constant::Bool(false) => Ok(0),
735            #[allow(unreachable_patterns)] // TODO: can there be other types?
736            x => Err(MinionError::NotImplemented(format!("{:?}", x))),
737        }?;
738
739        ffi::vec_int_push_back(raw_consts.ptr, val);
740    }
741
742    ffi::constraint_addConstantList(raw_constraint, raw_consts.ptr);
743    Ok(())
744}
745
746//TODO: check if the inner constraint is listed in the model or not?
747//Does this matter?
748// TODO: type-check inner constraints vars and tuples and so on?
749unsafe fn read_constraint(
750    instance: *mut ffi::ProbSpec_CSPInstance,
751    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
752    inner_constraint: Constraint,
753) -> Result<(), MinionError> {
754    let constraint_type = get_constraint_type(&inner_constraint)?;
755    let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
756        ffi::constraint_free(x as _)
757    });
758
759    constraint_add_args(instance, raw_inner_constraint.ptr, &inner_constraint)?;
760
761    ffi::constraint_addConstraint(raw_constraint, raw_inner_constraint.ptr);
762    Ok(())
763}
764
765unsafe fn read_constraint_list(
766    instance: *mut ffi::ProbSpec_CSPInstance,
767    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
768    inner_constraints: &[Constraint],
769) -> Result<(), MinionError> {
770    let raw_inners = Scoped::new(ffi::vec_constraints_new(), |x| {
771        ffi::vec_constraints_free(x as _)
772    });
773    for inner_constraint in inner_constraints.iter() {
774        let constraint_type = get_constraint_type(inner_constraint)?;
775        let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
776            ffi::constraint_free(x as _)
777        });
778
779        constraint_add_args(instance, raw_inner_constraint.ptr, inner_constraint)?;
780        ffi::vec_constraints_push_back(raw_inners.ptr, raw_inner_constraint.ptr);
781    }
782
783    ffi::constraint_addConstraintList(raw_constraint, raw_inners.ptr);
784    Ok(())
785}