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::ffi::{self};
14use 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/// ```
110pub 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
116static CALLBACK: Mutex<Option<Callback>> = Mutex::new(None);
117
118// the variables we want to return, and their ordering in the print matrix
119static PRINT_VARS: Mutex<Option<Vec<VarName>>> = Mutex::new(None);
120
121static LOCK: (Mutex<bool>, Condvar) = (Mutex::new(false), Condvar::new());
122
123#[unsafe(no_mangle)]
124unsafe 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    let mut guard: MutexGuard<'_, Option<Vec<VarName>>> = PRINT_VARS.lock().unwrap();
131
132    if guard.is_none() {
133        return true;
134    }
135
136    let print_vars = match &mut *guard {
137        Some(x) => x,
138        None => unreachable!(),
139    };
140
141    if print_vars.is_empty() {
142        return true;
143    }
144
145    // build nice solutions view to be used by callback
146    let mut solutions: HashMap<VarName, Constant> = HashMap::new();
147
148    for (i, var) in print_vars.iter().enumerate() {
149        let solution_int: i32 = ffi::printMatrix_getValue(i as _);
150        let solution: Constant = Constant::Integer(solution_int);
151        solutions.insert(var.to_string(), solution);
152    }
153
154    #[allow(clippy::unwrap_used)]
155    match *CALLBACK.lock().unwrap() {
156        None => true,
157        Some(func) => func(solutions),
158    }
159}
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)]
166pub fn run_minion(model: Model, callback: Callback) -> Result<(), MinionError> {
167    // Mutex poisoning is probably panic worthy.
168    *CALLBACK.lock().unwrap() = Some(callback);
169
170    let (lock, condvar) = &LOCK;
171    let mut _lock_guard = condvar
172        .wait_while(lock.lock().unwrap(), |locked| *locked)
173        .unwrap();
174
175    *_lock_guard = true;
176
177    unsafe {
178        // TODO: something better than a manual spinlock
179        let search_opts = ffi::searchOptions_new();
180        let search_method = ffi::searchMethod_new();
181        let search_instance = ffi::instance_new();
182
183        convert_model_to_raw(search_instance, &model)?;
184
185        let res = ffi::runMinion(
186            search_opts,
187            search_method,
188            search_instance,
189            Some(run_callback),
190        );
191
192        ffi::searchMethod_free(search_method);
193        ffi::searchOptions_free(search_opts);
194        ffi::instance_free(search_instance);
195
196        *_lock_guard = false;
197        std::mem::drop(_lock_guard);
198
199        condvar.notify_one();
200
201        match res {
202            0 => Ok(()),
203            x => Err(MinionError::from(RuntimeError::from(x))),
204        }
205    }
206}
207
208unsafe fn convert_model_to_raw(
209    instance: *mut ffi::ProbSpec_CSPInstance,
210    model: &Model,
211) -> 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    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    let mut print_vars_guard = PRINT_VARS.lock().unwrap();
230    *print_vars_guard = Some(vec![]);
231
232    // initialise all variables, and add all variables to the print order
233    for var_name in model.named_variables.get_variable_order() {
234        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        let vartype = model
242            .named_variables
243            .get_vartype(var_name.clone())
244            .ok_or(anyhow!("Could not get var type for {:?}", var_name.clone()))?;
245
246        let (vartype_raw, domain_low, domain_high) = match vartype {
247            VarDomain::Bound(a, b) => Ok((ffi::VariableType_VAR_BOUND, a, b)),
248            VarDomain::Bool => Ok((ffi::VariableType_VAR_BOOL, 0, 1)), // TODO: will this work?
249            x => Err(MinionError::NotImplemented(format!("{x:?}"))),
250        }?;
251
252        ffi::newVar_ffi(
253            instance,
254            c_str.as_ptr() as _,
255            vartype_raw,
256            domain_low,
257            domain_high,
258        );
259
260        let var = ffi::getVarByName(instance, c_str.as_ptr() as _);
261
262        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        (*print_vars_guard).as_mut().unwrap().push(var_name.clone());
269    }
270
271    // only add search variables to search order
272    for search_var_name in model.named_variables.get_search_variable_order() {
273        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        let var = ffi::getVarByName(instance, c_str.as_ptr() as _);
280        ffi::vec_var_push_back(search_vars.ptr, var);
281    }
282
283    let search_order = Scoped::new(
284        ffi::searchOrder_new(search_vars.ptr, ffi::VarOrderEnum_ORDER_STATIC, false),
285        |x| ffi::searchOrder_free(x as _),
286    );
287
288    ffi::instance_addSearchOrder(instance, search_order.ptr);
289
290    /*********************************/
291    /*        Add constraints        */
292    /*********************************/
293
294    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        let constraint_type = get_constraint_type(constraint)?;
300        let raw_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
301            ffi::constraint_free(x as _)
302        });
303
304        constraint_add_args(instance, raw_constraint.ptr, constraint)?;
305        ffi::instance_addConstraint(instance, raw_constraint.ptr);
306    }
307
308    Ok(())
309}
310
311unsafe fn get_constraint_type(constraint: &Constraint) -> Result<u32, MinionError> {
312    match constraint {
313        Constraint::SumGeq(_, _) => Ok(ffi::ConstraintType_CT_GEQSUM),
314        Constraint::SumLeq(_, _) => Ok(ffi::ConstraintType_CT_LEQSUM),
315        Constraint::Ineq(_, _, _) => Ok(ffi::ConstraintType_CT_INEQ),
316        Constraint::Eq(_, _) => Ok(ffi::ConstraintType_CT_EQ),
317        Constraint::Difference(_, _) => Ok(ffi::ConstraintType_CT_DIFFERENCE),
318        Constraint::Div(_, _) => Ok(ffi::ConstraintType_CT_DIV),
319        Constraint::DivUndefZero(_, _) => Ok(ffi::ConstraintType_CT_DIV_UNDEFZERO),
320        Constraint::Modulo(_, _) => Ok(ffi::ConstraintType_CT_MODULO),
321        Constraint::ModuloUndefZero(_, _) => Ok(ffi::ConstraintType_CT_MODULO_UNDEFZERO),
322        Constraint::Pow(_, _) => Ok(ffi::ConstraintType_CT_POW),
323        Constraint::Product(_, _) => Ok(ffi::ConstraintType_CT_PRODUCT2),
324        Constraint::WeightedSumGeq(_, _, _) => Ok(ffi::ConstraintType_CT_WEIGHTGEQSUM),
325        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        Constraint::Reify(_, _) => Ok(ffi::ConstraintType_CT_REIFY),
330        Constraint::ReifyImply(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY),
331        Constraint::ReifyImplyQuick(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY_QUICK),
332        Constraint::WatchedAnd(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_AND),
333        Constraint::WatchedOr(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_OR),
334        Constraint::GacAllDiff(_) => Ok(ffi::ConstraintType_CT_GACALLDIFF),
335        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        Constraint::LexLeq(_, _) => Ok(ffi::ConstraintType_CT_LEXLEQ),
347        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        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        Constraint::WLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LIT),
378        Constraint::WNotLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOTLIT),
379        Constraint::WInIntervalSet(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_ININTERVALSET),
380        Constraint::WInRange(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_INRANGE),
381        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        Constraint::Abs(_, _) => Ok(ffi::ConstraintType_CT_ABS),
385        Constraint::DisEq(_, _) => Ok(ffi::ConstraintType_CT_DISEQ),
386        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        Constraint::True => Ok(ffi::ConstraintType_CT_TRUE),
391        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}
399
400unsafe fn constraint_add_args(
401    i: *mut ffi::ProbSpec_CSPInstance,
402    r_constr: *mut ffi::ProbSpec_ConstraintBlob,
403    constr: &Constraint,
404) -> Result<(), MinionError> {
405    match constr {
406        Constraint::SumGeq(lhs_vars, rhs_var) => {
407            read_list(i, r_constr, lhs_vars)?;
408            read_var(i, r_constr, rhs_var)?;
409            Ok(())
410        }
411        Constraint::SumLeq(lhs_vars, rhs_var) => {
412            read_list(i, r_constr, lhs_vars)?;
413            read_var(i, r_constr, rhs_var)?;
414            Ok(())
415        }
416        Constraint::Ineq(var1, var2, c) => {
417            read_var(i, r_constr, var1)?;
418            read_var(i, r_constr, var2)?;
419            read_constant(r_constr, c)?;
420            Ok(())
421        }
422        Constraint::Eq(var1, var2) => {
423            read_var(i, r_constr, var1)?;
424            read_var(i, r_constr, var2)?;
425            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        Constraint::DivUndefZero((a, b), c) => {
438            read_2_vars(i, r_constr, a, b)?;
439            read_var(i, r_constr, c)?;
440            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        Constraint::ModuloUndefZero((a, b), c) => {
448            read_2_vars(i, r_constr, a, b)?;
449            read_var(i, r_constr, c)?;
450            Ok(())
451        }
452        Constraint::Pow((a, b), c) => {
453            read_2_vars(i, r_constr, a, b)?;
454            read_var(i, r_constr, c)?;
455            Ok(())
456        }
457        Constraint::Product((a, b), c) => {
458            read_2_vars(i, r_constr, a, b)?;
459            read_var(i, r_constr, c)?;
460            Ok(())
461        }
462        Constraint::WeightedSumGeq(a, b, c) => {
463            read_constant_list(r_constr, a)?;
464            read_list(i, r_constr, b)?;
465            read_var(i, r_constr, c)?;
466            Ok(())
467        }
468        Constraint::WeightedSumLeq(a, b, c) => {
469            read_constant_list(r_constr, a)?;
470            read_list(i, r_constr, b)?;
471            read_var(i, r_constr, c)?;
472            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        Constraint::Reify(a, b) => {
487            read_constraint(i, r_constr, (**a).clone())?;
488            read_var(i, r_constr, b)?;
489            Ok(())
490        }
491        Constraint::ReifyImply(a, b) => {
492            read_constraint(i, r_constr, (**a).clone())?;
493            read_var(i, r_constr, b)?;
494            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        Constraint::WatchedAnd(a) => {
502            read_constraint_list(i, r_constr, a)?;
503            Ok(())
504        }
505        Constraint::WatchedOr(a) => {
506            read_constraint_list(i, r_constr, a)?;
507            Ok(())
508        }
509        Constraint::GacAllDiff(a) => {
510            read_list(i, r_constr, a)?;
511            Ok(())
512        }
513        Constraint::AllDiff(a) => {
514            read_list(i, r_constr, a)?;
515            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        Constraint::LexLess(a, b) => {
551            read_list(i, r_constr, a)?;
552            read_list(i, r_constr, b)?;
553            Ok(())
554        }
555        Constraint::LexLeq(a, b) => {
556            read_list(i, r_constr, a)?;
557            read_list(i, r_constr, b)?;
558            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        Constraint::ElementOne(vec, j, e) => {
587            read_list(i, r_constr, vec)?;
588            read_var(i, r_constr, j)?;
589            read_var(i, r_constr, e)?;
590            Ok(())
591        }
592        //Constraint::WatchElementOneUndefZero(_, _, _) => todo!(),
593        //Constraint::WatchElementUndefZero(_, _, _) => todo!(),
594        Constraint::WLiteral(a, b) => {
595            read_var(i, r_constr, a)?;
596            read_constant(r_constr, b)?;
597            Ok(())
598        }
599        //Constraint::WNotLiteral(_, _) => todo!(),
600        Constraint::WInIntervalSet(var, consts) => {
601            read_var(i, r_constr, var)?;
602            read_constant_list(r_constr, consts)?;
603            Ok(())
604        }
605        //Constraint::WInRange(_, _) => todo!(),
606        Constraint::WInset(a, b) => {
607            read_var(i, r_constr, a)?;
608            read_constant_list(r_constr, b)?;
609            Ok(())
610        }
611        //Constraint::WNotInRange(_, _) => todo!(),
612        //Constraint::WNotInset(_, _) => todo!(),
613        Constraint::Abs(a, b) => {
614            read_var(i, r_constr, a)?;
615            read_var(i, r_constr, b)?;
616            Ok(())
617        }
618        Constraint::DisEq(a, b) => {
619            read_var(i, r_constr, a)?;
620            read_var(i, r_constr, b)?;
621            Ok(())
622        }
623        Constraint::MinusEq(a, b) => {
624            read_var(i, r_constr, a)?;
625            read_var(i, r_constr, b)?;
626            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        Constraint::True => Ok(()),
638        Constraint::False => Ok(()),
639        #[allow(unreachable_patterns)]
640        x => Err(MinionError::NotImplemented(format!("{x:?}"))),
641    }
642}
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
646unsafe fn read_list(
647    instance: *mut ffi::ProbSpec_CSPInstance,
648    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
649    vars: &Vec<Var>,
650) -> Result<(), MinionError> {
651    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
652    for var in vars {
653        let raw_var = match var {
654            Var::NameRef(name) => {
655                let c_str = CString::new(name.clone()).map_err(|_| {
656                    anyhow!(
657                        "Variable name {:?} contains a null character.",
658                        name.clone()
659                    )
660                })?;
661                ffi::getVarByName(instance, c_str.as_ptr() as _)
662            }
663            Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
664        };
665
666        ffi::vec_var_push_back(raw_vars.ptr, raw_var);
667    }
668
669    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
670
671    Ok(())
672}
673
674unsafe fn read_var(
675    instance: *mut ffi::ProbSpec_CSPInstance,
676    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
677    var: &Var,
678) -> Result<(), MinionError> {
679    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
680    let raw_var = match var {
681        Var::NameRef(name) => {
682            let c_str = CString::new(name.clone()).map_err(|_| {
683                anyhow!(
684                    "Variable name {:?} contains a null character.",
685                    name.clone()
686                )
687            })?;
688            ffi::getVarByName(instance, c_str.as_ptr() as _)
689        }
690        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
691    };
692
693    ffi::vec_var_push_back(raw_vars.ptr, raw_var);
694    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
695
696    Ok(())
697}
698
699unsafe fn read_2_vars(
700    instance: *mut ffi::ProbSpec_CSPInstance,
701    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
702    var1: &Var,
703    var2: &Var,
704) -> Result<(), MinionError> {
705    let mut raw_var = match var1 {
706        Var::NameRef(name) => {
707            let c_str = CString::new(name.clone()).map_err(|_| {
708                anyhow!(
709                    "Variable name {:?} contains a null character.",
710                    name.clone()
711                )
712            })?;
713            ffi::getVarByName(instance, c_str.as_ptr() as _)
714        }
715        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
716    };
717    let mut raw_var2 = match var2 {
718        Var::NameRef(name) => {
719            let c_str = CString::new(name.clone()).map_err(|_| {
720                anyhow!(
721                    "Variable name {:?} contains a null character.",
722                    name.clone()
723                )
724            })?;
725            ffi::getVarByName(instance, c_str.as_ptr() as _)
726        }
727        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    ffi::constraint_addTwoVars(raw_constraint, &mut raw_var, &mut raw_var2);
733    Ok(())
734}
735
736unsafe fn read_constant(
737    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
738    constant: &Constant,
739) -> Result<(), MinionError> {
740    let val: i32 = match constant {
741        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    ffi::constraint_addConstant(raw_constraint, val);
748
749    Ok(())
750}
751
752unsafe fn read_constant_list(
753    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
754    constants: &[Constant],
755) -> Result<(), MinionError> {
756    let raw_consts = Scoped::new(ffi::vec_int_new(), |x| ffi::vec_var_free(x as _));
757
758    for constant in constants.iter() {
759        let val = match constant {
760            Constant::Integer(n) => Ok(*n),
761            Constant::Bool(true) => Ok(1),
762            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        ffi::vec_int_push_back(raw_consts.ptr, val);
768    }
769
770    ffi::constraint_addConstantList(raw_constraint, raw_consts.ptr);
771    Ok(())
772}
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?
777unsafe fn read_constraint(
778    instance: *mut ffi::ProbSpec_CSPInstance,
779    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
780    inner_constraint: Constraint,
781) -> Result<(), MinionError> {
782    let constraint_type = get_constraint_type(&inner_constraint)?;
783    let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
784        ffi::constraint_free(x as _)
785    });
786
787    constraint_add_args(instance, raw_inner_constraint.ptr, &inner_constraint)?;
788
789    ffi::constraint_addConstraint(raw_constraint, raw_inner_constraint.ptr);
790    Ok(())
791}
792
793unsafe fn read_constraint_list(
794    instance: *mut ffi::ProbSpec_CSPInstance,
795    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
796    inner_constraints: &[Constraint],
797) -> Result<(), MinionError> {
798    let raw_inners = Scoped::new(ffi::vec_constraints_new(), |x| {
799        ffi::vec_constraints_free(x as _)
800    });
801    for inner_constraint in inner_constraints.iter() {
802        let constraint_type = get_constraint_type(inner_constraint)?;
803        let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
804            ffi::constraint_free(x as _)
805        });
806
807        constraint_add_args(instance, raw_inner_constraint.ptr, inner_constraint)?;
808        ffi::vec_constraints_push_back(raw_inners.ptr, raw_inner_constraint.ptr);
809    }
810
811    ffi::constraint_addConstraintList(raw_constraint, raw_inners.ptr);
812    Ok(())
813}
minion_sys/run.rs

minion_sys/
run.rs
