minion_sys/
run.rs

1#![allow(unreachable_patterns)]
2#![allow(unsafe_op_in_unsafe_fn)]
3
4use std::{
5    collections::HashMap,
6    ffi::CString,
7    sync::Condvar,
8    sync::{Mutex, MutexGuard},
9};
10
11use anyhow::anyhow;
12
13use crate::{
14    ast::Tuple,
15    ffi::{self},
16};
17use 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/// ```
113pub 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
119static CALLBACK: Mutex<Option<Callback>> = Mutex::new(None);
120
121// the variables we want to return, and their ordering in the print matrix
122static PRINT_VARS: Mutex<Option<Vec<VarName>>> = Mutex::new(None);
123
124static LOCK: (Mutex<bool>, Condvar) = (Mutex::new(false), Condvar::new());
125
126#[unsafe(no_mangle)]
127unsafe 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    let mut guard: MutexGuard<'_, Option<Vec<VarName>>> = PRINT_VARS.lock().unwrap();
134
135    if guard.is_none() {
136        return true;
137    }
138
139    let print_vars = match &mut *guard {
140        Some(x) => x,
141        None => unreachable!(),
142    };
143
144    if print_vars.is_empty() {
145        return true;
146    }
147
148    // build nice solutions view to be used by callback
149    let mut solutions: HashMap<VarName, Constant> = HashMap::new();
150
151    for (i, var) in print_vars.iter().enumerate() {
152        let solution_int: i32 = ffi::printMatrix_getValue(i as _);
153        let solution: Constant = Constant::Integer(solution_int);
154        solutions.insert(var.to_string(), solution);
155    }
156
157    #[allow(clippy::unwrap_used)]
158    match *CALLBACK.lock().unwrap() {
159        None => true,
160        Some(func) => func(solutions),
161    }
162}
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)]
169pub fn run_minion(model: Model, callback: Callback) -> Result<(), MinionError> {
170    // Mutex poisoning is probably panic worthy.
171    *CALLBACK.lock().unwrap() = Some(callback);
172
173    let (lock, condvar) = &LOCK;
174    let mut _lock_guard = condvar
175        .wait_while(lock.lock().unwrap(), |locked| *locked)
176        .unwrap();
177
178    *_lock_guard = true;
179
180    unsafe {
181        // TODO: something better than a manual spinlock
182        let search_opts = ffi::searchOptions_new();
183        let search_method = ffi::searchMethod_new();
184        let search_instance = ffi::instance_new();
185
186        convert_model_to_raw(search_instance, &model)?;
187
188        let res = ffi::runMinion(
189            search_opts,
190            search_method,
191            search_instance,
192            Some(run_callback),
193        );
194
195        ffi::searchMethod_free(search_method);
196        ffi::searchOptions_free(search_opts);
197        ffi::instance_free(search_instance);
198
199        *_lock_guard = false;
200        std::mem::drop(_lock_guard);
201
202        condvar.notify_one();
203
204        match res {
205            0 => Ok(()),
206            x => Err(MinionError::from(RuntimeError::from(x))),
207        }
208    }
209}
210
211unsafe fn convert_model_to_raw(
212    instance: *mut ffi::ProbSpec_CSPInstance,
213    model: &Model,
214) -> 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    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    let mut print_vars_guard = PRINT_VARS.lock().unwrap();
233    *print_vars_guard = Some(vec![]);
234
235    // initialise all variables, and add all variables to the print order
236    for var_name in model.named_variables.get_variable_order() {
237        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        let vartype = model
245            .named_variables
246            .get_vartype(var_name.clone())
247            .ok_or(anyhow!("Could not get var type for {:?}", var_name.clone()))?;
248
249        let (vartype_raw, domain_low, domain_high) = match vartype {
250            VarDomain::Bound(a, b) => Ok((ffi::VariableType_VAR_BOUND, a, b)),
251            VarDomain::Discrete(a, b) => Ok((ffi::VariableType_VAR_DISCRETE, a, b)),
252            VarDomain::Bool => Ok((ffi::VariableType_VAR_BOOL, 0, 1)), // TODO: will this work?
253            x => Err(MinionError::NotImplemented(format!("{x:?}"))),
254        }?;
255
256        ffi::newVar_ffi(
257            instance,
258            c_str.as_ptr() as _,
259            vartype_raw,
260            domain_low,
261            domain_high,
262        );
263
264        let var = ffi::getVarByName(instance, c_str.as_ptr() as _);
265
266        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        (*print_vars_guard).as_mut().unwrap().push(var_name.clone());
273    }
274
275    // only add search variables to search order
276    for search_var_name in model.named_variables.get_search_variable_order() {
277        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        let var = ffi::getVarByName(instance, c_str.as_ptr() as _);
284        ffi::vec_var_push_back(search_vars.ptr, var);
285    }
286
287    let search_order = Scoped::new(
288        ffi::searchOrder_new(search_vars.ptr, ffi::VarOrderEnum_ORDER_STATIC, false),
289        |x| ffi::searchOrder_free(x as _),
290    );
291
292    ffi::instance_addSearchOrder(instance, search_order.ptr);
293
294    /*********************************/
295    /*        Add constraints        */
296    /*********************************/
297
298    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        let constraint_type = get_constraint_type(constraint)?;
304        let raw_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
305            ffi::constraint_free(x as _)
306        });
307
308        constraint_add_args(instance, raw_constraint.ptr, constraint)?;
309        ffi::instance_addConstraint(instance, raw_constraint.ptr);
310    }
311
312    Ok(())
313}
314
315unsafe fn get_constraint_type(constraint: &Constraint) -> Result<u32, MinionError> {
316    match constraint {
317        Constraint::SumGeq(_, _) => Ok(ffi::ConstraintType_CT_GEQSUM),
318        Constraint::SumLeq(_, _) => Ok(ffi::ConstraintType_CT_LEQSUM),
319        Constraint::Ineq(_, _, _) => Ok(ffi::ConstraintType_CT_INEQ),
320        Constraint::Eq(_, _) => Ok(ffi::ConstraintType_CT_EQ),
321        Constraint::Difference(_, _) => Ok(ffi::ConstraintType_CT_DIFFERENCE),
322        Constraint::Div(_, _) => Ok(ffi::ConstraintType_CT_DIV),
323        Constraint::DivUndefZero(_, _) => Ok(ffi::ConstraintType_CT_DIV_UNDEFZERO),
324        Constraint::Modulo(_, _) => Ok(ffi::ConstraintType_CT_MODULO),
325        Constraint::ModuloUndefZero(_, _) => Ok(ffi::ConstraintType_CT_MODULO_UNDEFZERO),
326        Constraint::Pow(_, _) => Ok(ffi::ConstraintType_CT_POW),
327        Constraint::Product(_, _) => Ok(ffi::ConstraintType_CT_PRODUCT2),
328        Constraint::WeightedSumGeq(_, _, _) => Ok(ffi::ConstraintType_CT_WEIGHTGEQSUM),
329        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        Constraint::Reify(_, _) => Ok(ffi::ConstraintType_CT_REIFY),
334        Constraint::ReifyImply(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY),
335        Constraint::ReifyImplyQuick(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY_QUICK),
336        Constraint::WatchedAnd(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_AND),
337        Constraint::WatchedOr(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_OR),
338        Constraint::GacAllDiff(_) => Ok(ffi::ConstraintType_CT_GACALLDIFF),
339        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        Constraint::LexLeq(_, _) => Ok(ffi::ConstraintType_CT_LEXLEQ),
351        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        Constraint::NegativeTable(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NEGATIVE_TABLE),
360        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        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        Constraint::WLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LIT),
382        Constraint::WNotLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOTLIT),
383        Constraint::WInIntervalSet(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_ININTERVALSET),
384        Constraint::WInRange(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_INRANGE),
385        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        Constraint::Abs(_, _) => Ok(ffi::ConstraintType_CT_ABS),
389        Constraint::DisEq(_, _) => Ok(ffi::ConstraintType_CT_DISEQ),
390        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        Constraint::True => Ok(ffi::ConstraintType_CT_TRUE),
395        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}
403
404unsafe fn constraint_add_args(
405    i: *mut ffi::ProbSpec_CSPInstance,
406    r_constr: *mut ffi::ProbSpec_ConstraintBlob,
407    constr: &Constraint,
408) -> Result<(), MinionError> {
409    match constr {
410        Constraint::SumGeq(lhs_vars, rhs_var) => {
411            read_list(i, r_constr, lhs_vars)?;
412            read_var(i, r_constr, rhs_var)?;
413            Ok(())
414        }
415        Constraint::SumLeq(lhs_vars, rhs_var) => {
416            read_list(i, r_constr, lhs_vars)?;
417            read_var(i, r_constr, rhs_var)?;
418            Ok(())
419        }
420        Constraint::Ineq(var1, var2, c) => {
421            read_var(i, r_constr, var1)?;
422            read_var(i, r_constr, var2)?;
423            read_constant(r_constr, c)?;
424            Ok(())
425        }
426        Constraint::Eq(var1, var2) => {
427            read_var(i, r_constr, var1)?;
428            read_var(i, r_constr, var2)?;
429            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        Constraint::DivUndefZero((a, b), c) => {
442            read_2_vars(i, r_constr, a, b)?;
443            read_var(i, r_constr, c)?;
444            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        Constraint::ModuloUndefZero((a, b), c) => {
452            read_2_vars(i, r_constr, a, b)?;
453            read_var(i, r_constr, c)?;
454            Ok(())
455        }
456        Constraint::Pow((a, b), c) => {
457            read_2_vars(i, r_constr, a, b)?;
458            read_var(i, r_constr, c)?;
459            Ok(())
460        }
461        Constraint::Product((a, b), c) => {
462            read_2_vars(i, r_constr, a, b)?;
463            read_var(i, r_constr, c)?;
464            Ok(())
465        }
466        Constraint::WeightedSumGeq(a, b, c) => {
467            read_constant_list(r_constr, a)?;
468            read_list(i, r_constr, b)?;
469            read_var(i, r_constr, c)?;
470            Ok(())
471        }
472        Constraint::WeightedSumLeq(a, b, c) => {
473            read_constant_list(r_constr, a)?;
474            read_list(i, r_constr, b)?;
475            read_var(i, r_constr, c)?;
476            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        Constraint::Reify(a, b) => {
491            read_constraint(i, r_constr, (**a).clone())?;
492            read_var(i, r_constr, b)?;
493            Ok(())
494        }
495        Constraint::ReifyImply(a, b) => {
496            read_constraint(i, r_constr, (**a).clone())?;
497            read_var(i, r_constr, b)?;
498            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        Constraint::WatchedAnd(a) => {
506            read_constraint_list(i, r_constr, a)?;
507            Ok(())
508        }
509        Constraint::WatchedOr(a) => {
510            read_constraint_list(i, r_constr, a)?;
511            Ok(())
512        }
513        Constraint::GacAllDiff(a) => {
514            read_list(i, r_constr, a)?;
515            Ok(())
516        }
517        Constraint::AllDiff(a) => {
518            read_list(i, r_constr, a)?;
519            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        Constraint::LexLess(a, b) => {
555            read_list(i, r_constr, a)?;
556            read_list(i, r_constr, b)?;
557            Ok(())
558        }
559        Constraint::LexLeq(a, b) => {
560            read_list(i, r_constr, a)?;
561            read_list(i, r_constr, b)?;
562            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        Constraint::NegativeTable(vars, tuple_list) | Constraint::Table(vars, tuple_list) => {
576            read_list(i, r_constr, vars)?;
577            read_tuple_list(r_constr, tuple_list)?;
578            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        Constraint::ElementOne(vec, j, e) => {
594            read_list(i, r_constr, vec)?;
595            read_var(i, r_constr, j)?;
596            read_var(i, r_constr, e)?;
597            Ok(())
598        }
599        //Constraint::WatchElementOneUndefZero(_, _, _) => todo!(),
600        //Constraint::WatchElementUndefZero(_, _, _) => todo!(),
601        Constraint::WLiteral(a, b) => {
602            read_var(i, r_constr, a)?;
603            read_constant(r_constr, b)?;
604            Ok(())
605        }
606        //Constraint::WNotLiteral(_, _) => todo!(),
607        Constraint::WInIntervalSet(var, consts) => {
608            read_var(i, r_constr, var)?;
609            read_constant_list(r_constr, consts)?;
610            Ok(())
611        }
612        //Constraint::WInRange(_, _) => todo!(),
613        Constraint::WInset(a, b) => {
614            read_var(i, r_constr, a)?;
615            read_constant_list(r_constr, b)?;
616            Ok(())
617        }
618        //Constraint::WNotInRange(_, _) => todo!(),
619        //Constraint::WNotInset(_, _) => todo!(),
620        Constraint::Abs(a, b) => {
621            read_var(i, r_constr, a)?;
622            read_var(i, r_constr, b)?;
623            Ok(())
624        }
625        Constraint::DisEq(a, b) => {
626            read_var(i, r_constr, a)?;
627            read_var(i, r_constr, b)?;
628            Ok(())
629        }
630        Constraint::MinusEq(a, b) => {
631            read_var(i, r_constr, a)?;
632            read_var(i, r_constr, b)?;
633            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        Constraint::True => Ok(()),
645        Constraint::False => Ok(()),
646        #[allow(unreachable_patterns)]
647        x => Err(MinionError::NotImplemented(format!("{x:?}"))),
648    }
649}
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
653unsafe fn read_list(
654    instance: *mut ffi::ProbSpec_CSPInstance,
655    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
656    vars: &Vec<Var>,
657) -> Result<(), MinionError> {
658    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
659    for var in vars {
660        let raw_var = match var {
661            Var::NameRef(name) => {
662                let c_str = CString::new(name.clone()).map_err(|_| {
663                    anyhow!(
664                        "Variable name {:?} contains a null character.",
665                        name.clone()
666                    )
667                })?;
668                ffi::getVarByName(instance, c_str.as_ptr() as _)
669            }
670            Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
671        };
672
673        ffi::vec_var_push_back(raw_vars.ptr, raw_var);
674    }
675
676    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
677
678    Ok(())
679}
680
681unsafe fn read_var(
682    instance: *mut ffi::ProbSpec_CSPInstance,
683    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
684    var: &Var,
685) -> Result<(), MinionError> {
686    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
687    let raw_var = match var {
688        Var::NameRef(name) => {
689            let c_str = CString::new(name.clone()).map_err(|_| {
690                anyhow!(
691                    "Variable name {:?} contains a null character.",
692                    name.clone()
693                )
694            })?;
695            ffi::getVarByName(instance, c_str.as_ptr() as _)
696        }
697        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
698    };
699
700    ffi::vec_var_push_back(raw_vars.ptr, raw_var);
701    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
702
703    Ok(())
704}
705
706unsafe fn read_2_vars(
707    instance: *mut ffi::ProbSpec_CSPInstance,
708    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
709    var1: &Var,
710    var2: &Var,
711) -> Result<(), MinionError> {
712    let mut raw_var = match var1 {
713        Var::NameRef(name) => {
714            let c_str = CString::new(name.clone()).map_err(|_| {
715                anyhow!(
716                    "Variable name {:?} contains a null character.",
717                    name.clone()
718                )
719            })?;
720            ffi::getVarByName(instance, c_str.as_ptr() as _)
721        }
722        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
723    };
724    let mut raw_var2 = match var2 {
725        Var::NameRef(name) => {
726            let c_str = CString::new(name.clone()).map_err(|_| {
727                anyhow!(
728                    "Variable name {:?} contains a null character.",
729                    name.clone()
730                )
731            })?;
732            ffi::getVarByName(instance, c_str.as_ptr() as _)
733        }
734        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    ffi::constraint_addTwoVars(raw_constraint, &mut raw_var, &mut raw_var2);
740    Ok(())
741}
742
743unsafe fn read_constant(
744    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
745    constant: &Constant,
746) -> Result<(), MinionError> {
747    let val: i32 = match constant {
748        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    ffi::constraint_addConstant(raw_constraint, val);
755
756    Ok(())
757}
758
759unsafe fn read_constant_list(
760    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
761    constants: &[Constant],
762) -> Result<(), MinionError> {
763    let raw_consts = Scoped::new(ffi::vec_int_new(), |x| ffi::vec_int_free(x as _));
764
765    for constant in constants.iter() {
766        let val = match constant {
767            Constant::Integer(n) => Ok(*n),
768            Constant::Bool(true) => Ok(1),
769            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        ffi::vec_int_push_back(raw_consts.ptr, val);
775    }
776
777    ffi::constraint_addConstantList(raw_constraint, raw_consts.ptr);
778    Ok(())
779}
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?
784unsafe fn read_constraint(
785    instance: *mut ffi::ProbSpec_CSPInstance,
786    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
787    inner_constraint: Constraint,
788) -> Result<(), MinionError> {
789    let constraint_type = get_constraint_type(&inner_constraint)?;
790    let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
791        ffi::constraint_free(x as _)
792    });
793
794    constraint_add_args(instance, raw_inner_constraint.ptr, &inner_constraint)?;
795
796    ffi::constraint_addConstraint(raw_constraint, raw_inner_constraint.ptr);
797    Ok(())
798}
799
800unsafe fn read_constraint_list(
801    instance: *mut ffi::ProbSpec_CSPInstance,
802    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
803    inner_constraints: &[Constraint],
804) -> Result<(), MinionError> {
805    let raw_inners = Scoped::new(ffi::vec_constraints_new(), |x| {
806        ffi::vec_constraints_free(x as _)
807    });
808    for inner_constraint in inner_constraints.iter() {
809        let constraint_type = get_constraint_type(inner_constraint)?;
810        let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
811            ffi::constraint_free(x as _)
812        });
813
814        constraint_add_args(instance, raw_inner_constraint.ptr, inner_constraint)?;
815        ffi::vec_constraints_push_back(raw_inners.ptr, raw_inner_constraint.ptr);
816    }
817
818    ffi::constraint_addConstraintList(raw_constraint, raw_inners.ptr);
819    Ok(())
820}
821
822unsafe fn read_tuple_list(
823    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
824    tuples: &Vec<Tuple>,
825) -> Result<(), MinionError> {
826    // a tuple list is just a vec<vec<int>>, where each inner vec is a tuple
827    let raw_tuples = Scoped::new(ffi::vec_vec_int_new(), |x| ffi::vec_vec_int_free(x as _));
828    for tuple in tuples {
829        let raw_tuple = Scoped::new(ffi::vec_int_new(), |x| ffi::vec_int_free(x as _));
830        for constant in tuple.iter() {
831            let val = match constant {
832                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            ffi::vec_int_push_back(raw_tuple.ptr, val);
840        }
841
842        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    let raw_tuple_list = ffi::tupleList_new(raw_tuples.ptr);
848    ffi::constraint_setTuples(raw_constraint, raw_tuple_list);
849
850    Ok(())
851}
minion_sys/run.rs

minion_sys/
run.rs
