From 5db1b7d4df62fad14bb1fef5623a6fb04d370f99 Mon Sep 17 00:00:00 2001 From: Guillaume Pinot Date: Mon, 13 Sep 2021 15:33:56 +0200 Subject: [PATCH] Refactor for clean root module and documentation --- Cargo.toml | 2 +- examples/simple_sat_program.rs | 27 ++- src/builder.rs | 392 ++++++++++++++++++++++++++++++++- src/ffi.rs | 103 +++++++++ src/lib.rs | 143 +++++------- tests/bool_cst.rs | 69 ------ tests/min_max_cst.rs | 32 --- tests/tutorial_tests.rs | 27 ++- 8 files changed, 580 insertions(+), 215 deletions(-) create mode 100644 src/ffi.rs delete mode 100644 tests/min_max_cst.rs diff --git a/Cargo.toml b/Cargo.toml index 93dcded..ace00ec 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "cp_sat" -version = "0.2.1" +version = "0.3.0" edition = "2018" description = "Rust bindings to the Google CP-SAT constraint programming solver." documentation = "https://docs.rs/cp_sat" diff --git a/examples/simple_sat_program.rs b/examples/simple_sat_program.rs index 2872c54..3f077d2 100644 --- a/examples/simple_sat_program.rs +++ b/examples/simple_sat_program.rs @@ -1,19 +1,24 @@ +use cp_sat::builder::CpModelBuilder; +use cp_sat::proto::CpSolverStatus; + fn main() { - let mut model = cp_sat::builder::CpModelBuilder::default(); + let mut model = CpModelBuilder::default(); + let x = model.new_int_var_with_name([(0, 2)], "x"); let y = model.new_int_var_with_name([(0, 2)], "y"); let z = model.new_int_var_with_name([(0, 2)], "z"); - model.add_all_different([x, y, z]); - println!("{:#?}", model); - println!("model stats: {}", model.stats()); + + model.add_ne(x, y); + let response = model.solve(); - println!("{:#?}", response); println!( - "response stats: {}", - cp_sat::cp_solver_response_stats(&response, false) + "{}", + cp_sat::ffi::cp_solver_response_stats(&response, false) ); - assert_eq!(response.status(), cp_sat::proto::CpSolverStatus::Optimal); - assert!(x.solution_value(&response) != y.solution_value(&response)); - assert!(x.solution_value(&response) != z.solution_value(&response)); - assert!(y.solution_value(&response) != z.solution_value(&response)); + + if response.status() == CpSolverStatus::Optimal { + println!("x = {}", x.solution_value(&response)); + println!("y = {}", y.solution_value(&response)); + println!("z = {}", z.solution_value(&response)); + } } diff --git a/src/builder.rs b/src/builder.rs index 0d78f66..13a8ad9 100644 --- a/src/builder.rs +++ b/src/builder.rs @@ -1,18 +1,72 @@ -use crate::proto; +use crate::{ffi, proto}; use proto::constraint_proto::Constraint as CstEnum; +/// A builder for CP SAT. +/// +/// # Example +/// +/// ``` +/// # use cp_sat::builder::CpModelBuilder; +/// # use cp_sat::proto::CpSolverStatus; +/// let mut model = CpModelBuilder::default(); +/// let x = model.new_bool_var(); +/// let y = model.new_bool_var(); +/// model.add_and([x, y]); +/// let response = model.solve(); +/// assert_eq!(response.status(), CpSolverStatus::Optimal); +/// assert!(x.solution_value(&response)); +/// assert!(y.solution_value(&response)); +/// ``` #[derive(Default, Debug)] pub struct CpModelBuilder { proto: proto::CpModelProto, } impl CpModelBuilder { + /// Returns the corresponding [proto::CpModelProto]. pub fn proto(&self) -> &proto::CpModelProto { &self.proto } + + /// Creates a new boolean variable, and returns the [BoolVar] + /// indentifier. + /// + /// A boolean variable can be converted to an [IntVar] with the + /// `std::convert::From` trait. In this case it acts as a variable + /// within [0, 1]. + /// + /// A [BoolVar] can be negated with [std::ops::Not], so you can + /// use the `!` operator on it. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::{CpModelBuilder, IntVar}; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_bool_var(); + /// model.add_and([!x]); + /// let _x_integer: IntVar = x.into(); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// assert!(!x.solution_value(&response)); + /// ``` pub fn new_bool_var(&mut self) -> BoolVar { self.new_bool_var_with_name("") } + + /// Creates a new boolean variable with a name, and returns the + /// [BoolVar] indentifier. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_bool_var_with_name("x"); + /// assert_eq!("x", model.var_name(x)); + /// ``` pub fn new_bool_var_with_name(&mut self, name: impl Into) -> BoolVar { let index = self.proto.variables.len() as i32; self.proto.variables.push(proto::IntegerVariableProto { @@ -21,9 +75,40 @@ impl CpModelBuilder { }); BoolVar(index) } + /// Creates a new integer variable, and returns the [IntVar] + /// indentifier. + /// + /// The domain of the variable is given. Bounds are included, so + /// `[(0, 2), (4, 8)]` means [0, 2]∪[4, 8]. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::{CpModelBuilder, IntVar}; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_int_var([(0, 2), (4, 8)]); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// let x_val = x.solution_value(&response); + /// assert!(0 <= x_val && x_val <= 2 || 4 <= x_val && 8 <= x_val); + /// ``` pub fn new_int_var(&mut self, domain: impl IntoIterator) -> IntVar { self.new_int_var_with_name(domain, "") } + + /// Creates a new integer variable with a name, and returns the + /// [IntVar] indentifier. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_int_var_with_name([(0, 10)], "x"); + /// assert_eq!("x", model.var_name(x)); + /// ``` pub fn new_int_var_with_name( &mut self, domain: impl IntoIterator, @@ -36,45 +121,185 @@ impl CpModelBuilder { }); IntVar(index) } + + /// Returns the name of a variable, empty string if not setted. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_bool_var_with_name("x"); + /// assert_eq!("x", model.var_name(x)); + /// let y = model.new_int_var([(0, 2)]); + /// assert_eq!("", model.var_name(y)); + /// ``` pub fn var_name(&self, var: impl Into) -> &str { &self.proto.variables[var.into().0 as usize].name } + + /// Sets the variable name. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_bool_var(); + /// model.set_var_name(x, "x"); + /// assert_eq!("x", model.var_name(x)); + /// ``` pub fn set_var_name(&mut self, var: impl Into, name: &str) { self.proto.variables[var.into().0 as usize].name = name.into(); } + /// Adds a boolean OR constraint on a list of [BoolVar]. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_bool_var(); + /// let y = model.new_bool_var(); + /// model.add_or([x, y]); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// assert!(x.solution_value(&response) || y.solution_value(&response)); + /// ``` pub fn add_or(&mut self, vars: impl IntoIterator) -> Constraint { self.add_cst(CstEnum::BoolOr(proto::BoolArgumentProto { literals: vars.into_iter().map(|v| v.0).collect(), })) } + + /// Adds a boolean AND constraint on a list of [BoolVar]. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_bool_var(); + /// let y = model.new_bool_var(); + /// model.add_and([x, y]); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// assert!(x.solution_value(&response)); + /// assert!(y.solution_value(&response)); + /// ``` pub fn add_and(&mut self, vars: impl IntoIterator) -> Constraint { self.add_cst(CstEnum::BoolAnd(proto::BoolArgumentProto { literals: vars.into_iter().map(|v| v.0).collect(), })) } + + /// Adds a boolean "at most one" constraint on a list of [BoolVar]. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect(); + /// model.add_at_most_one(vars.iter().copied()); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// assert!( + /// vars.iter() + /// .map(|v| v.solution_value(&response) as u32) + /// .sum::() + /// <= 1 + /// ); + /// ``` pub fn add_at_most_one(&mut self, vars: impl IntoIterator) -> Constraint { self.add_cst(CstEnum::AtMostOne(proto::BoolArgumentProto { literals: vars.into_iter().map(|v| v.0).collect(), })) } + + /// Adds a boolean "exactly one" constraint on a list of [BoolVar]. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect(); + /// model.add_exactly_one(vars.iter().copied()); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// assert!( + /// vars.iter() + /// .map(|v| v.solution_value(&response) as u32) + /// .sum::() + /// == 1 + /// ); + /// ``` pub fn add_exactly_one(&mut self, vars: impl IntoIterator) -> Constraint { self.add_cst(CstEnum::ExactlyOne(proto::BoolArgumentProto { literals: vars.into_iter().map(|v| v.0).collect(), })) } + + /// Adds a boolean XOR constraint on a list of [BoolVar]. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect(); + /// model.add_xor(vars.iter().copied()); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// assert!( + /// vars.iter() + /// .map(|v| v.solution_value(&response) as u32) + /// .sum::() + /// % 2 + /// == 1 + /// ); + /// ``` pub fn add_xor(&mut self, vars: impl IntoIterator) -> Constraint { self.add_cst(CstEnum::BoolXor(proto::BoolArgumentProto { literals: vars.into_iter().map(|v| v.0).collect(), })) } + + /// Adds a "all different" constraint on a list of [BoolVar]. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_int_var([(0, 2)]); + /// let y = model.new_int_var([(0, 2)]); + /// let z = model.new_int_var([(0, 2)]); + /// model.add_all_different([x, y, z]); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// let x_val = x.solution_value(&response); + /// let y_val = y.solution_value(&response); + /// let z_val = z.solution_value(&response); + /// assert!(x_val != y_val); + /// assert!(x_val != z_val); + /// assert!(y_val != z_val); + /// ``` pub fn add_all_different(&mut self, vars: impl IntoIterator) -> Constraint { self.add_cst(CstEnum::AllDiff(proto::AllDifferentConstraintProto { vars: vars.into_iter().map(|v| v.0).collect(), })) } - /// Add a linear constraint + /// Adds a linear constraint. /// /// # Exemple /// @@ -119,7 +344,7 @@ impl CpModelBuilder { })) } - /// Add an equality constraint between 2 linear expressions. + /// Adds an equality constraint between 2 linear expressions. /// /// # Exemple /// @@ -144,7 +369,7 @@ impl CpModelBuilder { self.add_linear_constraint(lhs.into() - rhs.into(), [(0, 0)]) } - /// Add a greater or equal constraint between 2 linear expressions. + /// Adds a greater or equal constraint between 2 linear expressions. /// /// # Exemple /// @@ -169,7 +394,7 @@ impl CpModelBuilder { self.add_linear_constraint(lhs.into() - rhs.into(), [(0, i64::MAX)]) } - /// Add a lesser or equal constraint between 2 linear expressions. + /// Adds a lesser or equal constraint between 2 linear expressions. /// /// # Exemple /// @@ -194,7 +419,7 @@ impl CpModelBuilder { self.add_linear_constraint(lhs.into() - rhs.into(), [(i64::MIN, 0)]) } - /// Add a stricly greater constraint between 2 linear expressions. + /// Adds a stricly greater constraint between 2 linear expressions. /// /// # Exemple /// @@ -219,7 +444,7 @@ impl CpModelBuilder { self.add_linear_constraint(lhs.into() - rhs.into(), [(1, i64::MAX)]) } - /// Add a strictly lesser constraint between 2 linear expressions. + /// Adds a strictly lesser constraint between 2 linear expressions. /// /// # Exemple /// @@ -244,7 +469,7 @@ impl CpModelBuilder { self.add_linear_constraint(lhs.into() - rhs.into(), [(i64::MIN, -1)]) } - /// Add a not equal constraint between 2 linear expressions. + /// Adds a not equal constraint between 2 linear expressions. /// /// # Exemple /// @@ -268,6 +493,25 @@ impl CpModelBuilder { ) -> Constraint { self.add_linear_constraint(lhs.into() - rhs.into(), [(i64::MIN, -1), (1, i64::MAX)]) } + + /// Adds a constraint that force the `target` to be equal to the + /// minimum of the given `exprs`. + /// + /// # Exemple + /// + /// ``` + /// # use cp_sat::builder::{CpModelBuilder, LinearExpr}; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_int_var([(0, 10)]); + /// let y = model.new_int_var([(5, 15)]); + /// let m = model.new_int_var([(-100, 100)]); + /// model.add_min_eq(m, [x, y]); + /// model.maximize(m); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// assert_eq!(10., response.objective_value); + /// ``` pub fn add_min_eq( &mut self, target: impl Into, @@ -278,6 +522,25 @@ impl CpModelBuilder { exprs: exprs.into_iter().map(|e| e.into().into()).collect(), })) } + + /// Adds a constraint that force the `target` to be equal to the + /// maximum of the given `exprs`. + /// + /// # Exemple + /// + /// ``` + /// # use cp_sat::builder::{CpModelBuilder, LinearExpr}; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_int_var([(0, 10)]); + /// let y = model.new_int_var([(5, 15)]); + /// let m = model.new_int_var([(-100, 100)]); + /// model.add_max_eq(m, [x, y]); + /// model.minimize(m); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// assert_eq!(5., response.objective_value); + /// ``` pub fn add_max_eq( &mut self, target: impl Into, @@ -327,6 +590,21 @@ impl CpModelBuilder { } } + /// Sets the minimization objective. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_int_var([(0, 100)]); + /// model.minimize(x); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// assert_eq!(0, x.solution_value(&response)); + /// assert_eq!(0., response.objective_value); + /// ``` pub fn minimize>(&mut self, expr: T) { let expr = expr.into(); self.proto.objective = Some(proto::CpObjectiveProto { @@ -337,6 +615,22 @@ impl CpModelBuilder { domain: vec![], }); } + + /// Sets the maximization objective. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_int_var([(0, 100)]); + /// model.maximize(x); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// assert_eq!(100, x.solution_value(&response)); + /// assert_eq!(100., response.objective_value); + /// ``` pub fn maximize>(&mut self, expr: T) { let mut expr = expr.into(); for coeff in &mut expr.coeffs { @@ -351,20 +645,76 @@ impl CpModelBuilder { }); } + /// Returns some statistics on the model. + /// + /// #Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// let model = CpModelBuilder::default(); + /// let stats = model.stats(); + /// assert!(!stats.is_empty()); + /// ``` pub fn stats(&self) -> String { - crate::cp_model_stats(self.proto()) + ffi::cp_model_stats(self.proto()) } + + /// Solves the model, and returns the corresponding [proto::CpSolverResponse]. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::CpSolverStatus; + /// let model = CpModelBuilder::default(); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// ``` pub fn solve(&self) -> proto::CpSolverResponse { - crate::solve(self.proto()) + ffi::solve(self.proto()) } + + /// Solves the model with the given + /// [parameters][proto::SatParameters], and returns the + /// corresponding [proto::CpSolverResponse]. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::{CpSolverStatus, SatParameters}; + /// let model = CpModelBuilder::default(); + /// let mut params = SatParameters::default(); + /// params.max_deterministic_time = Some(1.); + /// let response = model.solve_with_parameters(¶ms); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// ``` pub fn solve_with_parameters(&self, params: &proto::SatParameters) -> proto::CpSolverResponse { - crate::solve_with_parameters(self.proto(), params) + ffi::solve_with_parameters(self.proto(), params) } } +/// Boolean variable identifier. #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct BoolVar(i32); impl BoolVar { + /// Gets the solution value of the variable from a solution. + /// + /// The solution must come from the same model as the variable, + /// and a solution must be present in the response. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::{CpSolverStatus, SatParameters}; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_bool_var(); + /// model.add_or([x]); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// assert!(x.solution_value(&response)); + /// ``` pub fn solution_value(self, response: &proto::CpSolverResponse) -> bool { if self.0 < 0 { use std::ops::Not; @@ -390,6 +740,7 @@ impl std::fmt::Debug for BoolVar { } } +/// Integer variable identifier. #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct IntVar(i32); impl From for IntVar { @@ -398,6 +749,23 @@ impl From for IntVar { } } impl IntVar { + /// Gets the solution value of the variable from a solution. + /// + /// The solution must come from the same model as the variable, + /// and a solution must be present in the response. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::CpModelBuilder; + /// # use cp_sat::proto::{CpSolverStatus, SatParameters}; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_int_var([(0, 42)]); + /// model.maximize(x); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// assert_eq!(42, x.solution_value(&response)); + /// ``` pub fn solution_value(self, response: &proto::CpSolverResponse) -> i64 { if self.0 < 0 { 1 - self.not().solution_value(response) @@ -410,10 +778,12 @@ impl IntVar { } } +/// Constraint identifier. #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct Constraint(usize); #[derive(Clone, Default, Debug)] +#[allow(missing_docs)] pub struct LinearExpr { vars: Vec, coeffs: Vec, diff --git a/src/ffi.rs b/src/ffi.rs new file mode 100644 index 0000000..aea469b --- /dev/null +++ b/src/ffi.rs @@ -0,0 +1,103 @@ +use crate::proto; +use libc::c_char; +use prost::Message; +use std::ffi::CStr; + +extern "C" { + fn cp_sat_wrapper_solve( + model_buf: *const u8, + model_size: usize, + out_size: &mut usize, + ) -> *mut u8; + fn cp_sat_wrapper_solve_with_parameters( + model_buf: *const u8, + model_size: usize, + params_buf: *const u8, + params_size: usize, + out_size: &mut usize, + ) -> *mut u8; + fn cp_sat_wrapper_cp_model_stats(model_buf: *const u8, model_size: usize) -> *mut c_char; + fn cp_sat_wrapper_cp_solver_response_stats( + response_buf: *const u8, + response_size: usize, + has_objective: bool, + ) -> *mut c_char; +} + +/// Solves the given [CpModelProto][crate::proto::CpModelProto] and +/// returns an instance of +/// [CpSolverResponse][crate::proto::CpSolverResponse]. +pub fn solve(model: &proto::CpModelProto) -> proto::CpSolverResponse { + let mut buf = Vec::default(); + model.encode(&mut buf).unwrap(); + let mut out_size = 0; + let res = unsafe { cp_sat_wrapper_solve(buf.as_ptr(), buf.len(), &mut out_size) }; + let out_slice = unsafe { std::slice::from_raw_parts(res, out_size) }; + let response = proto::CpSolverResponse::decode(out_slice).unwrap(); + unsafe { libc::free(res as _) }; + response +} + +/// Solves the given [CpModelProto][crate::proto::CpModelProto] with +/// the given parameters. +pub fn solve_with_parameters( + model: &proto::CpModelProto, + params: &proto::SatParameters, +) -> proto::CpSolverResponse { + let mut model_buf = Vec::default(); + model.encode(&mut model_buf).unwrap(); + let mut params_buf = Vec::default(); + params.encode(&mut params_buf).unwrap(); + + let mut out_size = 0; + let res = unsafe { + cp_sat_wrapper_solve_with_parameters( + model_buf.as_ptr(), + model_buf.len(), + params_buf.as_ptr(), + params_buf.len(), + &mut out_size, + ) + }; + let out_slice = unsafe { std::slice::from_raw_parts(res, out_size) }; + let response = proto::CpSolverResponse::decode(out_slice).unwrap(); + unsafe { libc::free(res as _) }; + response +} + +/// Returns a string with some statistics on the given +/// [CpModelProto][crate::proto::CpModelProto]. +pub fn cp_model_stats(model: &proto::CpModelProto) -> String { + let mut model_buf = Vec::default(); + model.encode(&mut model_buf).unwrap(); + let char_ptr = unsafe { cp_sat_wrapper_cp_model_stats(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 +} + +/// Returns a string with some statistics on the solver response. +/// +/// If the second argument is false, we will just display NA for the +/// objective value instead of zero. It is not really needed but it +/// makes things a bit clearer to see that there is no objective. +pub fn cp_solver_response_stats(response: &proto::CpSolverResponse, has_objective: bool) -> String { + let mut response_buf = Vec::default(); + response.encode(&mut response_buf).unwrap(); + let char_ptr = unsafe { + cp_sat_wrapper_cp_solver_response_stats( + response_buf.as_ptr(), + response_buf.len(), + has_objective, + ) + }; + let res = unsafe { CStr::from_ptr(char_ptr) } + .to_str() + .unwrap() + .to_owned(); + unsafe { libc::free(char_ptr as _) }; + res +} diff --git a/src/lib.rs b/src/lib.rs index b5f8bf6..9b77dc5 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,95 +1,58 @@ -use libc::c_char; -use prost::Message; -use std::ffi::CStr; +//! The `cp_sat` crate provides an interface to [Google CP +//! SAT](https://developers.google.com/optimization/cp/cp_solver). +//! +//! # OR-Tools installation +//! +//! For `cp_sat` to work, you need to have a working OR-Tools +//! installation. By default, this crate will use the default C++ +//! compiler, and add `/opt/ortools` in the search path. If you want +//! to provide your OR-Tools installation directory, you can define +//! the `ORTOOL_PREFIX` environment variable. +//! +//! # Brief overview +//! +//! The [builder::CpModelBuilder] provides an easy interface to +//! construct your problem. You can then solve and access to the +//! solver response easily. Here you can find the translation of the +//! first tutorial in the official documentation of CP SAT: +//! +//! ``` +//! use cp_sat::builder::CpModelBuilder; +//! use cp_sat::proto::CpSolverStatus; +//! +//! fn main() { +//! let mut model = CpModelBuilder::default(); +//! +//! let x = model.new_int_var_with_name([(0, 2)], "x"); +//! let y = model.new_int_var_with_name([(0, 2)], "y"); +//! let z = model.new_int_var_with_name([(0, 2)], "z"); +//! +//! model.add_ne(x, y); +//! +//! let response = model.solve(); +//! println!( +//! "{}", +//! cp_sat::ffi::cp_solver_response_stats(&response, false) +//! ); +//! +//! if response.status() == CpSolverStatus::Optimal { +//! println!("x = {}", x.solution_value(&response)); +//! println!("y = {}", y.solution_value(&response)); +//! println!("z = {}", z.solution_value(&response)); +//! } +//! } +//! ``` +#![deny(missing_docs)] + +/// Model builder for ergonomic and efficient model creation. +pub mod builder; + +/// Export of the CP SAT protobufs +#[allow(missing_docs, rustdoc::broken_intra_doc_links, rustdoc::bare_urls)] pub mod proto { include!(concat!(env!("OUT_DIR"), "/operations_research.sat.rs")); } -pub mod builder; -extern "C" { - fn cp_sat_wrapper_solve( - model_buf: *const u8, - model_size: usize, - out_size: &mut usize, - ) -> *mut u8; - fn cp_sat_wrapper_solve_with_parameters( - model_buf: *const u8, - model_size: usize, - params_buf: *const u8, - params_size: usize, - out_size: &mut usize, - ) -> *mut u8; - fn cp_sat_wrapper_cp_model_stats(model_buf: *const u8, model_size: usize) -> *mut c_char; - fn cp_sat_wrapper_cp_solver_response_stats( - response_buf: *const u8, - response_size: usize, - has_objective: bool, - ) -> *mut c_char; -} - -pub fn solve(model: &proto::CpModelProto) -> proto::CpSolverResponse { - let mut buf = Vec::default(); - model.encode(&mut buf).unwrap(); - let mut out_size = 0; - let res = unsafe { cp_sat_wrapper_solve(buf.as_ptr(), buf.len(), &mut out_size) }; - let out_slice = unsafe { std::slice::from_raw_parts(res, out_size) }; - let response = proto::CpSolverResponse::decode(out_slice).unwrap(); - unsafe { libc::free(res as _) }; - response -} - -pub fn solve_with_parameters( - model: &proto::CpModelProto, - params: &proto::SatParameters, -) -> proto::CpSolverResponse { - let mut model_buf = Vec::default(); - model.encode(&mut model_buf).unwrap(); - let mut params_buf = Vec::default(); - params.encode(&mut params_buf).unwrap(); - - let mut out_size = 0; - let res = unsafe { - cp_sat_wrapper_solve_with_parameters( - model_buf.as_ptr(), - model_buf.len(), - params_buf.as_ptr(), - params_buf.len(), - &mut out_size, - ) - }; - let out_slice = unsafe { std::slice::from_raw_parts(res, out_size) }; - let response = proto::CpSolverResponse::decode(out_slice).unwrap(); - unsafe { libc::free(res as _) }; - response -} - -pub fn cp_model_stats(model: &proto::CpModelProto) -> String { - let mut model_buf = Vec::default(); - model.encode(&mut model_buf).unwrap(); - let char_ptr = unsafe { cp_sat_wrapper_cp_model_stats(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 -} - -pub fn cp_solver_response_stats(response: &proto::CpSolverResponse, has_objective: bool) -> String { - let mut response_buf = Vec::default(); - response.encode(&mut response_buf).unwrap(); - let char_ptr = unsafe { - cp_sat_wrapper_cp_solver_response_stats( - response_buf.as_ptr(), - response_buf.len(), - has_objective, - ) - }; - let res = unsafe { CStr::from_ptr(char_ptr) } - .to_str() - .unwrap() - .to_owned(); - unsafe { libc::free(char_ptr as _) }; - res -} +/// Interface with the CP SAT functions. +pub mod ffi; diff --git a/tests/bool_cst.rs b/tests/bool_cst.rs index 6d2ea47..bbb8da6 100644 --- a/tests/bool_cst.rs +++ b/tests/bool_cst.rs @@ -1,75 +1,6 @@ use cp_sat::builder::CpModelBuilder; use cp_sat::proto::CpSolverStatus; -#[test] -fn or() { - let mut model = CpModelBuilder::default(); - let x = model.new_bool_var(); - let y = model.new_bool_var(); - model.add_or([x, y]); - let response = model.solve(); - assert_eq!(response.status(), CpSolverStatus::Optimal); - assert!(x.solution_value(&response) || y.solution_value(&response)); -} - -#[test] -fn and() { - let mut model = CpModelBuilder::default(); - let x = model.new_bool_var(); - let y = model.new_bool_var(); - model.add_and([x, y]); - let response = model.solve(); - assert_eq!(response.status(), CpSolverStatus::Optimal); - assert!(x.solution_value(&response)); - assert!(y.solution_value(&response)); -} - -#[test] -fn at_most_one() { - let mut model = CpModelBuilder::default(); - let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect(); - model.add_at_most_one(vars.iter().copied()); - let response = model.solve(); - assert_eq!(response.status(), CpSolverStatus::Optimal); - assert!( - vars.iter() - .map(|v| v.solution_value(&response) as u32) - .sum::() - <= 1 - ); -} - -#[test] -fn exactly_one() { - let mut model = CpModelBuilder::default(); - let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect(); - model.add_exactly_one(vars.iter().copied()); - let response = model.solve(); - assert_eq!(response.status(), CpSolverStatus::Optimal); - assert!( - vars.iter() - .map(|v| v.solution_value(&response) as u32) - .sum::() - == 1 - ); -} - -#[test] -fn xor() { - let mut model = CpModelBuilder::default(); - let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect(); - model.add_xor(vars.iter().copied()); - let response = model.solve(); - assert_eq!(response.status(), CpSolverStatus::Optimal); - assert!( - vars.iter() - .map(|v| v.solution_value(&response) as u32) - .sum::() - % 2 - == 1 - ); -} - #[test] fn not_infeasible() { let mut model = CpModelBuilder::default(); diff --git a/tests/min_max_cst.rs b/tests/min_max_cst.rs deleted file mode 100644 index e89def9..0000000 --- a/tests/min_max_cst.rs +++ /dev/null @@ -1,32 +0,0 @@ -use cp_sat::builder::CpModelBuilder; -use cp_sat::proto::CpSolverStatus; - -#[test] -fn min() { - let mut model = CpModelBuilder::default(); - let x = model.new_int_var([(0, 10)]); - let y = model.new_int_var([(5, 15)]); - let m = model.new_int_var([(-100, 100)]); - model.add_min_eq(m, [x, y]); - model.maximize(m); - - println!("{:#?}", model.proto()); - let response = model.solve(); - assert_eq!(response.status(), CpSolverStatus::Optimal); - assert_eq!(10., response.objective_value); -} - -#[test] -fn max() { - let mut model = CpModelBuilder::default(); - let x = model.new_int_var([(0, 10)]); - let y = model.new_int_var([(5, 15)]); - let m = model.new_int_var([(-100, 100)]); - model.add_max_eq(m, [x, y]); - model.minimize(m); - - println!("{:#?}", model.proto()); - let response = model.solve(); - assert_eq!(response.status(), CpSolverStatus::Optimal); - assert_eq!(5., response.objective_value); -} diff --git a/tests/tutorial_tests.rs b/tests/tutorial_tests.rs index d4384b0..79086d7 100644 --- a/tests/tutorial_tests.rs +++ b/tests/tutorial_tests.rs @@ -1,5 +1,5 @@ use cp_sat::builder::CpModelBuilder; -use cp_sat::proto::CpSolverStatus; +use cp_sat::proto::{CpSolverStatus, SatParameters}; #[test] fn presentation_problem() { @@ -57,3 +57,28 @@ fn solving_a_cp_problem() { assert!(3 * x_val - 5 * y_val + 7 * z_val <= 45); assert!(5 * x_val + 2 * y_val - 6 * z_val <= 37); } + +#[test] +fn solve_with_time_limit_sample_sat() { + let mut model = CpModelBuilder::default(); + let domain = [(0, 2)]; + let x = model.new_int_var_with_name(domain, "x"); + let y = model.new_int_var_with_name(domain, "y"); + let z = model.new_int_var_with_name(domain, "z"); + + model.add_ne(x, y); + + let mut params = SatParameters::default(); + params.max_time_in_seconds = Some(10.); + + let response = model.solve_with_parameters(¶ms); + println!("{:?}", response); + + assert_eq!(response.status(), CpSolverStatus::Optimal); + let x_val = x.solution_value(&response); + let y_val = y.solution_value(&response); + let z_val = z.solution_value(&response); + println!("x = {}", x_val); + println!("y = {}", y_val); + println!("z = {}", z_val); +}