From 7ecf0c3fc2cad4df246fc5116455f154ce676fed Mon Sep 17 00:00:00 2001 From: Guillaume Pinot Date: Wed, 22 Sep 2021 10:07:28 +0200 Subject: [PATCH] Bind `ValidateCpModel` and `SolutionIsFeasible` from cp_model_checker.h Fixes #22 --- Cargo.toml | 2 +- src/builder.rs | 19 +++++++++++++++ src/cp_sat_wrapper.cpp | 31 ++++++++++++++++++++++++ src/ffi.rs | 55 ++++++++++++++++++++++++++++++++++++++++++ src/lib.rs | 2 ++ 5 files changed, 108 insertions(+), 1 deletion(-) diff --git a/Cargo.toml b/Cargo.toml index 368bda5..40fcb55 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "cp_sat" -version = "0.3.2" +version = "0.3.3" edition = "2018" description = "Rust bindings to the Google CP-SAT constraint programming solver." documentation = "https://docs.rs/cp_sat" diff --git a/src/builder.rs b/src/builder.rs index b314e35..dc99381 100644 --- a/src/builder.rs +++ b/src/builder.rs @@ -715,6 +715,25 @@ impl CpModelBuilder { ffi::cp_model_stats(self.proto()) } + /// Verifies that the given model satisfies all the properties + /// described in the proto comments. Returns an empty string if it is + /// the case, otherwise fails at the first error and returns a + /// human-readable description of the issue. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_int_var([(0, -1)]); + /// model.maximize(x); + /// assert!(!model.validate_cp_model().is_empty()); + /// ``` + pub fn validate_cp_model(&self) -> String { + ffi::validate_cp_model(self.proto()) + } + /// Solves the model, and returns the corresponding [proto::CpSolverResponse]. /// /// # Example diff --git a/src/cp_sat_wrapper.cpp b/src/cp_sat_wrapper.cpp index 64c63a0..1dc82db 100644 --- a/src/cp_sat_wrapper.cpp +++ b/src/cp_sat_wrapper.cpp @@ -1,6 +1,7 @@ #include #include +#include namespace sat = operations_research::sat; @@ -73,3 +74,33 @@ cp_sat_wrapper_cp_solver_response_stats( const std::string stats = sat::CpSolverResponseStats(response, has_objective); return strdup(stats.c_str()); } + +extern "C" char* +cp_sat_wrapper_validate_cp_model(unsigned char* model_buf, size_t model_size) { + sat::CpModelProto model; + const bool res = model.ParseFromArray(model_buf, model_size); + assert(res); + + const std::string stats = sat::ValidateCpModel(model); + return strdup(stats.c_str()); +} + +extern "C" bool +cp_sat_wrapper_solution_is_feasible( + unsigned char* model_buf, + size_t model_size, + const int64_t* solution_buf, + size_t solution_size) +{ + sat::CpModelProto model; + const bool res = model.ParseFromArray(model_buf, model_size); + assert(res); + + std::vector variable_values; + variable_values.reserve(solution_size); + for (size_t i = 0; i < solution_size; ++i) { + variable_values.push_back(solution_buf[i]); + } + + return sat::SolutionIsFeasible(model, variable_values); +} diff --git a/src/ffi.rs b/src/ffi.rs index aea469b..759eabe 100644 --- a/src/ffi.rs +++ b/src/ffi.rs @@ -22,6 +22,13 @@ extern "C" { response_size: usize, has_objective: bool, ) -> *mut c_char; + fn cp_sat_wrapper_validate_cp_model(model_buf: *const u8, model_size: usize) -> *mut c_char; + fn cp_sat_wrapper_solution_is_feasible( + model_buf: *const u8, + model_size: usize, + solution_buf: *const i64, + solution_size: usize, + ) -> bool; } /// Solves the given [CpModelProto][crate::proto::CpModelProto] and @@ -101,3 +108,51 @@ pub fn cp_solver_response_stats(response: &proto::CpSolverResponse, has_objectiv unsafe { libc::free(char_ptr as _) }; res } + +/// Verifies that the given model satisfies all the properties +/// described in the proto comments. Returns an empty string if it is +/// the case, otherwise fails at the first error and returns a +/// human-readable description of the issue. +pub fn validate_cp_model(model: &proto::CpModelProto) -> String { + let mut model_buf = Vec::default(); + model.encode(&mut model_buf).unwrap(); + let char_ptr = unsafe { cp_sat_wrapper_validate_cp_model(model_buf.as_ptr(), model_buf.len()) }; + let res = unsafe { CStr::from_ptr(char_ptr) } + .to_str() + .unwrap() + .to_owned(); + unsafe { libc::free(char_ptr as _) }; + res +} + +/// Verifies that the given variable assignment is a feasible solution +/// of the given model. The values vector should be in one to one +/// correspondence with the model.variables() list of variables. +/// +/// # Example +/// +/// ``` +/// # use cp_sat::builder::CpModelBuilder; +/// # use cp_sat::proto::CpSolverStatus; +/// # use cp_sat::ffi::solution_is_feasible; +/// let mut model = CpModelBuilder::default(); +/// let x = model.new_bool_var(); +/// let y = model.new_bool_var(); +/// model.add_and([x, y]); +/// assert!(solution_is_feasible(model.proto(), &[1, 1])); +/// assert!(!solution_is_feasible(model.proto(), &[1, 0])); +/// assert!(!solution_is_feasible(model.proto(), &[0, 1])); +/// assert!(!solution_is_feasible(model.proto(), &[0, 0])); +/// ``` +pub fn solution_is_feasible(model: &proto::CpModelProto, solution: &[i64]) -> bool { + let mut model_buf = Vec::default(); + model.encode(&mut model_buf).unwrap(); + unsafe { + cp_sat_wrapper_solution_is_feasible( + model_buf.as_ptr(), + model_buf.len(), + solution.as_ptr(), + solution.len(), + ) + } +} diff --git a/src/lib.rs b/src/lib.rs index 8f33cc7..55e212e 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -57,3 +57,5 @@ pub mod proto { /// Interface with the CP SAT functions. pub mod ffi; + +pub use prost;