minion_sys/
run.rs

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

minion_sys/
run.rs
