minion_sys/
run.rs

1#![allow(unreachable_patterns)]
2#![allow(unsafe_op_in_unsafe_fn)]
3
4use std::{
5    collections::HashMap,
6    ffi::{CStr, CString, c_char, c_void},
7};
8
9use anyhow::anyhow;
10
11use crate::{
12    ast::Tuple,
13    ffi::{self},
14};
15use crate::{
16    ast::{Constant, Constraint, Model, Var, VarDomain, VarName},
17    error::{MinionError, RuntimeError},
18    scoped_ptr::Scoped,
19};
20
21unsafe fn take_minion_ffi_error() -> String {
22    let error_ptr = ffi::minion_get_last_error();
23    if error_ptr.is_null() {
24        return "unknown Minion FFI error".to_string();
25    }
26
27    let message = CStr::from_ptr(error_ptr).to_string_lossy().into_owned();
28    ffi::minion_clear_last_error();
29    if message.is_empty() {
30        "unknown Minion FFI error".to_string()
31    } else {
32        message
33    }
34}
35
36unsafe fn new_var_ffi_checked(
37    instance: *mut ffi::ProbSpec_CSPInstance,
38    name: *const c_char,
39    vartype_raw: ffi::VariableType,
40    domain_low: i32,
41    domain_high: i32,
42) -> Result<(), MinionError> {
43    if ffi::newVar_ffi_safe(
44        instance,
45        name as *mut c_char,
46        vartype_raw,
47        domain_low,
48        domain_high,
49    ) {
50        Ok(())
51    } else {
52        Err(MinionError::Other(anyhow!(take_minion_ffi_error())))
53    }
54}
55
56unsafe fn get_var_by_name_checked(
57    instance: *mut ffi::ProbSpec_CSPInstance,
58    name: *const c_char,
59) -> Result<ffi::ProbSpec_Var, MinionError> {
60    let mut var = ffi::ProbSpec_Var {
61        type_m: ffi::VariableType_VAR_CONSTANT,
62        pos_m: 0,
63    };
64
65    if ffi::getVarByName_safe(instance, name as *mut c_char, &mut var) {
66        Ok(var)
67    } else {
68        Err(MinionError::Other(anyhow!(take_minion_ffi_error())))
69    }
70}
71
72/// The callback type used by [`run_minion`].
73///
74/// Called by Minion whenever a solution is found. The input is
75/// a `HashMap` of all named variables along with their value.
76///
77/// Return `true` to continue searching, `false` to stop.
78///
79/// Since this is a boxed closure, it can capture state from its environment,
80/// eliminating the need for global or thread-local state in callers.
81///
82/// # Examples
83///
84/// ```
85///   use minion_sys::ast::*;
86///   use minion_sys::run_minion;
87///   use std::collections::HashMap;
88///
89///   let mut all_solutions: Vec<HashMap<VarName,Constant>> = vec![];
90///
91///   let callback = Box::new(|solutions: HashMap<VarName,Constant>| -> bool {
92///       all_solutions.push(solutions);
93///       true
94///   });
95///
96///   // Build and run the model.
97///   let mut model = Model::new();
98///
99///   // ... omitted for brevity ...
100/// # model
101/// #     .named_variables
102/// #     .add_var("x".to_owned(), VarDomain::Bound(1, 3));
103/// # model
104/// #     .named_variables
105/// #     .add_var("y".to_owned(), VarDomain::Bound(2, 4));
106/// # model
107/// #     .named_variables
108/// #     .add_var("z".to_owned(), VarDomain::Bound(1, 5));
109/// #
110/// # let leq = Constraint::SumLeq(
111/// #     vec![
112/// #         Var::NameRef("x".to_owned()),
113/// #         Var::NameRef("y".to_owned()),
114/// #         Var::NameRef("z".to_owned()),
115/// #     ],
116/// #     Var::ConstantAsVar(4),
117/// # );
118/// #
119/// # let geq = Constraint::SumGeq(
120/// #     vec![
121/// #         Var::NameRef("x".to_owned()),
122/// #         Var::NameRef("y".to_owned()),
123/// #         Var::NameRef("z".to_owned()),
124/// #     ],
125/// #     Var::ConstantAsVar(4),
126/// # );
127/// #
128/// # let ineq = Constraint::Ineq(
129/// #     Var::NameRef("x".to_owned()),
130/// #     Var::NameRef("y".to_owned()),
131/// #     Constant::Integer(-1),
132/// # );
133/// #
134/// # model.constraints.push(leq);
135/// # model.constraints.push(geq);
136/// # model.constraints.push(ineq);
137///
138///   let _solver_ctx = run_minion(model, callback).expect("Error occurred");
139///
140///   let solution_set_1 = &all_solutions[0];
141///   let x1 = solution_set_1.get("x").unwrap();
142///   let y1 = solution_set_1.get("y").unwrap();
143///   let z1 = solution_set_1.get("z").unwrap();
144/// #
145/// # assert_eq!(all_solutions.len(),1);
146/// # assert_eq!(*x1,Constant::Integer(1));
147/// # assert_eq!(*y1,Constant::Integer(2));
148/// # assert_eq!(*z1,Constant::Integer(1));
149/// ```
150pub type Callback<'a> = Box<dyn FnMut(HashMap<VarName, Constant>) -> bool + 'a>;
151
152/// State passed through the C callback's `void* userdata` pointer.
153///
154/// This replaces the old thread-local approach — all callback state is now
155/// passed explicitly through the FFI userdata mechanism.
156struct CallbackState<'a> {
157    callback: Callback<'a>,
158    print_vars: Vec<VarName>,
159}
160
161/// Opaque handle to a Minion solver context.
162///
163/// Holds solver state (including run statistics) after a solve completes.
164/// Query results (e.g. via [`SolverContext::get_from_table`]) before dropping.
165pub struct SolverContext {
166    ctx: *mut ffi::MinionContext,
167}
168
169// Safety: MinionContext is an independent solver instance. It is safe to send
170// between threads as long as it is not used concurrently (which we ensure by
171// only accessing it through &mut self or after the solve completes).
172unsafe impl Send for SolverContext {}
173
174impl SolverContext {
175    /// Gets a value from Minion's TableOut (where it stores run statistics).
176    pub fn get_from_table(&self, key: String) -> Option<String> {
177        unsafe {
178            #[allow(clippy::expect_used)]
179            let c_string = CString::new(key).expect("");
180            let key_ptr = c_string.into_raw();
181            let val_ptr: *mut c_char = ffi::TableOut_get(self.ctx, key_ptr);
182
183            drop(CString::from_raw(key_ptr));
184
185            if val_ptr.is_null() {
186                None
187            } else {
188                #[allow(clippy::unwrap_used)]
189                let res = CStr::from_ptr(val_ptr).to_str().unwrap().to_owned();
190                libc::free(val_ptr as _);
191                Some(res)
192            }
193        }
194    }
195}
196
197impl Drop for SolverContext {
198    fn drop(&mut self) {
199        unsafe {
200            ffi::minion_freeContext(self.ctx);
201        }
202    }
203}
204
205/// The C callback passed to `runMinion`. Receives the active context and our
206/// `CallbackState` via the userdata pointer.
207unsafe extern "C" fn run_callback(ctx: *mut ffi::MinionContext, userdata: *mut c_void) -> bool {
208    // Safety: userdata is a pointer to our CallbackState, set by run_minion
209    // and valid for the duration of the runMinion call.
210    let state = unsafe { &mut *(userdata as *mut CallbackState<'_>) };
211
212    if state.print_vars.is_empty() {
213        return true;
214    }
215
216    // Build solutions HashMap by reading variable values from Minion.
217    let mut solutions: HashMap<VarName, Constant> = HashMap::new();
218    for (i, var) in state.print_vars.iter().enumerate() {
219        let solution_int: i32 = unsafe { ffi::printMatrix_getValue(ctx, i as _) };
220        let solution: Constant = Constant::Integer(solution_int);
221        solutions.insert(var.to_string(), solution);
222    }
223
224    (state.callback)(solutions)
225}
226
227/// Run Minion on the given [Model].
228///
229/// The given [callback](Callback) is ran whenever a new solution set is found.
230///
231/// Returns a [`SolverContext`] on success, which can be used to query run
232/// statistics via [`SolverContext::get_from_table`].
233#[allow(clippy::unwrap_used)]
234pub fn run_minion(model: Model, callback: Callback<'_>) -> Result<SolverContext, MinionError> {
235    let mut state = CallbackState {
236        callback,
237        print_vars: vec![],
238    };
239
240    unsafe {
241        let ctx = ffi::minion_newContext();
242        let search_opts = ffi::searchOptions_new();
243        let search_method = ffi::searchMethod_new();
244        let search_instance = ffi::instance_new();
245
246        // Use Minion as a quiet library by default. Low-level FFI callers that
247        // want native solver output can opt out by configuring SearchOptions
248        // themselves instead of going through this wrapper.
249        (*search_opts).silent = true;
250        (*search_opts).print_solution = false;
251
252        convert_model_to_raw(search_instance, &model, &mut state.print_vars)?;
253
254        let userdata = &mut state as *mut CallbackState<'_> as *mut c_void;
255        let res = ffi::runMinion(
256            ctx,
257            search_opts,
258            search_method,
259            search_instance,
260            Some(run_callback),
261            userdata,
262        );
263
264        ffi::searchMethod_free(search_method);
265        ffi::searchOptions_free(search_opts);
266        ffi::instance_free(search_instance);
267
268        match res {
269            0 => Ok(SolverContext { ctx }),
270            x => {
271                ffi::minion_freeContext(ctx);
272                Err(MinionError::from(RuntimeError::from(x)))
273            }
274        }
275    }
276}
277
278unsafe fn convert_model_to_raw(
279    instance: *mut ffi::ProbSpec_CSPInstance,
280    model: &Model,
281    print_vars: &mut Vec<VarName>,
282) -> Result<(), MinionError> {
283    /*******************************/
284    /*        Add variables        */
285    /*******************************/
286
287    /*
288     * Add variables to:
289     * 1. symbol table
290     * 2. print matrix
291     * 3. search vars
292     *
293     * These are all done in the order saved in the SymbolTable.
294     */
295
296    let search_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
297
298    // initialise all variables, and add all variables to the print order
299    for var_name in model.named_variables.get_variable_order() {
300        let c_str = CString::new(var_name.clone()).map_err(|_| {
301            anyhow!(
302                "Variable name {:?} contains a null character.",
303                var_name.clone()
304            )
305        })?;
306
307        let vartype = model
308            .named_variables
309            .get_vartype(var_name.clone())
310            .ok_or(anyhow!("Could not get var type for {:?}", var_name.clone()))?;
311
312        let (vartype_raw, domain_low, domain_high) = match vartype {
313            VarDomain::Bound(a, b) => Ok((ffi::VariableType_VAR_BOUND, a, b)),
314            VarDomain::Discrete(a, b) => Ok((ffi::VariableType_VAR_DISCRETE, a, b)),
315            VarDomain::Bool => Ok((ffi::VariableType_VAR_BOOL, 0, 1)), // TODO: will this work?
316            x => Err(MinionError::NotImplemented(format!("{x:?}"))),
317        }?;
318
319        new_var_ffi_checked(
320            instance,
321            c_str.as_ptr(),
322            vartype_raw,
323            domain_low,
324            domain_high,
325        )?;
326
327        let var = get_var_by_name_checked(instance, c_str.as_ptr())?;
328
329        ffi::printMatrix_addVar(instance, var);
330
331        // Remember the order for the callback function.
332        print_vars.push(var_name.clone());
333    }
334
335    // only add search variables to search order
336    for search_var_name in model.named_variables.get_search_variable_order() {
337        let c_str = CString::new(search_var_name.clone()).map_err(|_| {
338            anyhow!(
339                "Variable name {:?} contains a null character.",
340                search_var_name.clone()
341            )
342        })?;
343        let var = get_var_by_name_checked(instance, c_str.as_ptr())?;
344        ffi::vec_var_push_back(search_vars.ptr, var);
345    }
346
347    let search_order = Scoped::new(
348        ffi::searchOrder_new(search_vars.ptr, ffi::VarOrderEnum_ORDER_STATIC, false),
349        |x| ffi::searchOrder_free(x as _),
350    );
351
352    ffi::instance_addSearchOrder(instance, search_order.ptr);
353
354    /*********************************/
355    /*        Add constraints        */
356    /*********************************/
357
358    for constraint in &model.constraints {
359        // 1. get constraint type and create C++ constraint object
360        // 2. run through arguments and add them to the constraint
361        // 3. add constraint to instance
362
363        let constraint_type = get_constraint_type(constraint)?;
364        let raw_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
365            ffi::constraint_free(x as _)
366        });
367
368        constraint_add_args(instance, raw_constraint.ptr, constraint)?;
369        ffi::instance_addConstraint(instance, raw_constraint.ptr);
370    }
371
372    Ok(())
373}
374
375unsafe fn get_constraint_type(constraint: &Constraint) -> Result<u32, MinionError> {
376    match constraint {
377        Constraint::SumGeq(_, _) => Ok(ffi::ConstraintType_CT_GEQSUM),
378        Constraint::SumLeq(_, _) => Ok(ffi::ConstraintType_CT_LEQSUM),
379        Constraint::Ineq(_, _, _) => Ok(ffi::ConstraintType_CT_INEQ),
380        Constraint::Eq(_, _) => Ok(ffi::ConstraintType_CT_EQ),
381        Constraint::Difference(_, _) => Ok(ffi::ConstraintType_CT_DIFFERENCE),
382        Constraint::Div(_, _) => Ok(ffi::ConstraintType_CT_DIV),
383        Constraint::DivUndefZero(_, _) => Ok(ffi::ConstraintType_CT_DIV_UNDEFZERO),
384        Constraint::Modulo(_, _) => Ok(ffi::ConstraintType_CT_MODULO),
385        Constraint::ModuloUndefZero(_, _) => Ok(ffi::ConstraintType_CT_MODULO_UNDEFZERO),
386        Constraint::Pow(_, _) => Ok(ffi::ConstraintType_CT_POW),
387        Constraint::Product(_, _) => Ok(ffi::ConstraintType_CT_PRODUCT2),
388        Constraint::WeightedSumGeq(_, _, _) => Ok(ffi::ConstraintType_CT_WEIGHTGEQSUM),
389        Constraint::WeightedSumLeq(_, _, _) => Ok(ffi::ConstraintType_CT_WEIGHTLEQSUM),
390        Constraint::CheckAssign(_) => Ok(ffi::ConstraintType_CT_CHECK_ASSIGN),
391        Constraint::CheckGsa(_) => Ok(ffi::ConstraintType_CT_CHECK_GSA),
392        Constraint::ForwardChecking(_) => Ok(ffi::ConstraintType_CT_FORWARD_CHECKING),
393        Constraint::Reify(_, _) => Ok(ffi::ConstraintType_CT_REIFY),
394        Constraint::ReifyImply(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY),
395        Constraint::ReifyImplyQuick(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY_QUICK),
396        Constraint::WatchedAnd(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_AND),
397        Constraint::WatchedOr(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_OR),
398        Constraint::GacAllDiff(_) => Ok(ffi::ConstraintType_CT_GACALLDIFF),
399        Constraint::AllDiff(_) => Ok(ffi::ConstraintType_CT_ALLDIFF),
400        Constraint::AllDiffMatrix(_, _) => Ok(ffi::ConstraintType_CT_ALLDIFFMATRIX),
401        Constraint::WatchSumGeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_GEQSUM),
402        Constraint::WatchSumLeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LEQSUM),
403        Constraint::OccurrenceGeq(_, _, _) => Ok(ffi::ConstraintType_CT_GEQ_OCCURRENCE),
404        Constraint::OccurrenceLeq(_, _, _) => Ok(ffi::ConstraintType_CT_LEQ_OCCURRENCE),
405        Constraint::Occurrence(_, _, _) => Ok(ffi::ConstraintType_CT_OCCURRENCE),
406        Constraint::LitSumGeq(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_LITSUM),
407        Constraint::Gcc(_, _, _) => Ok(ffi::ConstraintType_CT_GCC),
408        Constraint::GccWeak(_, _, _) => Ok(ffi::ConstraintType_CT_GCCWEAK),
409        Constraint::LexLeqRv(_, _) => Ok(ffi::ConstraintType_CT_GACLEXLEQ),
410        Constraint::LexLeq(_, _) => Ok(ffi::ConstraintType_CT_LEXLEQ),
411        Constraint::LexLess(_, _) => Ok(ffi::ConstraintType_CT_LEXLESS),
412        Constraint::LexLeqQuick(_, _) => Ok(ffi::ConstraintType_CT_QUICK_LEXLEQ),
413        Constraint::LexLessQuick(_, _) => Ok(ffi::ConstraintType_CT_QUICK_LEXLEQ),
414        Constraint::WatchVecNeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_VECNEQ),
415        Constraint::WatchVecExistsLess(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_VEC_OR_LESS),
416        Constraint::Hamming(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_HAMMING),
417        Constraint::NotHamming(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_HAMMING),
418        Constraint::FrameUpdate(_, _, _, _, _) => Ok(ffi::ConstraintType_CT_FRAMEUPDATE),
419        Constraint::NegativeTable(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NEGATIVE_TABLE),
420        Constraint::Table(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_TABLE),
421        Constraint::GacSchema(_, _) => Ok(ffi::ConstraintType_CT_GACSCHEMA),
422        Constraint::LightTable(_, _) => Ok(ffi::ConstraintType_CT_LIGHTTABLE),
423        Constraint::Mddc(_, _) => Ok(ffi::ConstraintType_CT_MDDC),
424        Constraint::NegativeMddc(_, _) => Ok(ffi::ConstraintType_CT_NEGATIVEMDDC),
425        Constraint::Str2Plus(_, _) => Ok(ffi::ConstraintType_CT_STR),
426        Constraint::Max(_, _) => Ok(ffi::ConstraintType_CT_MAX),
427        Constraint::Min(_, _) => Ok(ffi::ConstraintType_CT_MIN),
428        Constraint::NvalueGeq(_, _) => Ok(ffi::ConstraintType_CT_GEQNVALUE),
429        Constraint::NvalueLeq(_, _) => Ok(ffi::ConstraintType_CT_LEQNVALUE),
430        Constraint::Element(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT),
431        Constraint::ElementOne(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT_ONE),
432        Constraint::ElementUndefZero(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT_UNDEFZERO),
433        Constraint::WatchElement(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT),
434        Constraint::WatchElementOne(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_ONE),
435        Constraint::WatchElementOneUndefZero(_, _, _) => {
436            Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_ONE_UNDEFZERO)
437        }
438        Constraint::WatchElementUndefZero(_, _, _) => {
439            Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_UNDEFZERO)
440        }
441        Constraint::WLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LIT),
442        Constraint::WNotLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOTLIT),
443        Constraint::WInIntervalSet(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_ININTERVALSET),
444        Constraint::WInRange(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_INRANGE),
445        Constraint::WInset(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_INSET),
446        Constraint::WNotInRange(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_INRANGE),
447        Constraint::WNotInset(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_INSET),
448        Constraint::Abs(_, _) => Ok(ffi::ConstraintType_CT_ABS),
449        Constraint::DisEq(_, _) => Ok(ffi::ConstraintType_CT_DISEQ),
450        Constraint::MinusEq(_, _) => Ok(ffi::ConstraintType_CT_MINUSEQ),
451        Constraint::GacEq(_, _) => Ok(ffi::ConstraintType_CT_GACEQ),
452        Constraint::WatchLess(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LESS),
453        Constraint::WatchNeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NEQ),
454        Constraint::True => Ok(ffi::ConstraintType_CT_TRUE),
455        Constraint::False => Ok(ffi::ConstraintType_CT_FALSE),
456
457        #[allow(unreachable_patterns)]
458        x => Err(MinionError::NotImplemented(format!(
459            "Constraint not implemented {x:?}",
460        ))),
461    }
462}
463
464unsafe fn constraint_add_args(
465    i: *mut ffi::ProbSpec_CSPInstance,
466    r_constr: *mut ffi::ProbSpec_ConstraintBlob,
467    constr: &Constraint,
468) -> Result<(), MinionError> {
469    match constr {
470        Constraint::SumGeq(lhs_vars, rhs_var) => {
471            read_list(i, r_constr, lhs_vars)?;
472            read_var(i, r_constr, rhs_var)?;
473            Ok(())
474        }
475        Constraint::SumLeq(lhs_vars, rhs_var) => {
476            read_list(i, r_constr, lhs_vars)?;
477            read_var(i, r_constr, rhs_var)?;
478            Ok(())
479        }
480        Constraint::Ineq(var1, var2, c) => {
481            read_var(i, r_constr, var1)?;
482            read_var(i, r_constr, var2)?;
483            read_constant(r_constr, c)?;
484            Ok(())
485        }
486        Constraint::Eq(var1, var2) => {
487            read_var(i, r_constr, var1)?;
488            read_var(i, r_constr, var2)?;
489            Ok(())
490        }
491        Constraint::Difference((a, b), c) => {
492            read_2_vars(i, r_constr, a, b)?;
493            read_var(i, r_constr, c)?;
494            Ok(())
495        }
496        Constraint::Div((a, b), c) => {
497            read_2_vars(i, r_constr, a, b)?;
498            read_var(i, r_constr, c)?;
499            Ok(())
500        }
501        Constraint::DivUndefZero((a, b), c) => {
502            read_2_vars(i, r_constr, a, b)?;
503            read_var(i, r_constr, c)?;
504            Ok(())
505        }
506        Constraint::Modulo((a, b), c) => {
507            read_2_vars(i, r_constr, a, b)?;
508            read_var(i, r_constr, c)?;
509            Ok(())
510        }
511        Constraint::ModuloUndefZero((a, b), c) => {
512            read_2_vars(i, r_constr, a, b)?;
513            read_var(i, r_constr, c)?;
514            Ok(())
515        }
516        Constraint::Pow((a, b), c) => {
517            read_2_vars(i, r_constr, a, b)?;
518            read_var(i, r_constr, c)?;
519            Ok(())
520        }
521        Constraint::Product((a, b), c) => {
522            read_2_vars(i, r_constr, a, b)?;
523            read_var(i, r_constr, c)?;
524            Ok(())
525        }
526        Constraint::WeightedSumGeq(a, b, c) => {
527            read_constant_list(r_constr, a)?;
528            read_list(i, r_constr, b)?;
529            read_var(i, r_constr, c)?;
530            Ok(())
531        }
532        Constraint::WeightedSumLeq(a, b, c) => {
533            read_constant_list(r_constr, a)?;
534            read_list(i, r_constr, b)?;
535            read_var(i, r_constr, c)?;
536            Ok(())
537        }
538        Constraint::CheckAssign(a) => {
539            read_constraint(i, r_constr, (**a).clone())?;
540            Ok(())
541        }
542        Constraint::CheckGsa(a) => {
543            read_constraint(i, r_constr, (**a).clone())?;
544            Ok(())
545        }
546        Constraint::ForwardChecking(a) => {
547            read_constraint(i, r_constr, (**a).clone())?;
548            Ok(())
549        }
550        Constraint::Reify(a, b) => {
551            read_constraint(i, r_constr, (**a).clone())?;
552            read_var(i, r_constr, b)?;
553            Ok(())
554        }
555        Constraint::ReifyImply(a, b) => {
556            read_constraint(i, r_constr, (**a).clone())?;
557            read_var(i, r_constr, b)?;
558            Ok(())
559        }
560        Constraint::ReifyImplyQuick(a, b) => {
561            read_constraint(i, r_constr, (**a).clone())?;
562            read_var(i, r_constr, b)?;
563            Ok(())
564        }
565        Constraint::WatchedAnd(a) => {
566            read_constraint_list(i, r_constr, a)?;
567            Ok(())
568        }
569        Constraint::WatchedOr(a) => {
570            read_constraint_list(i, r_constr, a)?;
571            Ok(())
572        }
573        Constraint::GacAllDiff(a) => {
574            read_list(i, r_constr, a)?;
575            Ok(())
576        }
577        Constraint::AllDiff(a) => {
578            read_list(i, r_constr, a)?;
579            Ok(())
580        }
581        Constraint::AllDiffMatrix(a, b) => {
582            read_list(i, r_constr, a)?;
583            read_constant(r_constr, b)?;
584            Ok(())
585        }
586        Constraint::WatchSumGeq(a, b) => {
587            read_list(i, r_constr, a)?;
588            read_constant(r_constr, b)?;
589            Ok(())
590        }
591        Constraint::WatchSumLeq(a, b) => {
592            read_list(i, r_constr, a)?;
593            read_constant(r_constr, b)?;
594            Ok(())
595        }
596        Constraint::OccurrenceGeq(a, b, c) => {
597            read_list(i, r_constr, a)?;
598            read_constant(r_constr, b)?;
599            read_constant(r_constr, c)?;
600            Ok(())
601        }
602        Constraint::OccurrenceLeq(a, b, c) => {
603            read_list(i, r_constr, a)?;
604            read_constant(r_constr, b)?;
605            read_constant(r_constr, c)?;
606            Ok(())
607        }
608        Constraint::Occurrence(a, b, c) => {
609            read_list(i, r_constr, a)?;
610            read_constant(r_constr, b)?;
611            read_var(i, r_constr, c)?;
612            Ok(())
613        }
614        Constraint::LexLess(a, b) => {
615            read_list(i, r_constr, a)?;
616            read_list(i, r_constr, b)?;
617            Ok(())
618        }
619        Constraint::LexLeq(a, b) => {
620            read_list(i, r_constr, a)?;
621            read_list(i, r_constr, b)?;
622            Ok(())
623        }
624        //Constraint::LitSumGeq(_, _, _) => todo!(),
625        //Constraint::Gcc(_, _, _) => todo!(),
626        //Constraint::GccWeak(_, _, _) => todo!(),
627        //Constraint::LexLeqRv(_, _) => todo!(),
628        //Constraint::LexLeqQuick(_, _) => todo!(),
629        //Constraint::LexLessQuick(_, _) => todo!(),
630        //Constraint::WatchVecNeq(_, _) => todo!(),
631        //Constraint::WatchVecExistsLess(_, _) => todo!(),
632        //Constraint::Hamming(_, _, _) => todo!(),
633        //Constraint::NotHamming(_, _, _) => todo!(),
634        //Constraint::FrameUpdate(_, _, _, _, _) => todo!(),
635        Constraint::NegativeTable(vars, tuple_list) | Constraint::Table(vars, tuple_list) => {
636            read_list(i, r_constr, vars)?;
637            read_tuple_list(r_constr, tuple_list)?;
638            Ok(())
639        }
640        //Constraint::GacSchema(_, _) => todo!(),
641        //Constraint::LightTable(_, _) => todo!(),
642        //Constraint::Mddc(_, _) => todo!(),
643        //Constraint::NegativeMddc(_, _) => todo!(),
644        //Constraint::Str2Plus(_, _) => todo!(),
645        //Constraint::Max(_, _) => todo!(),
646        //Constraint::Min(_, _) => todo!(),
647        //Constraint::NvalueGeq(_, _) => todo!(),
648        //Constraint::NvalueLeq(_, _) => todo!(),
649        //Constraint::Element(_, _, _) => todo!(),
650        //Constraint::ElementUndefZero(_, _, _) => todo!(),
651        //Constraint::WatchElement(_, _, _) => todo!(),
652        //Constraint::WatchElementOne(_, _, _) => todo!(),
653        Constraint::ElementOne(vec, j, e) => {
654            read_list(i, r_constr, vec)?;
655            read_var(i, r_constr, j)?;
656            read_var(i, r_constr, e)?;
657            Ok(())
658        }
659        //Constraint::WatchElementOneUndefZero(_, _, _) => todo!(),
660        //Constraint::WatchElementUndefZero(_, _, _) => todo!(),
661        Constraint::WLiteral(a, b) => {
662            read_var(i, r_constr, a)?;
663            read_constant(r_constr, b)?;
664            Ok(())
665        }
666        //Constraint::WNotLiteral(_, _) => todo!(),
667        Constraint::WInIntervalSet(var, consts) => {
668            read_var(i, r_constr, var)?;
669            read_constant_list(r_constr, consts)?;
670            Ok(())
671        }
672        //Constraint::WInRange(_, _) => todo!(),
673        Constraint::WInset(a, b) => {
674            read_var(i, r_constr, a)?;
675            read_constant_list(r_constr, b)?;
676            Ok(())
677        }
678        //Constraint::WNotInRange(_, _) => todo!(),
679        //Constraint::WNotInset(_, _) => todo!(),
680        Constraint::Abs(a, b) => {
681            read_var(i, r_constr, a)?;
682            read_var(i, r_constr, b)?;
683            Ok(())
684        }
685        Constraint::DisEq(a, b) => {
686            read_var(i, r_constr, a)?;
687            read_var(i, r_constr, b)?;
688            Ok(())
689        }
690        Constraint::MinusEq(a, b) => {
691            read_var(i, r_constr, a)?;
692            read_var(i, r_constr, b)?;
693            Ok(())
694        }
695        //Constraint::GacEq(_, _) => todo!(),
696        //Constraint::WatchLess(_, _) => todo!(),
697        // TODO: ensure that this is a bool?
698        Constraint::WatchNeq(a, b) => {
699            read_var(i, r_constr, a)?;
700            read_var(i, r_constr, b)?;
701            Ok(())
702        }
703
704        Constraint::True => Ok(()),
705        Constraint::False => Ok(()),
706        #[allow(unreachable_patterns)]
707        x => Err(MinionError::NotImplemented(format!("{x:?}"))),
708    }
709}
710
711// DO NOT call manually - this assumes that all needed vars are already in the symbol table.
712// TODO not happy with this just assuming the name is in the symbol table
713unsafe fn read_list(
714    instance: *mut ffi::ProbSpec_CSPInstance,
715    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
716    vars: &Vec<Var>,
717) -> Result<(), MinionError> {
718    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
719    for var in vars {
720        let raw_var = match var {
721            Var::NameRef(name) => {
722                let c_str = CString::new(name.clone()).map_err(|_| {
723                    anyhow!(
724                        "Variable name {:?} contains a null character.",
725                        name.clone()
726                    )
727                })?;
728                get_var_by_name_checked(instance, c_str.as_ptr())?
729            }
730            Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
731        };
732
733        ffi::vec_var_push_back(raw_vars.ptr, raw_var);
734    }
735
736    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
737
738    Ok(())
739}
740
741unsafe fn read_var(
742    instance: *mut ffi::ProbSpec_CSPInstance,
743    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
744    var: &Var,
745) -> Result<(), MinionError> {
746    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));
747    let raw_var = match var {
748        Var::NameRef(name) => {
749            let c_str = CString::new(name.clone()).map_err(|_| {
750                anyhow!(
751                    "Variable name {:?} contains a null character.",
752                    name.clone()
753                )
754            })?;
755            get_var_by_name_checked(instance, c_str.as_ptr())?
756        }
757        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
758    };
759
760    ffi::vec_var_push_back(raw_vars.ptr, raw_var);
761    ffi::constraint_addList(raw_constraint, raw_vars.ptr);
762
763    Ok(())
764}
765
766unsafe fn read_2_vars(
767    instance: *mut ffi::ProbSpec_CSPInstance,
768    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
769    var1: &Var,
770    var2: &Var,
771) -> Result<(), MinionError> {
772    let mut raw_var = match var1 {
773        Var::NameRef(name) => {
774            let c_str = CString::new(name.clone()).map_err(|_| {
775                anyhow!(
776                    "Variable name {:?} contains a null character.",
777                    name.clone()
778                )
779            })?;
780            get_var_by_name_checked(instance, c_str.as_ptr())?
781        }
782        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
783    };
784    let mut raw_var2 = match var2 {
785        Var::NameRef(name) => {
786            let c_str = CString::new(name.clone()).map_err(|_| {
787                anyhow!(
788                    "Variable name {:?} contains a null character.",
789                    name.clone()
790                )
791            })?;
792            get_var_by_name_checked(instance, c_str.as_ptr())?
793        }
794        Var::ConstantAsVar(n) => ffi::constantAsVar(*n),
795    };
796    // todo: does this move or copy? I am confus!
797    // TODO need to mkae the semantics of move vs copy / ownership clear in libminion!!
798    // This shouldve leaked everywhere by now but i think libminion copies stuff??
799    ffi::constraint_addTwoVars(raw_constraint, &mut raw_var, &mut raw_var2);
800    Ok(())
801}
802
803unsafe fn read_constant(
804    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
805    constant: &Constant,
806) -> Result<(), MinionError> {
807    let val: i32 = match constant {
808        Constant::Integer(n) => Ok(*n),
809        Constant::Bool(true) => Ok(1),
810        Constant::Bool(false) => Ok(0),
811        x => Err(MinionError::NotImplemented(format!("{x:?}"))),
812    }?;
813
814    ffi::constraint_addConstant(raw_constraint, val);
815
816    Ok(())
817}
818
819unsafe fn read_constant_list(
820    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
821    constants: &[Constant],
822) -> Result<(), MinionError> {
823    let raw_consts = Scoped::new(ffi::vec_int_new(), |x| ffi::vec_int_free(x as _));
824
825    for constant in constants.iter() {
826        let val = match constant {
827            Constant::Integer(n) => Ok(*n),
828            Constant::Bool(true) => Ok(1),
829            Constant::Bool(false) => Ok(0),
830            #[allow(unreachable_patterns)] // TODO: can there be other types?
831            x => Err(MinionError::NotImplemented(format!("{x:?}"))),
832        }?;
833
834        ffi::vec_int_push_back(raw_consts.ptr, val);
835    }
836
837    ffi::constraint_addConstantList(raw_constraint, raw_consts.ptr);
838    Ok(())
839}
840
841//TODO: check if the inner constraint is listed in the model or not?
842//Does this matter?
843// TODO: type-check inner constraints vars and tuples and so on?
844unsafe fn read_constraint(
845    instance: *mut ffi::ProbSpec_CSPInstance,
846    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
847    inner_constraint: Constraint,
848) -> Result<(), MinionError> {
849    let constraint_type = get_constraint_type(&inner_constraint)?;
850    let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
851        ffi::constraint_free(x as _)
852    });
853
854    constraint_add_args(instance, raw_inner_constraint.ptr, &inner_constraint)?;
855
856    ffi::constraint_addConstraint(raw_constraint, raw_inner_constraint.ptr);
857    Ok(())
858}
859
860unsafe fn read_constraint_list(
861    instance: *mut ffi::ProbSpec_CSPInstance,
862    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
863    inner_constraints: &[Constraint],
864) -> Result<(), MinionError> {
865    let raw_inners = Scoped::new(ffi::vec_constraints_new(), |x| {
866        ffi::vec_constraints_free(x as _)
867    });
868    for inner_constraint in inner_constraints.iter() {
869        let constraint_type = get_constraint_type(inner_constraint)?;
870        let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {
871            ffi::constraint_free(x as _)
872        });
873
874        constraint_add_args(instance, raw_inner_constraint.ptr, inner_constraint)?;
875        ffi::vec_constraints_push_back(raw_inners.ptr, raw_inner_constraint.ptr);
876    }
877
878    ffi::constraint_addConstraintList(raw_constraint, raw_inners.ptr);
879    Ok(())
880}
881
882unsafe fn read_tuple_list(
883    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,
884    tuples: &Vec<Tuple>,
885) -> Result<(), MinionError> {
886    // a tuple list is just a vec<vec<int>>, where each inner vec is a tuple
887    let raw_tuples = Scoped::new(ffi::vec_vec_int_new(), |x| ffi::vec_vec_int_free(x as _));
888    for tuple in tuples {
889        let raw_tuple = Scoped::new(ffi::vec_int_new(), |x| ffi::vec_int_free(x as _));
890        for constant in tuple.iter() {
891            let val = match constant {
892                Constant::Integer(n) => Ok(*n),
893                Constant::Bool(true) => Ok(1),
894                Constant::Bool(false) => Ok(0),
895                #[allow(unreachable_patterns)] // TODO: can there be other types?
896                x => Err(MinionError::NotImplemented(format!("{:?}", x))),
897            }?;
898
899            ffi::vec_int_push_back(raw_tuple.ptr, val);
900        }
901
902        ffi::vec_vec_int_push_back_ptr(raw_tuples.ptr, raw_tuple.ptr);
903    }
904
905    // `constraint_setTuples` transfers ownership of `TupleList` into Minion via shared_ptr.
906    // Do not wrap this pointer in `Scoped` or it will be freed too early.
907    let raw_tuple_list = ffi::tupleList_new(raw_tuples.ptr);
908    ffi::constraint_setTuples(raw_constraint, raw_tuple_list);
909
910    Ok(())
911}
minion_sys/run.rs

minion_sys/
run.rs
