choco_solver/
constraint.rs

1use std::borrow::Borrow;
2use std::ffi::CStr;
3
4use crate::CHOCO_BACKEND;
5use crate::CHOCO_LIB;
6use crate::Sealed;
7use crate::SolverError;
8use crate::model::Model;
9use crate::utils::{Handle, HandleT, ModelObject, make_constraint_array};
10use crate::variables::{BoolVar, IntVar};
11
12/// Comparison operators for arithmetic constraints.
13#[derive(Debug, Clone, Copy, PartialEq, Eq)]
14pub enum EqualityOperator {
15    Eq,
16    Neq,
17    Lt,
18    Leq,
19    Gt,
20    Geq,
21}
22
23impl EqualityOperator {
24    #[must_use]
25    pub fn to_cstr(&self) -> &CStr {
26        match self {
27            EqualityOperator::Eq => c"=",
28            EqualityOperator::Neq => c"!=",
29            EqualityOperator::Lt => c"<",
30            EqualityOperator::Leq => c"<=",
31            EqualityOperator::Gt => c">",
32            EqualityOperator::Geq => c">=",
33        }
34    }
35}
36
37/// Arithmetic operators used in constraints (addition, subtraction, multiplication, division).
38#[derive(Debug, Clone, Copy, PartialEq, Eq)]
39pub enum ArithmeticOperator {
40    Sum,
41    Sub,
42    Mul,
43    Div,
44}
45
46impl ArithmeticOperator {
47    #[must_use]
48    pub fn to_cstr(&self) -> &CStr {
49        match self {
50            ArithmeticOperator::Sum => c"+",
51            ArithmeticOperator::Sub => c"-",
52            ArithmeticOperator::Mul => c"*",
53            ArithmeticOperator::Div => c"/",
54        }
55    }
56}
57
58/// The operational status of a constraint.
59#[derive(Debug, Clone, Copy, PartialEq, Eq)]
60pub enum ConstraintStatus {
61    /// Constraint is not yet posted or reified.
62    FREE,
63    /// Constraint has been posted to the solver.
64    POSTED,
65    /// Constraint has been converted to a boolean variable.
66    REIFIED,
67}
68
69impl TryFrom<i32> for ConstraintStatus {
70    type Error = ();
71
72    fn try_from(value: i32) -> Result<Self, Self::Error> {
73        match value {
74            0 => Ok(ConstraintStatus::FREE),
75            1 => Ok(ConstraintStatus::POSTED),
76            2 => Ok(ConstraintStatus::REIFIED),
77            _ => Err(()),
78        }
79    }
80}
81
82/// Represents the satisfaction state of a constraint.
83///
84/// This enum indicates whether a constraint is satisfied, not satisfied,
85/// or if it is not yet possible to determine its satisfaction state.
86#[derive(Debug, Clone, Copy, PartialEq, Eq)]
87pub enum ESat {
88    /// The constraint is satisfied.
89    True,
90    /// The constraint is not satisfied.
91    False,
92    /// The satisfaction state cannot be determined yet.
93    Undefined,
94}
95
96/// Trait for creating equality constraints between variables or constants.
97///
98/// Provides methods to create equality (`eq`) and inequality (`ne`) constraints.
99pub trait ConstraintEquality<'model, Rhs> {
100    /// Creates an equality constraint (=).
101    fn eq(self, other: Rhs) -> Constraint<'model>;
102    /// Creates an inequality constraint (!=).
103    fn ne(self, other: Rhs) -> Constraint<'model>;
104}
105
106/// Trait for creating modulo/remainder constraints.
107pub trait ArithmConstraint<'model, MOD, RES> {
108    /// Creates a modulo constraint: `self` % `modulo` = `res`.
109    fn modulo(&'model self, modulo: MOD, res: RES) -> Constraint<'model>;
110}
111
112/// A constraint attached to a [`Model`].
113///
114/// Constraints can be posted, reified, or combined to express relations
115/// between variables in the model.
116pub struct Constraint<'model> {
117    handle: Handle,
118    model: &'model Model,
119}
120
121impl HandleT for Constraint<'_> {
122    fn get_raw_handle(&self) -> *mut std::os::raw::c_void {
123        self.handle.get_raw_handle()
124    }
125}
126impl<'model> ModelObject<'model> for Constraint<'model> {
127    fn get_model(&self) -> &'model Model {
128        self.model
129    }
130}
131
132impl<'model> Constraint<'model> {
133    /// # Safety
134    /// - The caller must ensure that the handle is valid constraint pointer and the backend is initialized.
135    pub(crate) unsafe fn new(handle: *mut std::os::raw::c_void, model: &'model Model) -> Self {
136        Constraint {
137            handle: Handle::new(handle),
138            model,
139        }
140    }
141
142    pub fn post(&self) -> Result<(), SolverError> {
143        if self.status() != ConstraintStatus::FREE {
144            Err(SolverError::NotFreeConstraint)
145        } else {
146            // Safety:
147            // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
148            CHOCO_BACKEND.with(|backend| unsafe {
149                CHOCO_LIB.Java_org_chocosolver_capi_ConstraintApi_post(
150                    backend.thread,
151                    self.get_raw_handle(),
152                )
153            });
154            Ok(())
155        }
156    }
157
158    /// Reifies the constraint, i.e., returns a BoolVar whose instantiation in a solution
159    /// corresponds to the satisfaction state of the constraint in this solution.
160    ///
161    /// # Returns
162    ///
163    /// A `BoolVar` that encodes the satisfaction state of the constraint.
164    ///
165    /// # Panics
166    ///
167    /// Panics if the backend fails to reify the constraint and returns a null handle.
168    #[must_use]
169    pub fn reify(&self) -> BoolVar<'model> {
170        CHOCO_BACKEND.with(|backend|
171            // Safety:
172        // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
173            unsafe {
174           let var_handle = CHOCO_LIB.Java_org_chocosolver_capi_ConstraintApi_reify(
175                backend.thread,
176                self.get_raw_handle(),
177            );
178             assert!(!var_handle.is_null(), "Failed to reify constraint");
179             BoolVar::from_raw_handle(var_handle, self.model)})
180    }
181
182    /// Reifies the constraint with a given BoolVar whose instantiation in a solution
183    /// corresponds to the satisfaction state of the constraint in this solution.
184    ///
185    /// # Arguments
186    ///
187    /// * `boolvar` - The BoolVar to reify with.
188    pub fn reify_with(&self, boolvar: &BoolVar<'model>) {
189        // Safety:
190        // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
191        CHOCO_BACKEND.with(|backend| unsafe {
192            CHOCO_LIB.Java_org_chocosolver_capi_ConstraintApi_reify_with(
193                backend.thread,
194                self.get_raw_handle(),
195                boolvar.get_raw_handle(),
196            )
197        });
198    }
199
200    /// Encapsulates this constraint in an implication relationship.
201    /// The truth value of this constraint implies the truth value of the BoolVar.
202    ///
203    /// # Arguments
204    ///
205    /// * `boolvar` - The BoolVar that is implied by this constraint.
206    pub fn implies(&self, boolvar: &BoolVar<'model>) {
207        // Safety:
208        // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
209        CHOCO_BACKEND.with(|backend| unsafe {
210            CHOCO_LIB.Java_org_chocosolver_capi_ConstraintApi_implies(
211                backend.thread,
212                self.get_raw_handle(),
213                boolvar.get_raw_handle(),
214            )
215        });
216    }
217
218    /// Encapsulates this constraint in an implication relationship.
219    /// Represents half-reification of the constraint. If the BoolVar is true,
220    /// then the constraint must be satisfied.
221    ///
222    /// # Arguments
223    ///
224    /// * `boolvar` - The BoolVar that implies this constraint.
225    pub fn implied_by(&self, boolvar: &BoolVar<'model>) {
226        // Safety:
227        // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
228        CHOCO_BACKEND.with(|backend| unsafe {
229            CHOCO_LIB.Java_org_chocosolver_capi_ConstraintApi_implied_by(
230                backend.thread,
231                self.get_raw_handle(),
232                boolvar.get_raw_handle(),
233            )
234        });
235    }
236
237    /// Check whether the constraint is satisfied.
238    ///
239    /// Returns `ESat::True` if the constraint is satisfied, `ESat::False` if it is not,
240    /// or `ESat::Undefined` if it is not yet possible to determine whether the constraint
241    /// is satisfied or not.
242    ///
243    /// # Note
244    ///
245    /// This method can be useful to verify whether a constraint is satisfied (or not)
246    /// regardless of the variables' instantiation.
247    ///
248    /// # Returns
249    ///
250    /// The satisfaction state of the constraint.
251    #[must_use]
252    pub fn is_satisfied(&self) -> ESat {
253        // Safety:
254        // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
255        let state = CHOCO_BACKEND.with(|backend| unsafe {
256            CHOCO_LIB.Java_org_chocosolver_capi_ConstraintApi_is_satisfied(
257                backend.thread,
258                self.get_raw_handle(),
259            )
260        });
261        match state {
262            0 => ESat::False,
263            1 => ESat::True,
264            _ => ESat::Undefined,
265        }
266    }
267
268    #[must_use]
269    pub fn status(&self) -> ConstraintStatus {
270        // Safety:
271        // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
272        let status_code = CHOCO_BACKEND.with(|backend| unsafe {
273            CHOCO_LIB.Java_org_chocosolver_capi_ConstraintApi_getStatus(
274                backend.thread,
275                self.get_raw_handle(),
276            )
277        });
278        match ConstraintStatus::try_from(status_code) {
279            Ok(status) => status,
280            Err(_) => panic!("Unknown constraint status code: {}", status_code),
281        }
282    }
283    /// Posts a constraint ensuring that if self constraint is satisfied , then `then_constraint`
284    /// must be satisfied as well. Otherwise, `else_constraint` must be satisfied.
285    pub fn if_then_else(
286        &self,
287        then_constraint: &Constraint<'model>,
288        else_constraint: &Constraint<'model>,
289    ) {
290        // Safety:
291        // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
292        CHOCO_BACKEND.with(|backend| unsafe {
293            CHOCO_LIB.Java_org_chocosolver_capi_ReificationApi_if_then_else(
294                backend.thread,
295                self.model.get_raw_handle(),
296                self.get_raw_handle(),
297                then_constraint.get_raw_handle(),
298                else_constraint.get_raw_handle(),
299            )
300        });
301    }
302    /// Creates an if-then constraint: self constraint -> then_constraint.
303    pub fn if_then(&self, then_constraint: &Constraint<'model>) {
304        // Safety:
305        // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
306        CHOCO_BACKEND.with(|backend| unsafe {
307            CHOCO_LIB.Java_org_chocosolver_capi_ReificationApi_if_then(
308                backend.thread,
309                self.model.get_raw_handle(),
310                self.get_raw_handle(),
311                then_constraint.get_raw_handle(),
312            )
313        });
314    }
315
316    /// Posts an equivalence constraint stating that:
317    /// `self` constraint is satisfied (or true) <=> `constraint` is satisfied.
318    pub fn if_only_if(&self, constraint: &Constraint<'model>) {
319        // Safety:
320        // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
321        CHOCO_BACKEND.with(|backend| unsafe {
322            CHOCO_LIB.Java_org_chocosolver_capi_ReificationApi_if_only_if(
323                backend.thread,
324                self.model.get_raw_handle(),
325                self.get_raw_handle(),
326                constraint.get_raw_handle(),
327            )
328        });
329    }
330}
331
332/// # Safety
333/// - This trait assumes that the implementor use this only on IntVar or i32 types.
334unsafe trait IntoRawIntVarHandleT: Copy {
335    fn into_raw_ptr(self, model: &Model) -> *mut std::os::raw::c_void;
336}
337
338/// # SAFETY:
339/// - Implemented on &IntVar and i32 only, as required by the trait safety comment.
340unsafe impl<'model, T: Borrow<IntVar<'model>>> IntoRawIntVarHandleT for &T {
341    fn into_raw_ptr(self, _model: &Model) -> *mut std::os::raw::c_void {
342        self.borrow().get_raw_handle()
343    }
344}
345/// # SAFETY:
346/// - Implemented on &IntVar and i32 only, as required by the trait safety comment.
347/// - the integer variable is not actually destroyed after use, but this is safe as the backend will manage memory and the temporary IntVar will be garbage collected when the model is disposed.
348unsafe impl IntoRawIntVarHandleT for i32 {
349    fn into_raw_ptr(self, model: &Model) -> *mut std::os::raw::c_void {
350        // Safety:
351        // Safe because IntVar is created from Model and therefore the backend is initialized, model handle is valid.
352        CHOCO_BACKEND.with(|backend| unsafe {
353            CHOCO_LIB.Java_org_chocosolver_capi_IntVarApi_intVar_i(
354                backend.thread,
355                model.get_raw_handle(),
356                self,
357            )
358        })
359    }
360}
361
362pub(crate) trait ConstraintArithmT<'model> {
363    fn create(&self) -> Constraint<'model>;
364}
365
366impl<'model, X: Borrow<IntVar<'model>>> ConstraintArithmT<'model> for (X, EqualityOperator, i32) {
367    fn create(&self) -> Constraint<'model> {
368        let int_var = self.0.borrow();
369        CHOCO_BACKEND.with(|backend|
370            // Safety:
371            // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
372            unsafe {
373            let constraint_handle = CHOCO_LIB
374                .Java_org_chocosolver_capi_ConstraintApi_arithm_iv_cst(
375                    backend.thread,
376                    int_var.get_model().get_raw_handle(),
377                    int_var.get_raw_handle(),
378                    self.1.to_cstr().as_ptr().cast_mut(),
379                    self.2,
380                );
381assert!(
382            !constraint_handle.is_null(),
383            "Invalid parameters combination for arithm constraint. Please refer to the doc"
384        );
385        Constraint::new(constraint_handle, int_var.get_model())})
386    }
387}
388
389impl<'model, X: Borrow<IntVar<'model>>, Y: Borrow<IntVar<'model>>> ConstraintArithmT<'model>
390    for (X, EqualityOperator, Y)
391{
392    fn create(&self) -> Constraint<'model> {
393        let x_var = self.0.borrow();
394        let y_var = self.2.borrow();
395        CHOCO_BACKEND.with(|backend|
396// Safety:
397        // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
398            unsafe {
399            let constraint_handle = CHOCO_LIB
400                .Java_org_chocosolver_capi_ConstraintApi_arithm_iv_iv(
401                    backend.thread,
402                    x_var.get_model().get_raw_handle(),
403                    x_var.get_raw_handle(),
404                    self.1.to_cstr().as_ptr().cast_mut(),
405                    y_var.get_raw_handle(),
406                );
407assert!(
408            !constraint_handle.is_null(),
409            "Invalid parameters combination for arithm constraint. Please refer to the doc"
410        );
411        Constraint::new(constraint_handle, x_var.get_model())})
412    }
413}
414
415impl<'model, X: Borrow<IntVar<'model>>, Y: IntoRawIntVarHandleT> ConstraintArithmT<'model>
416    for (X, EqualityOperator, Y, ArithmeticOperator, &IntVar<'model>)
417{
418    fn create(&self) -> Constraint<'model> {
419        let x_var = self.0.borrow();
420        let yy = self.2.into_raw_ptr(x_var.get_model());
421        assert!(
422            !yy.is_null(),
423            "Failed to convert parameter to raw pointer for arithm constraint"
424        );
425
426        CHOCO_BACKEND.with(|backend|
427// Safety:
428        // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
429            unsafe {
430            let constraint_handle = CHOCO_LIB
431                .Java_org_chocosolver_capi_ConstraintApi_arithm_iv_iv_iv(
432                    backend.thread,
433                    x_var.get_model().get_raw_handle(),
434                    x_var.get_raw_handle(),
435                    self.1.to_cstr().as_ptr().cast_mut(),
436                    yy,
437                    self.3.to_cstr().as_ptr().cast_mut(),
438                    self.4.get_raw_handle(),
439                );
440                assert!(
441            !constraint_handle.is_null(),
442            "Invalid parameters combination for arithm constraint. Please refer to the doc"
443        );
444        Constraint::new(constraint_handle, x_var.get_model())})
445    }
446}
447impl<'model, X: Borrow<IntVar<'model>>, Y: IntoRawIntVarHandleT> ConstraintArithmT<'model>
448    for (X, EqualityOperator, Y, ArithmeticOperator, i32)
449{
450    fn create(&self) -> Constraint<'model> {
451        let x_var = self.0.borrow();
452        let yy = self.2.into_raw_ptr(x_var.get_model());
453
454        CHOCO_BACKEND.with(|backend|
455            // Safety:
456            // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
457            unsafe {
458            let constraint_handle = CHOCO_LIB
459                .Java_org_chocosolver_capi_ConstraintApi_arithm_iv_iv_cst(
460                    backend.thread,
461                    x_var.get_model().get_raw_handle(),
462                    x_var.get_raw_handle(),
463                    self.1.to_cstr().as_ptr().cast_mut(),
464                    yy,
465                    self.3.to_cstr().as_ptr().cast_mut(),
466                    self.4,
467                );
468                assert!(
469            !constraint_handle.is_null(),
470            "Invalid parameters combination for arithm constraint. Please refer to the doc");
471        Constraint::new(constraint_handle, x_var.get_model())
472        })
473    }
474}
475
476impl<'model, X: Borrow<IntVar<'model>>, Y: IntoRawIntVarHandleT> ConstraintArithmT<'model>
477    for (X, ArithmeticOperator, Y, EqualityOperator, &IntVar<'model>)
478{
479    fn create(&self) -> Constraint<'model> {
480        let x_var = self.0.borrow();
481        let yy = self.2.into_raw_ptr(x_var.get_model());
482        assert!(
483            !yy.is_null(),
484            "Failed to convert parameter to raw pointer for arithm constraint"
485        );
486
487        CHOCO_BACKEND.with(|backend|
488            // Safety:
489        // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
490             unsafe {
491            let constraint_handle =CHOCO_LIB
492                .Java_org_chocosolver_capi_ConstraintApi_arithm_iv_iv_iv(
493                    backend.thread,
494                    x_var.get_model().get_raw_handle(),
495                    x_var.get_raw_handle(),
496                    self.1.to_cstr().as_ptr().cast_mut(),
497                    yy,
498                    self.3.to_cstr().as_ptr().cast_mut(),
499                    self.4.get_raw_handle(),
500                );
501                assert!(
502            !constraint_handle.is_null(),
503            "Invalid parameters combination for arithm constraint. Please refer to the doc");
504        Constraint::new(constraint_handle, x_var.get_model())
505        })
506    }
507}
508impl<'model, X: Borrow<IntVar<'model>>, Y: IntoRawIntVarHandleT> ConstraintArithmT<'model>
509    for (X, ArithmeticOperator, Y, EqualityOperator, i32)
510{
511    fn create(&self) -> Constraint<'model> {
512        let x_var = self.0.borrow();
513        let yy = self.2.into_raw_ptr(x_var.get_model());
514
515        CHOCO_BACKEND.with(|backend|
516            // Safety:
517            // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
518            unsafe {
519             let constraint_handle = CHOCO_LIB
520                .Java_org_chocosolver_capi_ConstraintApi_arithm_iv_iv_cst(
521                    backend.thread,
522                    x_var.get_model().get_raw_handle(),
523                    x_var.get_raw_handle(),
524                    self.1.to_cstr().as_ptr().cast_mut(),
525                    yy,
526                    self.3.to_cstr().as_ptr().cast_mut(),
527                    self.4,
528                );
529        assert!(
530            !constraint_handle.is_null(),
531            "Invalid parameters combination for arithm constraint. Please refer to the doc");
532        Constraint::new(constraint_handle, x_var.get_model())
533        })
534    }
535}
536#[allow(private_bounds)]
537/// Logical operations on slices of Constraints/BoolVars
538pub trait ConstraintArrayLogicOps<'model>: Sealed {
539    /// AND of Constraints
540    /// # Arguments
541    /// * `constraints` - slice of Constraints/BoolVars
542    /// # Returns
543    /// Constraint representing the AND of the Constraints/BoolVars
544    /// # Panic:
545    /// if slice is empty
546    fn and(self) -> Constraint<'model>;
547    /// OR of Constraints
548    /// # Arguments
549    /// * `constraints` - slice of Constraints/BoolVars
550    /// # Returns
551    /// Constraint representing the OR of the Constraints/BoolVars
552    /// # Panic:
553    /// if slice is empty
554    fn or(self) -> Constraint<'model>;
555}
556
557impl<'model, Q: Borrow<Constraint<'model>> + Sealed> ConstraintArrayLogicOps<'model> for &[Q] {
558    fn and(self) -> Constraint<'model> {
559        let array_handle = make_constraint_array(self);
560        let model = self
561            .first()
562            .expect("Slice shall contains at least one element")
563            .borrow()
564            .get_model();
565        CHOCO_BACKEND.with(|backend|
566            // Safety:
567            // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
568            unsafe {
569            let constraint_handle =CHOCO_LIB
570                .Java_org_chocosolver_capi_ConstraintApi_and_cs_cs(
571                    backend.thread,
572                    model.get_raw_handle(),
573                    array_handle,
574                );
575        assert!(
576            !constraint_handle.is_null(),
577            "Failed to create AND constraint"
578        );
579        Constraint::new(constraint_handle, model)
580    })
581    }
582    fn or(self) -> Constraint<'model> {
583        let array_handle = make_constraint_array(self);
584        let model = self
585            .first()
586            .expect("Slice shall contains at least one element")
587            .borrow()
588            .get_model();
589        CHOCO_BACKEND.with(|backend|
590            // Safety:
591            // Safe because Constraint is created from Model and therefore the backend is initialized and model handle is valid.
592            unsafe {
593            let constraint_handle = CHOCO_LIB
594                .Java_org_chocosolver_capi_ConstraintApi_or_cs_cs(
595                    backend.thread,
596                    model.get_raw_handle(),
597                    array_handle,
598                );
599        assert!(!constraint_handle.is_null(),
600            "Failed to create OR constraint"
601        );
602        Constraint::new(constraint_handle, model)
603        })
604    }
605}
606
607#[cfg(test)]
608mod tests;
choco_solver/constraint.rs

choco_solver/
constraint.rs
