Skip to main content

choco_solver/
solver.rs

1#![allow(clippy::indexing_slicing)]
2mod criterion;
3use crate::{
4    CHOCO_BACKEND, CHOCO_LIB, Model, Solution, SolverError,
5    utils::{Handle, HandleT, ModelObject},
6};
7
8pub use criterion::Criterion;
9/// A solver instance associated with a [`Model`].
10///
11/// Provides solution search and propagation utilities for the model.
12pub struct Solver<'model> {
13    handle: Handle,
14    model: &'model Model,
15}
16
17impl<'model> Solver<'model> {
18    pub(crate) fn new(model: &'model Model) -> Self {
19        CHOCO_BACKEND.with(|backend|
20        // Safety:
21        // create solver function are guarantee to be called after chocosolver_init
22        // because Model can be created only after that by the ChocoBackend lazy initialization.
23        unsafe {
24            let handle = CHOCO_LIB.Java_org_chocosolver_capi_ModelApi_getSolver(backend.thread, model.get_raw_handle());
25            assert!(
26                !handle.is_null(),
27                "Failed to create solver: received null handle"
28            );
29            Solver {
30                handle: Handle::new(handle),
31                model,
32            }
33        })
34    }
35
36    /// Sets the time limit for the solver in milliseconds.
37    ///
38    /// # Panics
39    ///
40    /// Panics if `time_limit_ms` is negative.
41    pub fn set_time_limit(&self, time_limit_ms: i64) {
42        assert!(
43            !time_limit_ms.is_negative(),
44            "Time limit must be non-negative"
45        );
46        CHOCO_BACKEND.with(|backend|
47        // Safety:
48        // Safe because Solver instances are created from valid backend handles.
49        unsafe {
50            CHOCO_LIB.Java_org_chocosolver_capi_SolverApi_limit_time_ms(backend.thread, self.get_raw_handle(), time_limit_ms);
51        })
52    }
53
54    #[must_use]
55    pub fn find_solution(&self, criterions: &Criterion) -> Option<Solution> {
56        CHOCO_BACKEND.with(|backend|
57        // Safety:
58        // Safe because Solver instances are created from valid backend handles.
59        unsafe {
60            let criterion_array = criterion::make_criterion_var_array(criterions, self.model);
61            let solution_handle =
62                CHOCO_LIB.Java_org_chocosolver_capi_SolverApi_find_solution(backend.thread, self.get_raw_handle(), criterion_array);
63            if solution_handle.is_null() {
64                None
65            } else {
66                Some(Solution::new(solution_handle))
67            }
68        })
69    }
70
71    ///
72    ///    Propagates constraints and related events through the constraint network until a fix point is find,
73    ///    or a contradiction is detected.
74    /// # Returns
75    /// SolverError::FoundContradiction if a contradiction is detected during propagation.
76    pub fn propagate(&self) -> Result<(), SolverError> {
77        CHOCO_BACKEND.with(|backend|
78        // Safety:
79        // Safe because Solver instances are created from valid backend handles.
80        unsafe {
81            if CHOCO_LIB.Java_org_chocosolver_capi_SolverApi_propagate(backend.thread, self.get_raw_handle()) != 0 {
82                Ok(())
83            } else {
84                Err(SolverError::FoundContradiction)
85            }
86        })
87    }
88}
89
90impl HandleT for Solver<'_> {
91    fn get_raw_handle(&self) -> *mut std::os::raw::c_void {
92        self.handle.get_raw_handle()
93    }
94}
95
96impl<'model> ModelObject<'model> for Solver<'model> {
97    fn get_model(&self) -> &'model Model {
98        self.model
99    }
100}
101
102#[cfg(test)]
103mod tests {
104    use crate::utils::ModelObject;
105    use crate::*;
106    use crate::{EqualityOperator, Model, SolverError};
107    #[test]
108    fn test_solver_contradiction_propagate() {
109        let model = Model::new(None);
110        let solver = model.solver();
111        let var1 = model.int_var_bounded(0, 10, Some("var1"), None);
112
113        let constraint = var1.arithm(EqualityOperator::Eq, 25);
114        constraint.post().unwrap();
115        let result = solver.propagate();
116        assert!(matches!(result, Err(SolverError::FoundContradiction)));
117    }
118
119    #[test]
120    fn test_solver_model_object() {
121        let model = Model::new(Some("TestModel"));
122        let solver = model.solver();
123
124        // Verify that solver.get_model() returns a reference to the same model
125        let retrieved_model = solver.get_model();
126        assert_eq!(retrieved_model.name().as_deref(), Some("TestModel"));
127    }
128
129    #[test]
130    fn test_solver_time_limit() {
131        let model = Model::new(Some("TimeLimitTest"));
132        let vec_vars: Vec<_> = (0..=99)
133            .map(|_| model.int_var_bounded(0, 100, None, None))
134            .collect();
135        vec_vars.all_different().post().unwrap();
136
137        // Post constraints that require search
138
139        assert!(
140            vec_vars[0]
141                .arithm(EqualityOperator::Gt, 50i32)
142                .post()
143                .is_ok()
144        );
145        assert!(
146            vec_vars[1]
147                .arithm(EqualityOperator::Lt, 50i32)
148                .post()
149                .is_ok()
150        );
151        assert!(
152            vec_vars[2]
153                .arithm(EqualityOperator::Eq, 25i32)
154                .post()
155                .is_ok()
156        );
157
158        let solver = model.solver();
159
160        // Set time limit to 1 millisecond
161        solver.set_time_limit(1);
162
163        let criterion = Criterion::new();
164        let solution = solver.find_solution(&criterion);
165
166        // The solver should not find a solution due to the 1ms time limit
167        assert!(solution.is_none());
168    }
169}