Fixed a typo in the README

Fixes #22

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"

README.md

@@ -6,5 +6,5 @@ To use this library, you need a C++ compiler and an installation of
 google or-tools library files.
 
 The environment variable `ORTOOLS_PREFIX` is used to find include
-files and library files. If not setted, `/opt/ortools` will be added
+files and library files. If not set, `/opt/ortools` will be added
 to the search path (classical search path will also be used).

src/builder.rs

@@ -10,8 +10,8 @@ use smallvec::SmallVec;
 /// # 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();
+/// let x = model.new_bool_var("x");
+/// let y = model.new_bool_var("y");
 /// model.add_and([x, y]);
 /// let response = model.solve();
 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
@@ -29,8 +29,8 @@ impl CpModelBuilder {
         &self.proto
     }
 
-    /// Creates a new boolean variable, and returns the [BoolVar]
-    /// indentifier.
+    /// Creates a new boolean variable with the given name, and returns the [BoolVar]
+    /// identifier.
     ///
     /// A boolean variable can be converted to an [IntVar] with the
     /// `std::convert::From` trait. In this case it acts as a variable
@@ -45,30 +45,15 @@ impl CpModelBuilder {
     /// # use cp_sat::builder::{CpModelBuilder, IntVar};
     /// # use cp_sat::proto::CpSolverStatus;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_bool_var();
+    /// let x = model.new_bool_var("x");
     /// 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<String>) -> BoolVar {
+    pub fn new_bool_var(&mut self, name: impl Into<String>) -> BoolVar {
         let index = self.proto.variables.len() as i32;
         self.proto.variables.push(proto::IntegerVariableProto {
             name: name.into(),
@@ -76,8 +61,9 @@ impl CpModelBuilder {
         });
         BoolVar(index)
     }
-    /// Creates a new integer variable, and returns the [IntVar]
-    /// indentifier.
+
+    /// Creates a new integer variable with the given name, and returns the [IntVar]
+    /// identifier.
     ///
     /// The domain of the variable is given. Bounds are included, so
     /// `[(0, 2), (4, 8)]` means [0, 2]∪[4, 8].
@@ -88,29 +74,14 @@ impl CpModelBuilder {
     /// # 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 x = model.new_int_var([(0, 2), (4, 8)], "x");
     /// 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<Item = (i64, i64)>) -> 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(
+    pub fn new_int_var(
         &mut self,
         domain: impl IntoIterator<Item = (i64, i64)>,
         name: impl Into<String>,
@@ -123,17 +94,38 @@ impl CpModelBuilder {
         IntVar(index)
     }
 
-    /// Returns the name of a variable, empty string if not setted.
+    /// Removes the [IntVar] whose name matches the given name from the model.
+    ///
+    /// # Example
+    ///
+    /// ```
+    /// # use cp_sat::builder::{CpModelBuilder, IntVar};
+    /// let mut model = CpModelBuilder::default();
+    /// let x = model.new_int_var([(0, 1)], "some cool name");
+    /// assert!(!model.proto().variables.is_empty());
+    /// let name = model.remove_int_var("some cool name");
+    /// assert!(model.proto().variables.is_empty());
+    pub fn remove_int_var(&mut self, name: &str) {
+        let position = self
+          .proto
+          .variables
+          .iter()
+          .position(|variable| variable.name == name)
+          .unwrap();
+        self.proto.variables.remove(position);
+    }
+
+    /// Returns the name of a variable.
     ///
     /// # Example
     ///
     /// ```
     /// # use cp_sat::builder::CpModelBuilder;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_bool_var_with_name("x");
+    /// let x = model.new_bool_var("x");
     /// assert_eq!("x", model.var_name(x));
-    /// let y = model.new_int_var([(0, 2)]);
-    /// assert_eq!("", model.var_name(y));
+    /// let y = model.new_int_var([(0, 2)], "y");
+    /// assert_eq!("y", model.var_name(y));
     /// ```
     pub fn var_name(&self, var: impl Into<IntVar>) -> &str {
         &self.proto.variables[var.into().0 as usize].name
@@ -146,7 +138,7 @@ impl CpModelBuilder {
     /// ```
     /// # use cp_sat::builder::CpModelBuilder;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_bool_var();
+    /// let x = model.new_bool_var("y");
     /// model.set_var_name(x, "x");
     /// assert_eq!("x", model.var_name(x));
     /// ```
@@ -154,14 +146,46 @@ impl CpModelBuilder {
         self.proto.variables[var.into().0 as usize].name = name.into();
     }
 
-    /// Returns the name of a constraint, empty string if not setted.
+    /// Extracts the domain for an [IntVar]
     ///
     /// # Example
     ///
     /// ```
     /// # use cp_sat::builder::CpModelBuilder;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_bool_var();
+    /// let x = model.new_int_var([(0, 10)], "x");
+    /// assert_eq!((0, 10), model.int_var_domain(x));
+    /// ```
+    pub fn int_var_domain(&self, int_var: IntVar) -> (i64, i64) {
+        let integer_variable_proto = self.proto.variables.iter().find(|variable| variable.name == self.var_name(int_var)).unwrap();
+
+        (*integer_variable_proto.domain.first().unwrap(), *integer_variable_proto.domain.last().unwrap())
+    }
+
+    /// Changes the domain of the [IntVar] with the given name
+    ///
+    /// # Example
+    ///
+    /// ```
+    /// # use cp_sat::builder::CpModelBuilder;
+    /// let mut model = CpModelBuilder::default();
+    /// let x = model.new_int_var([(0, 10)], "x");
+    /// model.set_int_var_domain("x", (-10, 10));
+    /// assert_eq!((-10, 10), model.int_var_domain(x));
+    /// ```
+    pub fn set_int_var_domain(&mut self, name: &str, bounds: (i64, i64)) -> IntVar {
+        self.remove_int_var(name);
+        self.new_int_var([bounds], name)
+    }
+
+    /// Returns the name of a constraint, empty string if not set.
+    ///
+    /// # Example
+    ///
+    /// ```
+    /// # use cp_sat::builder::CpModelBuilder;
+    /// let mut model = CpModelBuilder::default();
+    /// let x = model.new_bool_var("x");
     /// let constraint = model.add_or([x]);
     /// assert_eq!("", model.constraint_name(constraint));
     /// model.set_constraint_name(constraint, "or");
@@ -178,7 +202,7 @@ impl CpModelBuilder {
     /// ```
     /// # use cp_sat::builder::CpModelBuilder;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_bool_var();
+    /// let x = model.new_bool_var("x");
     /// let constraint = model.add_or([x]);
     /// model.set_constraint_name(constraint, "or");
     /// assert_eq!("or", model.constraint_name(constraint));
@@ -195,8 +219,8 @@ impl CpModelBuilder {
     /// # 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();
+    /// let x = model.new_bool_var("x");
+    /// let y = model.new_bool_var("y");
     /// model.add_or([x, y]);
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
@@ -216,8 +240,8 @@ impl CpModelBuilder {
     /// # 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();
+    /// let x = model.new_bool_var("x");
+    /// let y = model.new_bool_var("y");
     /// model.add_and([x, y]);
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
@@ -238,7 +262,7 @@ impl CpModelBuilder {
     /// # 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();
+    /// let vars: Vec<_> = (0..10).map(|i| model.new_bool_var("")).collect();
     /// model.add_at_most_one(vars.iter().copied());
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
@@ -263,16 +287,11 @@ impl CpModelBuilder {
     /// # 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();
+    /// let vars: Vec<_> = (0..10).map(|i| model.new_bool_var(format!("x{i}"))).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::<u32>()
-    ///         == 1
-    /// );
+    /// assert_eq!(vars.iter().map(|v| v.solution_value(&response) as u32).sum::<u32>(), 1);
     /// ```
     pub fn add_exactly_one(&mut self, vars: impl IntoIterator<Item = BoolVar>) -> Constraint {
         self.add_cst(CstEnum::ExactlyOne(proto::BoolArgumentProto {
@@ -288,17 +307,11 @@ impl CpModelBuilder {
     /// # 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();
+    /// let vars: Vec<_> = (0..10).map(|i| model.new_bool_var(format!("x{i}"))).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::<u32>()
-    ///         % 2
-    ///         == 1
-    /// );
+    /// assert_eq!(vars.iter().map(|v| v.solution_value(&response) as u32).sum::<u32>() % 2, 1);
     /// ```
     pub fn add_xor(&mut self, vars: impl IntoIterator<Item = BoolVar>) -> Constraint {
         self.add_cst(CstEnum::BoolXor(proto::BoolArgumentProto {
@@ -314,35 +327,35 @@ impl CpModelBuilder {
     /// # 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)]);
+    /// let x = model.new_int_var([(0, 2)], "x");
+    /// let y = model.new_int_var([(0, 2)], "y");
+    /// let z = model.new_int_var([(0, 2)], "z");
     /// 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);
+    /// assert_ne!(x_val, y_val);
+    /// assert_ne!(x_val, z_val);
+    /// assert_ne!(y_val, z_val);
     /// ```
-    pub fn add_all_different(&mut self, vars: impl IntoIterator<Item = IntVar>) -> Constraint {
+    pub fn add_all_different(&mut self, exprs: impl IntoIterator<Item = impl Into<LinearExpr>>) -> Constraint {
         self.add_cst(CstEnum::AllDiff(proto::AllDifferentConstraintProto {
-            vars: vars.into_iter().map(|v| v.0).collect(),
+            exprs: exprs.into_iter().map(|e| e.into().into()).collect(),
         }))
     }
 
     /// Adds a linear constraint.
     ///
-    /// # Exemple
+    /// # Example
     ///
     /// ```
     /// # use cp_sat::builder::CpModelBuilder;
     /// # use cp_sat::proto::CpSolverStatus;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_int_var([(0, 100)]);
-    /// let y = model.new_int_var([(0, 100)]);
+    /// let x = model.new_int_var([(0, 100)], "x");
+    /// let y = model.new_int_var([(0, 100)], "y");
     /// model.add_linear_constraint([(1, x), (3, y)], [(301, i64::MAX)]);
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
@@ -380,14 +393,14 @@ impl CpModelBuilder {
 
     /// Adds an equality constraint between 2 linear expressions.
     ///
-    /// # Exemple
+    /// # Example
     ///
     /// ```
     /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
     /// # use cp_sat::proto::CpSolverStatus;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_int_var([(0, 50)]);
-    /// let y = model.new_int_var([(53, 100)]);
+    /// let x = model.new_int_var([(0, 50)], "x");
+    /// let y = model.new_int_var([(53, 100)], "y");
     /// model.add_eq(y, LinearExpr::from(x) + 3);
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
@@ -411,8 +424,8 @@ impl CpModelBuilder {
     /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
     /// # use cp_sat::proto::CpSolverStatus;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_int_var([(0, 50)]);
-    /// let y = model.new_int_var([(50, 100)]);
+    /// let x = model.new_int_var([(0, 50)], "x");
+    /// let y = model.new_int_var([(50, 100)], "y");
     /// model.add_ge(x, y);
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
@@ -428,16 +441,16 @@ impl CpModelBuilder {
         self.add_linear_constraint(lhs.into() - rhs.into(), [(0, i64::MAX)])
     }
 
-    /// Adds a lesser or equal constraint between 2 linear expressions.
+    /// Adds a less than or equal to constraint between 2 linear expressions.
     ///
-    /// # Exemple
+    /// # Example
     ///
     /// ```
     /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
     /// # use cp_sat::proto::CpSolverStatus;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_int_var([(50, 100)]);
-    /// let y = model.new_int_var([(0, 50)]);
+    /// let x = model.new_int_var([(50, 100)], "x");
+    /// let y = model.new_int_var([(0, 50)], "y");
     /// model.add_le(x, y);
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
@@ -453,16 +466,39 @@ impl CpModelBuilder {
         self.add_linear_constraint(lhs.into() - rhs.into(), [(i64::MIN, 0)])
     }
 
-    /// Adds a stricly greater constraint between 2 linear expressions.
+    /// Adds a less than or equal to constraint between a linear expression and some domain.
     ///
-    /// # Exemple
+    /// # Example
     ///
     /// ```
     /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
     /// # use cp_sat::proto::CpSolverStatus;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_int_var([(0, 51)]);
-    /// let y = model.new_int_var([(50, 100)]);
+    /// let x = model.new_int_var([(50, 100)], "x");
+    /// model.add_leq(x, (0, 75));
+    /// let response = model.solve();
+    /// assert_eq!(response.status(), CpSolverStatus::Optimal);
+    /// assert!(x.solution_value(&response) <= 75);
+    /// assert_eq!(50, x.solution_value(&response));
+    /// ```
+    pub fn add_leq<T: Into<LinearExpr>>(
+        &mut self,
+        lhs: T,
+        rhs: (i64, i64),
+    ) -> Constraint {
+        self.add_linear_constraint(lhs.into(), [rhs])
+    }
+
+    /// Adds a strictly greater constraint between 2 linear expressions.
+    ///
+    /// # Example
+    ///
+    /// ```
+    /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
+    /// # use cp_sat::proto::CpSolverStatus;
+    /// let mut model = CpModelBuilder::default();
+    /// let x = model.new_int_var([(0, 51)], "x");
+    /// let y = model.new_int_var([(50, 100)], "y");
     /// model.add_gt(x, y);
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
@@ -480,14 +516,14 @@ impl CpModelBuilder {
 
     /// Adds a strictly lesser constraint between 2 linear expressions.
     ///
-    /// # Exemple
+    /// # Example
     ///
     /// ```
     /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
     /// # use cp_sat::proto::CpSolverStatus;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_int_var([(50, 100)]);
-    /// let y = model.new_int_var([(0, 51)]);
+    /// let x = model.new_int_var([(50, 100)], "x");
+    /// let y = model.new_int_var([(0, 51)], "y");
     /// model.add_lt(x, y);
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
@@ -505,17 +541,17 @@ impl CpModelBuilder {
 
     /// Adds a not equal constraint between 2 linear expressions.
     ///
-    /// # Exemple
+    /// # Example
     ///
     /// ```
     /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
     /// # use cp_sat::proto::CpSolverStatus;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_bool_var();
+    /// let x = model.new_bool_var("x");
     /// model.add_ne(x, 1);
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
-    /// assert!(x.solution_value(&response) as i64 != 1);
+    /// assert_ne!(x.solution_value(&response) as i64, 1);
     /// assert!(!x.solution_value(&response));
     /// ```
     pub fn add_ne<T: Into<LinearExpr>, U: Into<LinearExpr>>(
@@ -527,17 +563,47 @@ impl CpModelBuilder {
     }
 
     /// Adds a constraint that force the `target` to be equal to the
-    /// minimum of the given `exprs`.
+    /// product of the given `exprs`.
     ///
-    /// # Exemple
+    /// # Example
     ///
     /// ```
     /// # 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)]);
+    /// let x = model.new_int_var([(0, 10)], "x");
+    /// let y = model.new_int_var([(5, 15)], "y");
+    /// let m = model.new_int_var([(-200, 200)], "m");
+    /// model.add_mult_eq(m, [x, y]);
+    /// model.maximize(m);
+    /// let response = model.solve();
+    /// assert_eq!(response.status(), CpSolverStatus::Optimal);
+    /// assert_eq!(150., response.objective_value);
+    /// assert_eq!(150, m.solution_value(&response));
+    /// ```
+    pub fn add_mult_eq(
+        &mut self,
+        target: impl Into<LinearExpr>,
+        exprs: impl IntoIterator<Item = impl Into<LinearExpr>>,
+    ) -> Constraint {
+        self.add_cst(CstEnum::IntProd(proto::LinearArgumentProto {
+            target: Some(target.into().into()),
+            exprs: exprs.into_iter().map(|e| e.into().into()).collect(),
+        }))
+    }
+
+    /// Adds a constraint that force the `target` to be equal to the
+    /// minimum of the given `exprs`.
+    ///
+    /// # Example
+    ///
+    /// ```
+    /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
+    /// # use cp_sat::proto::CpSolverStatus;
+    /// let mut model = CpModelBuilder::default();
+    /// let x = model.new_int_var([(0, 10)], "x");
+    /// let y = model.new_int_var([(5, 15)], "y");
+    /// let m = model.new_int_var([(-100, 100)], "m");
     /// model.add_min_eq(m, [x, y]);
     /// model.maximize(m);
     /// let response = model.solve();
@@ -550,24 +616,24 @@ impl CpModelBuilder {
         target: impl Into<LinearExpr>,
         exprs: impl IntoIterator<Item = impl Into<LinearExpr>>,
     ) -> Constraint {
-        self.add_cst(CstEnum::LinMin(proto::LinearArgumentProto {
-            target: Some(target.into().into()),
-            exprs: exprs.into_iter().map(|e| e.into().into()).collect(),
+        self.add_cst(CstEnum::LinMax(proto::LinearArgumentProto {
+            target: Some((-target.into()).into()),
+            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
+    /// # Example
     ///
     /// ```
     /// # 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)]);
+    /// let x = model.new_int_var([(0, 10)], "x");
+    /// let y = model.new_int_var([(5, 15)], "y");
+    /// let m = model.new_int_var([(-100, 100)], "m");
     /// model.add_max_eq(m, [x, y]);
     /// model.minimize(m);
     /// let response = model.solve();
@@ -585,6 +651,7 @@ impl CpModelBuilder {
             exprs: exprs.into_iter().map(|e| e.into().into()).collect(),
         }))
     }
+
     fn add_cst(&mut self, cst: CstEnum) -> Constraint {
         let index = self.proto.constraints.len();
         self.proto.constraints.push(proto::ConstraintProto {
@@ -602,8 +669,8 @@ impl CpModelBuilder {
     /// # use cp_sat::builder::CpModelBuilder;
     /// # use cp_sat::proto::CpSolverStatus;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_int_var([(0, 100)]);
-    /// let y = model.new_bool_var();
+    /// let x = model.new_int_var([(0, 100)], "x");
+    /// let y = model.new_bool_var("y");
     /// model.add_hint(x, 42);
     /// model.add_hint(y, 1);
     /// let response = model.solve();
@@ -632,8 +699,8 @@ impl CpModelBuilder {
     /// # use cp_sat::builder::CpModelBuilder;
     /// # use cp_sat::proto::CpSolverStatus;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_int_var([(0, 100)]);
-    /// let y = model.new_bool_var();
+    /// let x = model.new_int_var([(0, 100)], "x");
+    /// let y = model.new_bool_var("y");
     /// model.add_hint(x, 42);
     /// model.add_hint(y, 1);
     /// model.del_hints();
@@ -654,7 +721,7 @@ impl CpModelBuilder {
     /// # use cp_sat::builder::CpModelBuilder;
     /// # use cp_sat::proto::CpSolverStatus;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_int_var([(0, 100)]);
+    /// let x = model.new_int_var([(0, 100)], "x");
     /// model.minimize(x);
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
@@ -668,6 +735,10 @@ impl CpModelBuilder {
             coeffs: expr.coeffs.into_vec(),
             offset: expr.constant as f64,
             scaling_factor: 1.,
+            integer_before_offset: 0,
+            integer_after_offset: 0,
+            integer_scaling_factor: 0,
+            scaling_was_exact: true,
             domain: vec![],
         });
     }
@@ -680,7 +751,7 @@ impl CpModelBuilder {
     /// # use cp_sat::builder::CpModelBuilder;
     /// # use cp_sat::proto::CpSolverStatus;
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_int_var([(0, 100)]);
+    /// let x = model.new_int_var([(0, 100)], "x");
     /// model.maximize(x);
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
@@ -697,6 +768,10 @@ impl CpModelBuilder {
             coeffs: expr.coeffs.into_vec(),
             offset: -expr.constant as f64,
             scaling_factor: -1.,
+            integer_before_offset: 0,
+            integer_after_offset: 0,
+            integer_scaling_factor: 0,
+            scaling_was_exact: true,
             domain: vec![],
         });
     }
@@ -715,6 +790,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)], "x");
+    /// 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
@@ -765,12 +859,13 @@ impl BoolVar {
     /// # use cp_sat::builder::CpModelBuilder;
     /// # use cp_sat::proto::{CpSolverStatus, SatParameters};
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_bool_var();
+    /// let x = model.new_bool_var("x");
     /// model.add_or([x]);
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
     /// assert!(x.solution_value(&response));
     /// ```
+    #[track_caller]
     pub fn solution_value(self, response: &proto::CpSolverResponse) -> bool {
         if self.0 < 0 {
             use std::ops::Not;
@@ -816,12 +911,13 @@ impl IntVar {
     /// # use cp_sat::builder::CpModelBuilder;
     /// # use cp_sat::proto::{CpSolverStatus, SatParameters};
     /// let mut model = CpModelBuilder::default();
-    /// let x = model.new_int_var([(0, 42)]);
+    /// let x = model.new_int_var([(0, 42)], "x");
     /// model.maximize(x);
     /// let response = model.solve();
     /// assert_eq!(response.status(), CpSolverStatus::Optimal);
     /// assert_eq!(42, x.solution_value(&response));
     /// ```
+    #[track_caller]
     pub fn solution_value(self, response: &proto::CpSolverResponse) -> i64 {
         if self.0 < 0 {
             1 - self.not().solution_value(response)
@@ -844,7 +940,7 @@ pub struct Constraint(usize);
 /// It describes an expression in the form `ax+by+c`. Several [From]
 /// and [std::ops] traits are implemented for easy modeling.
 ///
-/// # Exemple
+/// # Example
 ///
 /// Most of the builder methods that takes something linear take in
 /// practice a `impl Into<LinearExpr>`.  In the example, we will use
@@ -853,10 +949,10 @@ pub struct Constraint(usize);
 /// ```
 /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
 /// let mut model = CpModelBuilder::default();
-/// let x1 = model.new_int_var([(0, 100)]);
-/// let x2 = model.new_int_var([(0, 100)]);
-/// let y1 = model.new_bool_var();
-/// let y2 = model.new_bool_var();
+/// let x1 = model.new_int_var([(0, 100)], "x1");
+/// let x2 = model.new_int_var([(0, 100)], "x2");
+/// let y1 = model.new_bool_var("y1");
+/// let y2 = model.new_bool_var("y2");
 /// model.maximize(x1); // IntVar can be converted in LinearExpr
 /// model.maximize(y1); // as BoolVar
 /// model.maximize(42); // as i64
@@ -867,7 +963,7 @@ pub struct Constraint(usize);
 /// model.maximize([(42, x1), (1337, y2.into())]); // BoolVar conversion
 ///
 /// // for easy looping, we can also modify a LinearExpr
-/// let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect();
+/// let vars: Vec<_> = (0..10).map(|i| model.new_bool_var(format!("x{i}"))).collect();
 /// let mut expr = LinearExpr::default(); // means 0, can also be LinearExpr::from(0)
 /// for (i, v) in vars.iter().copied().enumerate() {
 ///     match i {
@@ -980,7 +1076,7 @@ impl From<LinearExpr> for proto::LinearExpressionProto {
     }
 }
 
-impl<T: Into<LinearExpr>> std::iter::Extend<T> for LinearExpr {
+impl<T: Into<LinearExpr>> Extend<T> for LinearExpr {
     fn extend<I: IntoIterator<Item = T>>(&mut self, iter: I) {
         for e in iter {
             *self += e;

src/cp_model.proto

@@ -1,4 +1,4 @@
-// Copyright 2010-2021 Google LLC
+// Copyright 2010-2022 Google LLC
 // Licensed under the Apache License, Version 2.0 (the "License");
 // you may not use this file except in compliance with the License.
 // You may obtain a copy of the License at
@@ -70,12 +70,6 @@ message BoolArgumentProto {
   repeated int32 literals = 1;
 }
 
-// Argument of the constraints of the form target_var = OP(vars).
-message IntegerArgumentProto {
-  int32 target = 1;
-  repeated int32 vars = 2;
-}
-
 // Some constraints supports linear expression instead of just using a reference
 // to a variable. This is especially useful during presolve to reduce the model
 // size.
@@ -90,9 +84,9 @@ message LinearArgumentProto {
   repeated LinearExpressionProto exprs = 2;
 }
 
-// All variables must take different values.
+// All affine expressions must take different values.
 message AllDifferentConstraintProto {
-  repeated int32 vars = 1;
+  repeated LinearExpressionProto exprs = 1;
 }
 
 // The linear sum vars[i] * coeffs[i] must fall in the given domain. The domain
@@ -115,33 +109,21 @@ message ElementConstraintProto {
   repeated int32 vars = 3;
 }
 
-// This "special" constraint not only enforces (start + size == end) and (size
-// >= 0) but can also be referred by other constraints using this "interval"
-// concept.
-message IntervalConstraintProto {
-  int32 start = 1;
-  int32 end = 2;
-  int32 size = 3;
-
-  // EXPERIMENTAL: This will become the new way to specify an interval.
-  // Depending on the parameters, the presolve will convert the old way to the
-  // new way. Do not forget to add an associated linear constraint if you use
-  // this directly.
-  //
-  // If any of this field is set, then all must be set and the ones above will
-  // be ignored.
+// This is not really a constraint. It is there so it can be referred by other
+// constraints using this "interval" concept.
 //
 // IMPORTANT: For now, this constraint do not enforce any relations on the
-  // view, and a linear constraint must be added together with this to enforce
-  // enforcement => start_view + size_view == end_view. An enforcement =>
-  // size_view >=0 might also be needed.
+// components, and it is up to the client to add in the model:
+// - enforcement => start + size == end.
+// - enforcement => size >= 0  // Only needed if size is not already >= 0.
 //
 // IMPORTANT: For now, we just support affine relation. We could easily
 // create an intermediate variable to support full linear expression, but this
 // isn't done currently.
-  LinearExpressionProto start_view = 4;
-  LinearExpressionProto end_view = 5;
-  LinearExpressionProto size_view = 6;
+message IntervalConstraintProto {
+  LinearExpressionProto start = 4;
+  LinearExpressionProto end = 5;
+  LinearExpressionProto size = 6;
 }
 
 // All the intervals (index of IntervalConstraintProto) must be disjoint. More
@@ -154,32 +136,41 @@ message NoOverlapConstraintProto {
 }
 
 // The boxes defined by [start_x, end_x) * [start_y, end_y) cannot overlap.
+// Furthermore, one box is optional if at least one of the x or y interval is
+// optional.
 message NoOverlap2DConstraintProto {
   repeated int32 x_intervals = 1;
   repeated int32 y_intervals = 2;  // Same size as x_intervals.
   bool boxes_with_null_area_can_overlap = 3;
+  // TODO(user): Add optional areas as repeated LinearExpressionProto.
 }
 
 // The sum of the demands of the intervals at each interval point cannot exceed
 // a capacity. Note that intervals are interpreted as [start, end) and as
 // such intervals like [2,3) and [3,4) do not overlap for the point of view of
 // this constraint. Moreover, intervals of size zero are ignored.
+//
+// All demands must not contain any negative value in their domains. This is
+// checked at validation. The capacity can currently contains negative values,
+// but it will be propagated to >= 0 right away.
 message CumulativeConstraintProto {
-  int32 capacity = 1;
+  LinearExpressionProto capacity = 1;
   repeated int32 intervals = 2;
-  repeated int32 demands = 3;  // Same size as intervals.
+  repeated LinearExpressionProto demands = 3;  // Same size as intervals.
 }
 
 // Maintain a reservoir level within bounds. The water level starts at 0, and at
 // any time, it must be within [min_level, max_level].
 //
-// If the variable actives[i] is true, and if the variable times[i] is assigned
-// a value t, then the current level changes by demands[i] (which is constant)
-// at the time t. Therefore, at any time t:
-//      sum(demands[i] * actives[i] if times[i] <= t) in [min_level, max_level]
+// If the variable active_literals[i] is true, and if the expression
+// time_exprs[i] is assigned a value t, then the current level changes by
+// level_changes[i] at the time t. Therefore, at any time t:
+//
+// sum(level_changes[i] * active_literals[i] if time_exprs[i] <= t)
+//   in [min_level, max_level]
 //
 // Note that min level must be <= 0, and the max level must be >= 0. Please use
-// fixed demands to simulate initial state.
+// fixed level_changes to simulate initial state.
 //
 // The array of boolean variables 'actives', if defined, indicates which actions
 // are actually performed. If this array is not defined, then it is assumed that
@@ -187,9 +178,11 @@ message CumulativeConstraintProto {
 message ReservoirConstraintProto {
   int64 min_level = 1;
   int64 max_level = 2;
-  repeated int32 times = 3;    // variables.
-  repeated int64 demands = 4;  // constants, can be negative.
-  repeated int32 actives = 5;  // literals.
+  repeated LinearExpressionProto time_exprs = 3;  // affine expressions.
+  // Currently, we only support constant level changes.
+  repeated LinearExpressionProto level_changes = 6;  // affine expressions.
+  repeated int32 active_literals = 5;
+  reserved 4;
 }
 
 // The circuit constraint is defined on a graph where the arc presence are
@@ -218,6 +211,11 @@ message CircuitConstraintProto {
 // - Self-arcs are allowed except for node 0.
 // - There is no cycle in this graph, except through node 0.
 //
+// Note: Currently this constraint expect all the nodes in [0, num_nodes) to
+// have at least one incident arc. The model will be considered invalid if it
+// is not the case. You can add self-arc fixed to one to ignore some nodes if
+// needed.
+//
 // TODO(user): It is probably possible to generalize this constraint to a
 // no-cycle in a general graph, or a no-cycle with sum incoming <= 1 and sum
 // outgoing <= 1 (more efficient implementation). On the other hand, having this
@@ -227,7 +225,7 @@ message RoutesConstraintProto {
   repeated int32 heads = 2;
   repeated int32 literals = 3;
 
-  // Experimental. The demands for each node, and the maximum capacity for each
+  // EXPERIMENTAL. The demands for each node, and the maximum capacity for each
   // route. Note that this is currently only used for the LP relaxation and one
   // need to add the corresponding constraint to enforce this outside of the LP.
   //
@@ -280,7 +278,12 @@ message AutomatonConstraintProto {
   repeated int32 vars = 7;
 }
 
-// Next id: 30
+// A list of variables, without any semantics.
+message ListOfVariablesProto {
+  repeated int32 vars = 1;
+}
+
+// Next id: 31
 message ConstraintProto {
   // For debug/logging only. Can be empty.
   string name = 1;
@@ -343,40 +346,31 @@ message ConstraintProto {
     // The bool_xor constraint forces an odd number of the literals to be true.
     BoolArgumentProto bool_xor = 5;
 
-    // The int_div constraint forces the target to equal vars[0] / vars[1].
-    // In particular, vars[1] can never take the value 0.
-    IntegerArgumentProto int_div = 7;
+    // The int_div constraint forces the target to equal exprs[0] / exprs[1].
+    // In particular, exprs[1] can never take the value 0. Also, as for now, we
+    // do not support exprs[1] spanning across 0.
+    LinearArgumentProto int_div = 7;
 
-    // The int_mod constraint forces the target to equal vars[0] % vars[1].
-    // The domain of vars[1] must be strictly positive.
-    IntegerArgumentProto int_mod = 8;
-
-    // The int_max constraint forces the target to equal the maximum of all
-    // variables.
-    //
-    // The lin_max constraint forces the target to equal the maximum of all
-    // linear expressions.
-    //
-    // TODO(user): Remove int_max in favor of lin_max.
-    IntegerArgumentProto int_max = 9;
-    LinearArgumentProto lin_max = 27;
-
-    // The int_min constraint forces the target to equal the minimum of all
-    // variables.
-    //
-    // The lin_min constraint forces the target to equal the minimum of all
-    // linear expressions.
-    //
-    // TODO(user): Remove int_min in favor of lin_min.
-    IntegerArgumentProto int_min = 10;
-    LinearArgumentProto lin_min = 28;
+    // The int_mod constraint forces the target to equal exprs[0] % exprs[1].
+    // The domain of exprs[1] must be strictly positive. The sign of the target
+    // is the same as the sign of exprs[0].
+    LinearArgumentProto int_mod = 8;
 
     // The int_prod constraint forces the target to equal the product of all
     // variables. By convention, because we can just remove term equal to one,
     // the empty product forces the target to be one.
     //
+    // Note that the solver checks for potential integer overflow. So it is
+    // recommended to limit the domain of the variables such that the product
+    // fits in [INT_MIN + 1..INT_MAX - 1].
+    //
     // TODO(user): Support more than two terms in the product.
-    IntegerArgumentProto int_prod = 11;
+    LinearArgumentProto int_prod = 11;
+
+    // The lin_max constraint forces the target to equal the maximum of all
+    // linear expressions.
+    // Note that this can model a minimum simply by negating all expressions.
+    LinearArgumentProto lin_max = 27;
 
     // The linear constraint enforces a linear inequality among the variables,
     // such as 0 <= x + 2y <= 10.
@@ -438,16 +432,18 @@ message ConstraintProto {
     // of the demands of the intervals containing that point does not exceed
     // the capacity.
     CumulativeConstraintProto cumulative = 22;
+
+    // This constraint is not meant to be used and will be rejected by the
+    // solver. It is meant to mark variable when testing the presolve code.
+    ListOfVariablesProto dummy_constraint = 30;
   }
 }
 
 // Optimization objective.
-//
-// This is in a message because decision problems don't have any objective.
 message CpObjectiveProto {
   // The linear terms of the objective to minimize.
   // For a maximization problem, one can negate all coefficients in the
-  // objective and set a scaling_factor to -1.
+  // objective and set scaling_factor to -1.
   repeated int32 vars = 1;
   repeated int64 coeffs = 4;
 
@@ -465,6 +461,40 @@ message CpObjectiveProto {
   // Note that this does not depend on the offset or scaling factor, it is a
   // domain on the sum of the objective terms only.
   repeated int64 domain = 5;
+
+  // Internal field. Do not set. When we scale a FloatObjectiveProto to a
+  // integer version, we set this to true if the scaling was exact (i.e. all
+  // original coeff were integer for instance).
+  //
+  // TODO(user): Put the error bounds we computed instead?
+  bool scaling_was_exact = 6;
+
+  // Internal fields to recover a bound on the original integer objective from
+  // the presolved one. Basically, initially the integer objective fit on an
+  // int64 and is in [Initial_lb, Initial_ub]. During presolve, we might change
+  // the linear expression to have a new domain [Presolved_lb, Presolved_ub]
+  // that will also always fit on an int64.
+  //
+  // The two domain will always be linked with an affine transformation between
+  // the two of the form:
+  //   old = (new + before_offset) * integer_scaling_factor + after_offset.
+  // Note that we use both offsets to always be able to do the computation while
+  // staying in the int64 domain. In particular, the after_offset will always
+  // be in (-integer_scaling_factor, integer_scaling_factor).
+  int64 integer_before_offset = 7;
+  int64 integer_after_offset = 9;
+  int64 integer_scaling_factor = 8;
+}
+
+// A linear floating point objective: sum coeffs[i] * vars[i] + offset.
+// Note that the variable can only still take integer value.
+message FloatObjectiveProto {
+  repeated int32 vars = 1;
+  repeated double coeffs = 2;
+  double offset = 3;
+
+  // The optimization direction. The default is to minimize
+  bool maximize = 4;
 }
 
 // Define the strategy to follow when the solver needs to take a new decision.
@@ -538,7 +568,7 @@ message DenseMatrixProto {
   repeated int32 entries = 3;
 }
 
-// Experimental. For now, this is meant to be used by the solver and not filled
+// EXPERIMENTAL. For now, this is meant to be used by the solver and not filled
 // by clients.
 //
 // Hold symmetry information about the set of feasible solutions. If we permute
@@ -580,6 +610,21 @@ message CpModelProto {
   // The objective to minimize. Can be empty for pure decision problems.
   CpObjectiveProto objective = 4;
 
+  // Advanced usage.
+  // It is invalid to have both an objective and a floating point objective.
+  //
+  // The objective of the model, in floating point format. The solver will
+  // automatically scale this to integer during expansion and thus convert it to
+  // a normal CpObjectiveProto. See the mip* parameters to control how this is
+  // scaled. In most situation the precision will be good enough, but you can
+  // see the logs to see what are the precision guaranteed when this is
+  // converted to a fixed point representation.
+  //
+  // Note that even if the precision is bad, the returned objective_value and
+  // best_objective_bound will be computed correctly. So at the end of the solve
+  // you can check the gap if you only want precise optimal.
+  FloatObjectiveProto floating_point_objective = 9;
+
   // Defines the strategy that the solver should follow when the
   // search_branching parameter is set to FIXED_SEARCH. Note that this strategy
   // is also used as a heuristic when we are not in fixed search.
@@ -587,9 +632,8 @@ message CpModelProto {
   // Advanced Usage: if not all variables appears and the parameter
   // "instantiate_all_variables" is set to false, then the solver will not try
   // to instantiate the variables that do not appear. Thus, at the end of the
-  // search, not all variables may be fixed and this is why we have the
-  // solution_lower_bounds and solution_upper_bounds fields in the
-  // CpSolverResponse.
+  // search, not all variables may be fixed. Currently, we will set them to
+  // their lower bound in the solution.
   repeated DecisionStrategyProto search_strategy = 5;
 
   // Solution hint.
@@ -612,7 +656,7 @@ message CpModelProto {
   // infeasibility.
   //
   // Think (IIS), except when you are only concerned by the provided
-  // assumptions. This is powerful as it allows to group a set of logicially
+  // assumptions. This is powerful as it allows to group a set of logically
   // related constraint under only one enforcement literal which can potentially
   // give you a good and interpretable explanation for infeasiblity.
   //
@@ -657,11 +701,17 @@ enum CpSolverStatus {
   OPTIMAL = 4;
 }
 
+// Just a message used to store dense solution.
+// This is used by the additional_solutions field.
+message CpSolverSolution {
+  repeated int64 values = 1;
+}
+
 // The response returned by a solver trying to solve a CpModelProto.
 //
 // TODO(user): support returning multiple solutions. Look at the Stubby
 // streaming API as we probably wants to get them as they are found.
-// Next id: 27
+// Next id: 30
 message CpSolverResponse {
   // The status of the solve.
   CpSolverStatus status = 1;
@@ -683,15 +733,13 @@ message CpSolverResponse {
   // maximization problem.
   double best_objective_bound = 4;
 
-  // Advanced usage.
+  // If the parameter fill_additional_solutions_in_response is set, then we
+  // copy all the solutions from our internal solution pool here.
   //
-  // If the problem has some variables that are not fixed at the end of the
-  // search (because of a particular search strategy in the CpModelProto) then
-  // this will be used instead of filling the solution above. The two fields
-  // will then contains the lower and upper bounds of each variable as they were
-  // when the best "solution" was found.
-  repeated int64 solution_lower_bounds = 18;
-  repeated int64 solution_upper_bounds = 19;
+  // Note that the one returned in the solution field will likely appear here
+  // too. Do not rely on the solutions order as it depends on our internal
+  // representation (after postsolve).
+  repeated CpSolverSolution additional_solutions = 27;
 
   // Advanced usage.
   //
@@ -721,17 +769,28 @@ message CpSolverResponse {
   // changing your model to minimize the number of assumptions at false, but
   // this is likely an harder problem to solve.
   //
+  // Important: Currently, this is minimized only in single-thread and if the
+  // problem is not an optimization problem, otherwise, it will always include
+  // all the assumptions.
+  //
   // TODO(user): Allows for returning multiple core at once.
   repeated int32 sufficient_assumptions_for_infeasibility = 23;
 
-  // This will be true iff the solver was asked to find all solutions to a
-  // satisfiability problem (or all optimal solutions to an optimization
-  // problem), and it was successful in doing so.
+  // Contains the integer objective optimized internally. This is only filled if
+  // the problem had a floating point objective, and on the final response, not
+  // the ones given to callbacks.
+  CpObjectiveProto integer_objective = 28;
+
+  // Advanced usage.
   //
-  // TODO(user): Remove as we also use the OPTIMAL vs FEASIBLE status for that.
-  bool all_solutions_were_found = 5;
+  // A lower bound on the inner integer expression of the objective. This is
+  // either a bound on the expression in the returned integer_objective or on
+  // the integer expression of the original objective if the problem already has
+  // an integer objective.
+  int64 inner_objective_lower_bound = 29;
 
   // Some statistics about the solve.
+  // TODO(user): These are broken in multi-thread.
   int64 num_booleans = 10;
   int64 num_conflicts = 11;
   int64 num_branches = 12;
@@ -740,12 +799,16 @@ message CpSolverResponse {
   int64 num_restarts = 24;
   int64 num_lp_iterations = 25;
 
+  // The time counted from the beginning of the Solve() call.
   double wall_time = 15;
   double user_time = 16;
   double deterministic_time = 17;
-  double primal_integral = 22;
 
-  // Additional information about how the solution was found.
+  // The integral of log(1 + absolute_objective_gap) over time.
+  double gap_integral = 22;
+
+  // Additional information about how the solution was found. It also stores
+  // model or parameters errors that caused the model to be invalid.
   string solution_info = 20;
 
   // The solve log will be filled if the parameter log_to_response is set to

src/cp_sat_wrapper.cpp

@@ -1,6 +1,7 @@
 #include <iostream>
 
 #include <ortools/sat/cp_model.h>
+#include <ortools/sat/cp_model_checker.h>
 
 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<int64_t> 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);
+}

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("x");
+/// let y = model.new_bool_var("y");
+/// 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(),
+        )
+    }
+}

src/lib.rs

@@ -24,9 +24,9 @@
 //! 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");
+//!     let x = model.new_int_var([(0, 2)], "x");
+//!     let y = model.new_int_var([(0, 2)], "y");
+//!     let z = model.new_int_var([(0, 2)], "z");
 //!
 //!     model.add_ne(x, y);
 //!
@@ -57,3 +57,5 @@ pub mod proto {
 
 /// Interface with the CP SAT functions.
 pub mod ffi;
+
+pub use prost;

tests/bool_cst.rs

@@ -4,7 +4,7 @@ use cp_sat::proto::CpSolverStatus;
 #[test]
 fn not_infeasible() {
   let mut model = CpModelBuilder::default();
-    let x = model.new_bool_var();
+  let x = model.new_bool_var("x");
   model.add_and([x, !x]);
   let response = model.solve();
   assert_eq!(response.status(), CpSolverStatus::Infeasible);
@@ -13,8 +13,8 @@ fn not_infeasible() {
 #[test]
 fn not_feasible() {
   let mut model = CpModelBuilder::default();
-    let x = model.new_bool_var();
-    let y = model.new_bool_var();
+  let x = model.new_bool_var("x");
+  let y = model.new_bool_var("y");
   model.add_and([x, !y]);
   let response = model.solve();
   assert_eq!(response.status(), CpSolverStatus::Optimal);

tests/sat_parameters.rs

@@ -4,7 +4,7 @@ use cp_sat::proto::{CpSolverStatus, SatParameters};
 #[test]
 fn simple_sat_parameters() {
   let mut model = CpModelBuilder::default();
-    let x = model.new_bool_var();
+  let x = model.new_bool_var("x");
   let params = SatParameters::default();
   let response = model.solve_with_parameters(&params);
   assert_eq!(response.status(), CpSolverStatus::Optimal);

tests/tutorial_tests.rs

@@ -5,14 +5,13 @@ use cp_sat::proto::{CpSolverStatus, SatParameters};
 fn presentation_problem() {
   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");
+  let x = model.new_int_var(domain, "x");
+  let y = model.new_int_var(domain, "y");
+  let z = model.new_int_var(domain, "z");
 
   model.add_ne(x, y);
 
   let response = model.solve();
-    println!("{:?}", response);
 
   assert_eq!(response.status(), CpSolverStatus::Optimal);
   let x_val = x.solution_value(&response);
@@ -22,19 +21,19 @@ fn presentation_problem() {
   println!("y = {}", y_val);
   println!("z = {}", z_val);
 
-    assert!(x_val != y_val);
-    assert!(0 <= x_val && x_val <= 2);
-    assert!(0 <= y_val && y_val <= 2);
-    assert!(0 <= z_val && z_val <= 2);
+  assert_ne!(x_val, y_val);
+  assert!((0..=2).contains(&x_val));
+  assert!((0..=2).contains(&y_val));
+  assert!((0..=2).contains(&z_val));
 }
 
 #[test]
 fn solving_a_cp_problem() {
   let mut model = CpModelBuilder::default();
   let var_upper_bound = vec![50, 45, 37].into_iter().max().unwrap();
-    let x = model.new_int_var_with_name([(0, var_upper_bound)], "x");
-    let y = model.new_int_var_with_name([(0, var_upper_bound)], "y");
-    let z = model.new_int_var_with_name([(0, var_upper_bound)], "z");
+  let x = model.new_int_var([(0, var_upper_bound)], "x");
+  let y = model.new_int_var([(0, var_upper_bound)], "y");
+  let z = model.new_int_var([(0, var_upper_bound)], "z");
 
   model.add_le([(2, x), (7, y), (3, z)], 50);
   model.add_le([(3, x), (-5, y), (7, z)], 45);
@@ -62,17 +61,18 @@ fn solving_a_cp_problem() {
 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");
+  let x = model.new_int_var(domain, "x");
+  let y = model.new_int_var(domain, "y");
+  let z = model.new_int_var(domain, "z");
 
   model.add_ne(x, y);
 
-    let mut params = SatParameters::default();
-    params.max_time_in_seconds = Some(10.);
+  let params = SatParameters {
+    max_time_in_seconds: Some(10.),
+    ..SatParameters::default()
+  };
 
   let response = model.solve_with_parameters(&params);
-    println!("{:?}", response);
 
   assert_eq!(response.status(), CpSolverStatus::Optimal);
   let x_val = x.solution_value(&response);