cp_sat/builder.rs
1use crate::{ffi, proto};
2use proto::constraint_proto::Constraint as CstEnum;
3use smallvec::SmallVec;
4
5/// A builder for CP SAT.
6///
7/// # Example
8///
9/// ```
10/// # use cp_sat::builder::CpModelBuilder;
11/// # use cp_sat::proto::CpSolverStatus;
12/// let mut model = CpModelBuilder::default();
13/// let x = model.new_bool_var();
14/// let y = model.new_bool_var();
15/// model.add_and([x, y]);
16/// let response = model.solve();
17/// assert_eq!(response.status(), CpSolverStatus::Optimal);
18/// assert!(x.solution_value(&response));
19/// assert!(y.solution_value(&response));
20/// ```
21#[derive(Default, Debug)]
22pub struct CpModelBuilder {
23 proto: proto::CpModelProto,
24}
25
26impl CpModelBuilder {
27 /// Returns the corresponding [proto::CpModelProto].
28 pub fn proto(&self) -> &proto::CpModelProto {
29 &self.proto
30 }
31
32 /// Creates a new boolean variable, and returns the [BoolVar]
33 /// indentifier.
34 ///
35 /// A boolean variable can be converted to an [IntVar] with the
36 /// `std::convert::From` trait. In this case it acts as a variable
37 /// within [0, 1].
38 ///
39 /// A [BoolVar] can be negated with [std::ops::Not], so you can
40 /// use the `!` operator on it.
41 ///
42 /// # Example
43 ///
44 /// ```
45 /// # use cp_sat::builder::{CpModelBuilder, IntVar};
46 /// # use cp_sat::proto::CpSolverStatus;
47 /// let mut model = CpModelBuilder::default();
48 /// let x = model.new_bool_var();
49 /// model.add_and([!x]);
50 /// let _x_integer: IntVar = x.into();
51 /// let response = model.solve();
52 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
53 /// assert!(!x.solution_value(&response));
54 /// ```
55 pub fn new_bool_var(&mut self) -> BoolVar {
56 self.new_bool_var_with_name("")
57 }
58
59 /// Creates a new boolean variable with a name, and returns the
60 /// [BoolVar] indentifier.
61 ///
62 /// # Example
63 ///
64 /// ```
65 /// # use cp_sat::builder::CpModelBuilder;
66 /// # use cp_sat::proto::CpSolverStatus;
67 /// let mut model = CpModelBuilder::default();
68 /// let x = model.new_bool_var_with_name("x");
69 /// assert_eq!("x", model.var_name(x));
70 /// ```
71 pub fn new_bool_var_with_name(&mut self, name: impl Into<String>) -> BoolVar {
72 let index = self.proto.variables.len() as i32;
73 self.proto.variables.push(proto::IntegerVariableProto {
74 name: name.into(),
75 domain: vec![0, 1],
76 });
77 BoolVar(index)
78 }
79 /// Creates a new integer variable, and returns the [IntVar]
80 /// indentifier.
81 ///
82 /// The domain of the variable is given. Bounds are included, so
83 /// `[(0, 2), (4, 8)]` means [0, 2]∪[4, 8].
84 ///
85 /// # Example
86 ///
87 /// ```
88 /// # use cp_sat::builder::{CpModelBuilder, IntVar};
89 /// # use cp_sat::proto::CpSolverStatus;
90 /// let mut model = CpModelBuilder::default();
91 /// let x = model.new_int_var([(0, 2), (4, 8)]);
92 /// let response = model.solve();
93 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
94 /// let x_val = x.solution_value(&response);
95 /// assert!(0 <= x_val && x_val <= 2 || 4 <= x_val && 8 <= x_val);
96 /// ```
97 pub fn new_int_var(&mut self, domain: impl IntoIterator<Item = (i64, i64)>) -> IntVar {
98 self.new_int_var_with_name(domain, "")
99 }
100
101 /// Creates a new integer variable with a name, and returns the
102 /// [IntVar] indentifier.
103 ///
104 /// # Example
105 ///
106 /// ```
107 /// # use cp_sat::builder::CpModelBuilder;
108 /// # use cp_sat::proto::CpSolverStatus;
109 /// let mut model = CpModelBuilder::default();
110 /// let x = model.new_int_var_with_name([(0, 10)], "x");
111 /// assert_eq!("x", model.var_name(x));
112 /// ```
113 pub fn new_int_var_with_name(
114 &mut self,
115 domain: impl IntoIterator<Item = (i64, i64)>,
116 name: impl Into<String>,
117 ) -> IntVar {
118 let index = self.proto.variables.len() as i32;
119 self.proto.variables.push(proto::IntegerVariableProto {
120 name: name.into(),
121 domain: domain.into_iter().flat_map(|(b, e)| [b, e]).collect(),
122 });
123 IntVar(index)
124 }
125
126 /// Returns the name of a variable, empty string if not setted.
127 ///
128 /// # Example
129 ///
130 /// ```
131 /// # use cp_sat::builder::CpModelBuilder;
132 /// let mut model = CpModelBuilder::default();
133 /// let x = model.new_bool_var_with_name("x");
134 /// assert_eq!("x", model.var_name(x));
135 /// let y = model.new_int_var([(0, 2)]);
136 /// assert_eq!("", model.var_name(y));
137 /// ```
138 pub fn var_name(&self, var: impl Into<IntVar>) -> &str {
139 &self.proto.variables[var.into().0 as usize].name
140 }
141
142 /// Sets the variable name.
143 ///
144 /// # Example
145 ///
146 /// ```
147 /// # use cp_sat::builder::CpModelBuilder;
148 /// let mut model = CpModelBuilder::default();
149 /// let x = model.new_bool_var();
150 /// model.set_var_name(x, "x");
151 /// assert_eq!("x", model.var_name(x));
152 /// ```
153 pub fn set_var_name(&mut self, var: impl Into<IntVar>, name: &str) {
154 self.proto.variables[var.into().0 as usize].name = name.into();
155 }
156
157 /// Returns the name of a constraint, empty string if not setted.
158 ///
159 /// # Example
160 ///
161 /// ```
162 /// # use cp_sat::builder::CpModelBuilder;
163 /// let mut model = CpModelBuilder::default();
164 /// let x = model.new_bool_var();
165 /// let constraint = model.add_or([x]);
166 /// assert_eq!("", model.constraint_name(constraint));
167 /// model.set_constraint_name(constraint, "or");
168 /// assert_eq!("or", model.constraint_name(constraint));
169 /// ```
170 pub fn constraint_name(&self, constraint: Constraint) -> &str {
171 &self.proto.constraints[constraint.0].name
172 }
173
174 /// Sets the name of a constraint.
175 ///
176 /// # Example
177 ///
178 /// ```
179 /// # use cp_sat::builder::CpModelBuilder;
180 /// let mut model = CpModelBuilder::default();
181 /// let x = model.new_bool_var();
182 /// let constraint = model.add_or([x]);
183 /// model.set_constraint_name(constraint, "or");
184 /// assert_eq!("or", model.constraint_name(constraint));
185 /// ```
186 pub fn set_constraint_name(&mut self, constraint: Constraint, name: &str) {
187 self.proto.constraints[constraint.0].name = name.into();
188 }
189
190 /// Sets enforcement literals on a constraint. The constraint will only
191 /// be enforced when ALL the given literals are true.
192 ///
193 /// This is also called "half-reification". When the enforcement literals
194 /// are false, the constraint is simply ignored.
195 ///
196 /// Note: Only bool_or, bool_and, and linear constraints fully support
197 /// enforcement literals.
198 ///
199 /// # Example
200 ///
201 /// ```
202 /// # use cp_sat::builder::CpModelBuilder;
203 /// # use cp_sat::proto::CpSolverStatus;
204 /// let mut model = CpModelBuilder::default();
205 /// let x = model.new_bool_var();
206 /// let y = model.new_bool_var();
207 /// let z = model.new_bool_var();
208 /// // z must be true, but only if x is true
209 /// let cst = model.add_and([z]);
210 /// model.only_enforce_if(cst, [x]);
211 /// // force x to be false, so z can be anything
212 /// model.add_and([!x, !y]);
213 /// let response = model.solve();
214 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
215 /// assert!(!x.solution_value(&response));
216 /// // z is unconstrained since x is false
217 /// ```
218 pub fn only_enforce_if(
219 &mut self,
220 constraint: Constraint,
221 literals: impl IntoIterator<Item = BoolVar>,
222 ) {
223 self.proto.constraints[constraint.0]
224 .enforcement_literal
225 .extend(literals.into_iter().map(|v| v.0));
226 }
227
228 /// Adds an implication constraint: if `a` is true, then `b` must be true.
229 ///
230 /// This is equivalent to `add_or([!a, b])`.
231 ///
232 /// # Example
233 ///
234 /// ```
235 /// # use cp_sat::builder::CpModelBuilder;
236 /// # use cp_sat::proto::CpSolverStatus;
237 /// let mut model = CpModelBuilder::default();
238 /// let a = model.new_bool_var();
239 /// let b = model.new_bool_var();
240 /// model.add_implication(a, b); // a => b
241 /// model.add_and([a]); // force a to be true
242 /// let response = model.solve();
243 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
244 /// assert!(a.solution_value(&response));
245 /// assert!(b.solution_value(&response)); // b must be true since a is true
246 /// ```
247 pub fn add_implication(&mut self, a: BoolVar, b: BoolVar) -> Constraint {
248 self.add_or([!a, b])
249 }
250
251 /// Adds a boolean OR constraint on a list of [BoolVar].
252 ///
253 /// # Example
254 ///
255 /// ```
256 /// # use cp_sat::builder::CpModelBuilder;
257 /// # use cp_sat::proto::CpSolverStatus;
258 /// let mut model = CpModelBuilder::default();
259 /// let x = model.new_bool_var();
260 /// let y = model.new_bool_var();
261 /// model.add_or([x, y]);
262 /// let response = model.solve();
263 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
264 /// assert!(x.solution_value(&response) || y.solution_value(&response));
265 /// ```
266 pub fn add_or(&mut self, vars: impl IntoIterator<Item = BoolVar>) -> Constraint {
267 self.add_cst(CstEnum::BoolOr(proto::BoolArgumentProto {
268 literals: vars.into_iter().map(|v| v.0).collect(),
269 }))
270 }
271
272 /// Adds a boolean AND constraint on a list of [BoolVar].
273 ///
274 /// # Example
275 ///
276 /// ```
277 /// # use cp_sat::builder::CpModelBuilder;
278 /// # use cp_sat::proto::CpSolverStatus;
279 /// let mut model = CpModelBuilder::default();
280 /// let x = model.new_bool_var();
281 /// let y = model.new_bool_var();
282 /// model.add_and([x, y]);
283 /// let response = model.solve();
284 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
285 /// assert!(x.solution_value(&response));
286 /// assert!(y.solution_value(&response));
287 /// ```
288 pub fn add_and(&mut self, vars: impl IntoIterator<Item = BoolVar>) -> Constraint {
289 self.add_cst(CstEnum::BoolAnd(proto::BoolArgumentProto {
290 literals: vars.into_iter().map(|v| v.0).collect(),
291 }))
292 }
293
294 /// Adds a boolean "at most one" constraint on a list of [BoolVar].
295 ///
296 /// # Example
297 ///
298 /// ```
299 /// # use cp_sat::builder::CpModelBuilder;
300 /// # use cp_sat::proto::CpSolverStatus;
301 /// let mut model = CpModelBuilder::default();
302 /// let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect();
303 /// model.add_at_most_one(vars.iter().copied());
304 /// let response = model.solve();
305 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
306 /// assert!(
307 /// vars.iter()
308 /// .map(|v| v.solution_value(&response) as u32)
309 /// .sum::<u32>()
310 /// <= 1
311 /// );
312 /// ```
313 pub fn add_at_most_one(&mut self, vars: impl IntoIterator<Item = BoolVar>) -> Constraint {
314 self.add_cst(CstEnum::AtMostOne(proto::BoolArgumentProto {
315 literals: vars.into_iter().map(|v| v.0).collect(),
316 }))
317 }
318
319 /// Adds a boolean "exactly one" constraint on a list of [BoolVar].
320 ///
321 /// # Example
322 ///
323 /// ```
324 /// # use cp_sat::builder::CpModelBuilder;
325 /// # use cp_sat::proto::CpSolverStatus;
326 /// let mut model = CpModelBuilder::default();
327 /// let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect();
328 /// model.add_exactly_one(vars.iter().copied());
329 /// let response = model.solve();
330 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
331 /// assert!(
332 /// vars.iter()
333 /// .map(|v| v.solution_value(&response) as u32)
334 /// .sum::<u32>()
335 /// == 1
336 /// );
337 /// ```
338 pub fn add_exactly_one(&mut self, vars: impl IntoIterator<Item = BoolVar>) -> Constraint {
339 self.add_cst(CstEnum::ExactlyOne(proto::BoolArgumentProto {
340 literals: vars.into_iter().map(|v| v.0).collect(),
341 }))
342 }
343
344 /// Adds a boolean XOR constraint on a list of [BoolVar].
345 ///
346 /// # Example
347 ///
348 /// ```
349 /// # use cp_sat::builder::CpModelBuilder;
350 /// # use cp_sat::proto::CpSolverStatus;
351 /// let mut model = CpModelBuilder::default();
352 /// let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect();
353 /// model.add_xor(vars.iter().copied());
354 /// let response = model.solve();
355 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
356 /// assert!(
357 /// vars.iter()
358 /// .map(|v| v.solution_value(&response) as u32)
359 /// .sum::<u32>()
360 /// % 2
361 /// == 1
362 /// );
363 /// ```
364 pub fn add_xor(&mut self, vars: impl IntoIterator<Item = BoolVar>) -> Constraint {
365 self.add_cst(CstEnum::BoolXor(proto::BoolArgumentProto {
366 literals: vars.into_iter().map(|v| v.0).collect(),
367 }))
368 }
369
370 /// Adds a "all different" constraint on a list of [BoolVar].
371 ///
372 /// # Example
373 ///
374 /// ```
375 /// # use cp_sat::builder::CpModelBuilder;
376 /// # use cp_sat::proto::CpSolverStatus;
377 /// let mut model = CpModelBuilder::default();
378 /// let x = model.new_int_var([(0, 2)]);
379 /// let y = model.new_int_var([(0, 2)]);
380 /// let z = model.new_int_var([(0, 2)]);
381 /// model.add_all_different([x, y, z]);
382 /// let response = model.solve();
383 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
384 /// let x_val = x.solution_value(&response);
385 /// let y_val = y.solution_value(&response);
386 /// let z_val = z.solution_value(&response);
387 /// assert!(x_val != y_val);
388 /// assert!(x_val != z_val);
389 /// assert!(y_val != z_val);
390 /// ```
391 pub fn add_all_different(
392 &mut self,
393 exprs: impl IntoIterator<Item = impl Into<LinearExpr>>,
394 ) -> Constraint {
395 self.add_cst(CstEnum::AllDiff(proto::AllDifferentConstraintProto {
396 exprs: exprs
397 .into_iter()
398 .map(Into::into)
399 .map(|expr| proto::LinearExpressionProto {
400 vars: expr.vars.into_vec(),
401 coeffs: expr.coeffs.into_vec(),
402 offset: expr.constant,
403 })
404 .collect(),
405 }))
406 }
407
408 /// Adds a linear constraint.
409 ///
410 /// # Example
411 ///
412 /// ```
413 /// # use cp_sat::builder::CpModelBuilder;
414 /// # use cp_sat::proto::CpSolverStatus;
415 /// let mut model = CpModelBuilder::default();
416 /// let x = model.new_int_var([(0, 100)]);
417 /// let y = model.new_int_var([(0, 100)]);
418 /// model.add_linear_constraint([(1, x), (3, y)], [(301, i64::MAX)]);
419 /// let response = model.solve();
420 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
421 /// assert!(x.solution_value(&response) + 3 * y.solution_value(&response) >= 301);
422 /// ```
423 pub fn add_linear_constraint(
424 &mut self,
425 expr: impl Into<LinearExpr>,
426 domain: impl IntoIterator<Item = (i64, i64)>,
427 ) -> Constraint {
428 let expr = expr.into();
429 let constant = expr.constant;
430 self.add_cst(CstEnum::Linear(proto::LinearConstraintProto {
431 vars: expr.vars.into_vec(),
432 coeffs: expr.coeffs.into_vec(),
433 domain: domain
434 .into_iter()
435 .flat_map(|(begin, end)| {
436 [
437 if begin == i64::MIN {
438 i64::MIN
439 } else {
440 begin.saturating_sub(constant)
441 },
442 if end == i64::MAX {
443 i64::MAX
444 } else {
445 end.saturating_sub(constant)
446 },
447 ]
448 })
449 .collect(),
450 }))
451 }
452
453 /// Adds an equality constraint between 2 linear expressions.
454 ///
455 /// # Example
456 ///
457 /// ```
458 /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
459 /// # use cp_sat::proto::CpSolverStatus;
460 /// let mut model = CpModelBuilder::default();
461 /// let x = model.new_int_var([(0, 50)]);
462 /// let y = model.new_int_var([(53, 100)]);
463 /// model.add_eq(y, LinearExpr::from(x) + 3);
464 /// let response = model.solve();
465 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
466 /// assert_eq!(y.solution_value(&response), x.solution_value(&response) + 3);
467 /// assert_eq!(50, x.solution_value(&response));
468 /// assert_eq!(53, y.solution_value(&response));
469 /// ```
470 pub fn add_eq<T: Into<LinearExpr>, U: Into<LinearExpr>>(
471 &mut self,
472 lhs: T,
473 rhs: U,
474 ) -> Constraint {
475 self.add_linear_constraint(lhs.into() - rhs.into(), [(0, 0)])
476 }
477
478 /// Adds a greater or equal constraint between 2 linear expressions.
479 ///
480 /// # Example
481 ///
482 /// ```
483 /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
484 /// # use cp_sat::proto::CpSolverStatus;
485 /// let mut model = CpModelBuilder::default();
486 /// let x = model.new_int_var([(0, 50)]);
487 /// let y = model.new_int_var([(50, 100)]);
488 /// model.add_ge(x, y);
489 /// let response = model.solve();
490 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
491 /// assert!(x.solution_value(&response) >= y.solution_value(&response));
492 /// assert_eq!(50, x.solution_value(&response));
493 /// assert_eq!(50, y.solution_value(&response));
494 /// ```
495 pub fn add_ge<T: Into<LinearExpr>, U: Into<LinearExpr>>(
496 &mut self,
497 lhs: T,
498 rhs: U,
499 ) -> Constraint {
500 self.add_linear_constraint(lhs.into() - rhs.into(), [(0, i64::MAX)])
501 }
502
503 /// Adds a lesser or equal constraint between 2 linear expressions.
504 ///
505 /// # Example
506 ///
507 /// ```
508 /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
509 /// # use cp_sat::proto::CpSolverStatus;
510 /// let mut model = CpModelBuilder::default();
511 /// let x = model.new_int_var([(50, 100)]);
512 /// let y = model.new_int_var([(0, 50)]);
513 /// model.add_le(x, y);
514 /// let response = model.solve();
515 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
516 /// assert!(x.solution_value(&response) <= y.solution_value(&response));
517 /// assert_eq!(50, x.solution_value(&response));
518 /// assert_eq!(50, y.solution_value(&response));
519 /// ```
520 pub fn add_le<T: Into<LinearExpr>, U: Into<LinearExpr>>(
521 &mut self,
522 lhs: T,
523 rhs: U,
524 ) -> Constraint {
525 self.add_linear_constraint(lhs.into() - rhs.into(), [(i64::MIN, 0)])
526 }
527
528 /// Adds a stricly greater constraint between 2 linear expressions.
529 ///
530 /// # Example
531 ///
532 /// ```
533 /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
534 /// # use cp_sat::proto::CpSolverStatus;
535 /// let mut model = CpModelBuilder::default();
536 /// let x = model.new_int_var([(0, 51)]);
537 /// let y = model.new_int_var([(50, 100)]);
538 /// model.add_gt(x, y);
539 /// let response = model.solve();
540 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
541 /// assert!(x.solution_value(&response) > y.solution_value(&response));
542 /// assert_eq!(51, x.solution_value(&response));
543 /// assert_eq!(50, y.solution_value(&response));
544 /// ```
545 pub fn add_gt<T: Into<LinearExpr>, U: Into<LinearExpr>>(
546 &mut self,
547 lhs: T,
548 rhs: U,
549 ) -> Constraint {
550 self.add_linear_constraint(lhs.into() - rhs.into(), [(1, i64::MAX)])
551 }
552
553 /// Adds a strictly lesser constraint between 2 linear expressions.
554 ///
555 /// # Example
556 ///
557 /// ```
558 /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
559 /// # use cp_sat::proto::CpSolverStatus;
560 /// let mut model = CpModelBuilder::default();
561 /// let x = model.new_int_var([(50, 100)]);
562 /// let y = model.new_int_var([(0, 51)]);
563 /// model.add_lt(x, y);
564 /// let response = model.solve();
565 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
566 /// assert!(x.solution_value(&response) < y.solution_value(&response));
567 /// assert_eq!(50, x.solution_value(&response));
568 /// assert_eq!(51, y.solution_value(&response));
569 /// ```
570 pub fn add_lt<T: Into<LinearExpr>, U: Into<LinearExpr>>(
571 &mut self,
572 lhs: T,
573 rhs: U,
574 ) -> Constraint {
575 self.add_linear_constraint(lhs.into() - rhs.into(), [(i64::MIN, -1)])
576 }
577
578 /// Adds a not equal constraint between 2 linear expressions.
579 ///
580 /// # Example
581 ///
582 /// ```
583 /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
584 /// # use cp_sat::proto::CpSolverStatus;
585 /// let mut model = CpModelBuilder::default();
586 /// let x = model.new_bool_var();
587 /// model.add_ne(x, 1);
588 /// let response = model.solve();
589 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
590 /// assert!(x.solution_value(&response) as i64 != 1);
591 /// assert!(!x.solution_value(&response));
592 /// ```
593 pub fn add_ne<T: Into<LinearExpr>, U: Into<LinearExpr>>(
594 &mut self,
595 lhs: T,
596 rhs: U,
597 ) -> Constraint {
598 self.add_linear_constraint(lhs.into() - rhs.into(), [(i64::MIN, -1), (1, i64::MAX)])
599 }
600
601 /// Adds a constraint that force the `target` to be equal to the
602 /// minimum of the given `exprs`.
603 ///
604 /// # Example
605 ///
606 /// ```
607 /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
608 /// # use cp_sat::proto::CpSolverStatus;
609 /// let mut model = CpModelBuilder::default();
610 /// let x = model.new_int_var([(0, 10)]);
611 /// let y = model.new_int_var([(5, 15)]);
612 /// let m = model.new_int_var([(-100, 100)]);
613 /// model.add_min_eq(m, [x, y]);
614 /// model.maximize(m);
615 /// let response = model.solve();
616 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
617 /// assert_eq!(10., response.objective_value);
618 /// assert_eq!(10, m.solution_value(&response));
619 /// ```
620 pub fn add_min_eq(
621 &mut self,
622 target: impl Into<LinearExpr>,
623 exprs: impl IntoIterator<Item = impl Into<LinearExpr>>,
624 ) -> Constraint {
625 self.add_cst(CstEnum::LinMax(proto::LinearArgumentProto {
626 target: Some((-target.into()).into()),
627 exprs: exprs
628 .into_iter()
629 .map(|expr| (-expr.into()).into())
630 .collect(),
631 }))
632 }
633
634 /// Adds a constraint that force the `target` to be equal to the
635 /// maximum of the given `exprs`.
636 ///
637 /// # Example
638 ///
639 /// ```
640 /// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
641 /// # use cp_sat::proto::CpSolverStatus;
642 /// let mut model = CpModelBuilder::default();
643 /// let x = model.new_int_var([(0, 10)]);
644 /// let y = model.new_int_var([(5, 15)]);
645 /// let m = model.new_int_var([(-100, 100)]);
646 /// model.add_max_eq(m, [x, y]);
647 /// model.minimize(m);
648 /// let response = model.solve();
649 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
650 /// assert_eq!(5., response.objective_value);
651 /// assert_eq!(5, m.solution_value(&response));
652 /// ```
653 pub fn add_max_eq(
654 &mut self,
655 target: impl Into<LinearExpr>,
656 exprs: impl IntoIterator<Item = impl Into<LinearExpr>>,
657 ) -> Constraint {
658 self.add_cst(CstEnum::LinMax(proto::LinearArgumentProto {
659 target: Some(target.into().into()),
660 exprs: exprs.into_iter().map(|e| e.into().into()).collect(),
661 }))
662 }
663 fn add_cst(&mut self, cst: CstEnum) -> Constraint {
664 let index = self.proto.constraints.len();
665 self.proto.constraints.push(proto::ConstraintProto {
666 constraint: Some(cst),
667 ..Default::default()
668 });
669 Constraint(index)
670 }
671
672 /// Add a solution hint.
673 ///
674 /// # Example
675 ///
676 /// ```
677 /// # use cp_sat::builder::CpModelBuilder;
678 /// # use cp_sat::proto::CpSolverStatus;
679 /// let mut model = CpModelBuilder::default();
680 /// let x = model.new_int_var([(0, 100)]);
681 /// let y = model.new_bool_var();
682 /// model.add_hint(x, 42);
683 /// model.add_hint(y, 1);
684 /// let response = model.solve();
685 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
686 /// ```
687 pub fn add_hint(&mut self, var: impl Into<IntVar>, value: i64) {
688 let var = var.into();
689 let hints = self
690 .proto
691 .solution_hint
692 .get_or_insert_with(Default::default);
693 if var.0 < 0 {
694 hints.vars.push(var.not().0);
695 hints.values.push(1 - value);
696 } else {
697 hints.vars.push(var.0);
698 hints.values.push(value);
699 }
700 }
701
702 /// Delete all solution hints.
703 ///
704 /// # Example
705 ///
706 /// ```
707 /// # use cp_sat::builder::CpModelBuilder;
708 /// # use cp_sat::proto::CpSolverStatus;
709 /// let mut model = CpModelBuilder::default();
710 /// let x = model.new_int_var([(0, 100)]);
711 /// let y = model.new_bool_var();
712 /// model.add_hint(x, 42);
713 /// model.add_hint(y, 1);
714 /// model.del_hints();
715 /// model.add_hint(x, 75);
716 /// model.add_hint(y, 0);
717 /// let response = model.solve();
718 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
719 /// ```
720 pub fn del_hints(&mut self) {
721 self.proto.solution_hint = None;
722 }
723
724 /// Sets the minimization objective.
725 ///
726 /// # Example
727 ///
728 /// ```
729 /// # use cp_sat::builder::CpModelBuilder;
730 /// # use cp_sat::proto::CpSolverStatus;
731 /// let mut model = CpModelBuilder::default();
732 /// let x = model.new_int_var([(0, 100)]);
733 /// model.minimize(x);
734 /// let response = model.solve();
735 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
736 /// assert_eq!(0, x.solution_value(&response));
737 /// assert_eq!(0., response.objective_value);
738 /// ```
739 pub fn minimize<T: Into<LinearExpr>>(&mut self, expr: T) {
740 let expr = expr.into();
741 self.proto.objective = Some(proto::CpObjectiveProto {
742 vars: expr.vars.into_vec(),
743 coeffs: expr.coeffs.into_vec(),
744 offset: expr.constant as f64,
745 scaling_factor: 1.,
746 domain: vec![],
747 scaling_was_exact: false,
748 integer_before_offset: 0,
749 integer_after_offset: 0,
750 integer_scaling_factor: 0,
751 });
752 }
753
754 /// Sets the maximization objective.
755 ///
756 /// # Example
757 ///
758 /// ```
759 /// # use cp_sat::builder::CpModelBuilder;
760 /// # use cp_sat::proto::CpSolverStatus;
761 /// let mut model = CpModelBuilder::default();
762 /// let x = model.new_int_var([(0, 100)]);
763 /// model.maximize(x);
764 /// let response = model.solve();
765 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
766 /// assert_eq!(100, x.solution_value(&response));
767 /// assert_eq!(100., response.objective_value);
768 /// ```
769 pub fn maximize<T: Into<LinearExpr>>(&mut self, expr: T) {
770 let mut expr = expr.into();
771 for coeff in &mut expr.coeffs {
772 *coeff *= -1;
773 }
774 self.proto.objective = Some(proto::CpObjectiveProto {
775 vars: expr.vars.into_vec(),
776 coeffs: expr.coeffs.into_vec(),
777 offset: -expr.constant as f64,
778 scaling_factor: -1.,
779 domain: vec![],
780 scaling_was_exact: false,
781 integer_before_offset: 0,
782 integer_after_offset: 0,
783 integer_scaling_factor: 0,
784 });
785 }
786
787 /// Returns some statistics on the model.
788 ///
789 /// # Example
790 ///
791 /// ```
792 /// # use cp_sat::builder::CpModelBuilder;
793 /// let model = CpModelBuilder::default();
794 /// let stats = model.stats();
795 /// assert!(!stats.is_empty());
796 /// ```
797 pub fn stats(&self) -> String {
798 ffi::cp_model_stats(self.proto())
799 }
800
801 /// Verifies that the given model satisfies all the properties
802 /// described in the proto comments. Returns an empty string if it is
803 /// the case, otherwise fails at the first error and returns a
804 /// human-readable description of the issue.
805 ///
806 /// # Example
807 ///
808 /// ```
809 /// # use cp_sat::builder::CpModelBuilder;
810 /// # use cp_sat::proto::CpSolverStatus;
811 /// let mut model = CpModelBuilder::default();
812 /// let x = model.new_int_var([(0, -1)]);
813 /// model.maximize(x);
814 /// assert!(!model.validate_cp_model().is_empty());
815 /// ```
816 pub fn validate_cp_model(&self) -> String {
817 ffi::validate_cp_model(self.proto())
818 }
819
820 /// Solves the model, and returns the corresponding [proto::CpSolverResponse].
821 ///
822 /// # Example
823 ///
824 /// ```
825 /// # use cp_sat::builder::CpModelBuilder;
826 /// # use cp_sat::proto::CpSolverStatus;
827 /// let model = CpModelBuilder::default();
828 /// let response = model.solve();
829 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
830 /// ```
831 pub fn solve(&self) -> proto::CpSolverResponse {
832 ffi::solve(self.proto())
833 }
834
835 /// Solves the model with the given
836 /// [parameters][proto::SatParameters], and returns the
837 /// corresponding [proto::CpSolverResponse].
838 ///
839 /// # Example
840 ///
841 /// ```
842 /// # use cp_sat::builder::CpModelBuilder;
843 /// # use cp_sat::proto::{CpSolverStatus, SatParameters};
844 /// let model = CpModelBuilder::default();
845 /// let mut params = SatParameters::default();
846 /// params.max_deterministic_time = Some(1.);
847 /// let response = model.solve_with_parameters(¶ms);
848 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
849 /// ```
850 pub fn solve_with_parameters(&self, params: &proto::SatParameters) -> proto::CpSolverResponse {
851 ffi::solve_with_parameters(self.proto(), params)
852 }
853}
854
855/// Boolean variable identifier.
856#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
857pub struct BoolVar(i32);
858impl BoolVar {
859 /// Gets the solution value of the variable from a solution.
860 ///
861 /// The solution must come from the same model as the variable,
862 /// and a solution must be present in the response.
863 ///
864 /// # Example
865 ///
866 /// ```
867 /// # use cp_sat::builder::CpModelBuilder;
868 /// # use cp_sat::proto::{CpSolverStatus, SatParameters};
869 /// let mut model = CpModelBuilder::default();
870 /// let x = model.new_bool_var();
871 /// model.add_or([x]);
872 /// let response = model.solve();
873 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
874 /// assert!(x.solution_value(&response));
875 /// ```
876 #[track_caller]
877 pub fn solution_value(self, response: &proto::CpSolverResponse) -> bool {
878 if self.0 < 0 {
879 use std::ops::Not;
880 !self.not().solution_value(response)
881 } else {
882 response.solution[self.0 as usize] != 0
883 }
884 }
885}
886impl std::ops::Not for BoolVar {
887 type Output = Self;
888 fn not(self) -> Self {
889 Self(-self.0 - 1)
890 }
891}
892impl std::fmt::Debug for BoolVar {
893 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> Result<(), std::fmt::Error> {
894 if self.0 < 0 {
895 write!(f, "Not({:?})", !*self)
896 } else {
897 write!(f, "BoolVar({})", self.0)
898 }
899 }
900}
901
902impl std::ops::Mul<i64> for BoolVar {
903 type Output = LinearExpr;
904 fn mul(self, rhs: i64) -> Self::Output {
905 LinearExpr::from((rhs, self))
906 }
907}
908
909/// Integer variable identifier.
910#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
911pub struct IntVar(i32);
912impl From<BoolVar> for IntVar {
913 fn from(bool_var: BoolVar) -> IntVar {
914 IntVar(bool_var.0)
915 }
916}
917impl IntVar {
918 /// Gets the solution value of the variable from a solution.
919 ///
920 /// The solution must come from the same model as the variable,
921 /// and a solution must be present in the response.
922 ///
923 /// # Example
924 ///
925 /// ```
926 /// # use cp_sat::builder::CpModelBuilder;
927 /// # use cp_sat::proto::{CpSolverStatus, SatParameters};
928 /// let mut model = CpModelBuilder::default();
929 /// let x = model.new_int_var([(0, 42)]);
930 /// model.maximize(x);
931 /// let response = model.solve();
932 /// assert_eq!(response.status(), CpSolverStatus::Optimal);
933 /// assert_eq!(42, x.solution_value(&response));
934 /// ```
935 #[track_caller]
936 pub fn solution_value(self, response: &proto::CpSolverResponse) -> i64 {
937 if self.0 < 0 {
938 1 - self.not().solution_value(response)
939 } else {
940 response.solution[self.0 as usize]
941 }
942 }
943 fn not(self) -> Self {
944 IntVar::from(!BoolVar(self.0))
945 }
946}
947
948/// Constraint identifier.
949#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
950pub struct Constraint(usize);
951
952/// A linear expression, used in several places in the
953/// [builder][CpModelBuilder].
954///
955/// It describes an expression in the form `ax+by+c`. Several [From]
956/// and [std::ops] traits are implemented for easy modeling.
957///
958/// # Example
959///
960/// Most of the builder methods that takes something linear take in
961/// practice a `impl Into<LinearExpr>`. In the example, we will use
962/// [CpModelBuilder::maximize].
963///
964/// ```
965/// # use cp_sat::builder::{CpModelBuilder, LinearExpr};
966/// let mut model = CpModelBuilder::default();
967/// let x1 = model.new_int_var([(0, 100)]);
968/// let x2 = model.new_int_var([(0, 100)]);
969/// let y1 = model.new_bool_var();
970/// let y2 = model.new_bool_var();
971/// model.maximize(x1); // IntVar can be converted in LinearExpr
972/// model.maximize(y1); // as BoolVar
973/// model.maximize(42); // as i64
974/// model.maximize((42, x1)); // this means maximize 42 * x1
975/// model.maximize((42, y1)); // works also with BoolVar
976/// model.maximize([(42, x1), (1337, x2)]); // with array: 42*x1 + 1337*x2
977/// model.maximize([(42, y1), (1337, y2)]); // with array: also with bool
978/// model.maximize([(42, x1), (1337, y2.into())]); // BoolVar conversion
979///
980/// // for easy looping, we can also modify a LinearExpr
981/// let vars: Vec<_> = (0..10).map(|_| model.new_bool_var()).collect();
982/// let mut expr = LinearExpr::default(); // means 0, can also be LinearExpr::from(0)
983/// for (i, v) in vars.iter().copied().enumerate() {
984/// match i {
985/// 0..=1 => expr += (i as i64, v),
986/// 2..=3 => expr -= (42, v),
987/// 4..=5 => expr += v,
988/// _ => expr -= LinearExpr::from([(42, v), (1337, y1)]) + 5,
989/// }
990/// }
991///
992/// // an iterator of `Into<LinearExpr>` can be collected or extended,
993/// // meaning summing the elements
994/// model.maximize(vars.iter().copied().collect::<LinearExpr>()); // means sum(vars)
995/// expr.extend(vars.iter().map(|&v| (2, v))); // means expr += sum_vars(2 * v)
996/// ```
997#[derive(Clone, Default, Debug)]
998pub struct LinearExpr {
999 vars: SmallVec<[i32; 4]>,
1000 coeffs: SmallVec<[i64; 2]>,
1001 constant: i64,
1002}
1003
1004impl<E: Into<LinearExpr>> std::ops::AddAssign<E> for LinearExpr {
1005 fn add_assign(&mut self, rhs: E) {
1006 let mut rhs = rhs.into();
1007 if self.vars.len() < rhs.vars.len() {
1008 std::mem::swap(self, &mut rhs);
1009 }
1010 self.vars.extend_from_slice(&rhs.vars);
1011 self.coeffs.extend_from_slice(&rhs.coeffs);
1012 self.constant += rhs.constant;
1013 }
1014}
1015impl std::ops::Neg for LinearExpr {
1016 type Output = LinearExpr;
1017 fn neg(mut self) -> Self::Output {
1018 for c in &mut self.coeffs {
1019 *c = -*c;
1020 }
1021 self.constant = -self.constant;
1022 self
1023 }
1024}
1025impl<L: Into<LinearExpr>> std::ops::SubAssign<L> for LinearExpr {
1026 fn sub_assign(&mut self, rhs: L) {
1027 *self += -rhs.into();
1028 }
1029}
1030
1031impl<V: Into<IntVar>> From<V> for LinearExpr {
1032 fn from(var: V) -> Self {
1033 Self::from((1, var))
1034 }
1035}
1036impl From<i64> for LinearExpr {
1037 fn from(constant: i64) -> Self {
1038 let mut res = Self::default();
1039 res.constant += constant;
1040 res
1041 }
1042}
1043impl<V: Into<IntVar>> From<(i64, V)> for LinearExpr {
1044 fn from((coeff, var): (i64, V)) -> Self {
1045 let mut res = Self::default();
1046 let var = var.into();
1047 if var.0 < 0 {
1048 res.vars.push(var.not().0);
1049 res.coeffs.push(-coeff);
1050 res.constant += coeff;
1051 } else {
1052 res.vars.push(var.0);
1053 res.coeffs.push(coeff);
1054 }
1055 res
1056 }
1057}
1058impl<V: Into<IntVar>, const L: usize> From<[(i64, V); L]> for LinearExpr {
1059 fn from(expr: [(i64, V); L]) -> Self {
1060 let mut res = Self::default();
1061 for term in expr {
1062 res += term;
1063 }
1064 res
1065 }
1066}
1067
1068impl<T: Into<LinearExpr>> std::ops::Add<T> for LinearExpr {
1069 type Output = LinearExpr;
1070 fn add(mut self, rhs: T) -> Self::Output {
1071 self += rhs.into();
1072 self
1073 }
1074}
1075
1076impl<T: Into<LinearExpr>> std::ops::Sub<T> for LinearExpr {
1077 type Output = LinearExpr;
1078 fn sub(mut self, rhs: T) -> Self::Output {
1079 self -= rhs.into();
1080 self
1081 }
1082}
1083
1084impl std::ops::Mul<i64> for LinearExpr {
1085 type Output = LinearExpr;
1086 fn mul(mut self, rhs: i64) -> Self::Output {
1087 for c in &mut self.coeffs {
1088 *c *= rhs;
1089 }
1090 self.constant *= rhs;
1091 self
1092 }
1093}
1094
1095impl From<LinearExpr> for proto::LinearExpressionProto {
1096 fn from(expr: LinearExpr) -> Self {
1097 proto::LinearExpressionProto {
1098 vars: expr.vars.into_vec(),
1099 coeffs: expr.coeffs.into_vec(),
1100 offset: expr.constant,
1101 }
1102 }
1103}
1104
1105impl<T: Into<LinearExpr>> std::iter::Extend<T> for LinearExpr {
1106 fn extend<I: IntoIterator<Item = T>>(&mut self, iter: I) {
1107 for e in iter {
1108 *self += e;
1109 }
1110 }
1111}
1112impl<T: Into<LinearExpr>> std::iter::FromIterator<T> for LinearExpr {
1113 fn from_iter<I: IntoIterator<Item = T>>(iter: I) -> Self {
1114 let mut res = LinearExpr::default();
1115 res.extend(iter);
1116 res
1117 }
1118}