OR-Tools  8.2
cp_model.cc
Go to the documentation of this file.
1// Copyright 2010-2018 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
15
16#include "absl/strings/str_format.h"
18#include "ortools/sat/cp_model.pb.h"
21#include "ortools/sat/sat_parameters.pb.h"
22
23namespace operations_research {
24namespace sat {
25
26BoolVar::BoolVar() : cp_model_(nullptr), index_(0) {}
27
28BoolVar::BoolVar(int index, CpModelProto* cp_model)
29 : cp_model_(cp_model), index_(index) {}
30
31BoolVar BoolVar::WithName(const std::string& name) {
32 cp_model_->mutable_variables(index_)->set_name(name);
33 return *this;
34}
35
36std::string BoolVar::DebugString() const {
37 if (index_ < 0) {
38 return absl::StrFormat("Not(%s)", Not().DebugString());
39 } else {
40 std::string output;
41 const IntegerVariableProto& var_proto = cp_model_->variables(index_);
42 // Special case for constant variables without names.
43 if (var_proto.name().empty() && var_proto.domain_size() == 2 &&
44 var_proto.domain(0) == var_proto.domain(1)) {
45 output.append(var_proto.domain(0) == 0 ? "false" : "true");
46 } else {
47 if (var_proto.name().empty()) {
48 absl::StrAppendFormat(&output, "BoolVar%i(", index_);
49 } else {
50 absl::StrAppendFormat(&output, "%s(", var_proto.name());
51 }
52 if (var_proto.domain(0) == var_proto.domain(1)) {
53 output.append(var_proto.domain(0) == 0 ? "false)" : "true)");
54 } else {
55 absl::StrAppend(&output, var_proto.domain(0), ", ", var_proto.domain(1),
56 ")");
57 }
58 }
59 return output;
60 }
61}
62
63BoolVar Not(BoolVar x) { return x.Not(); }
64
65std::ostream& operator<<(std::ostream& os, const BoolVar& var) {
66 os << var.DebugString();
67 return os;
68}
69
70IntVar::IntVar() : cp_model_(nullptr), index_(0) {}
71
72IntVar::IntVar(int index, CpModelProto* cp_model)
73 : cp_model_(cp_model), index_(index) {
75}
76
77IntVar IntVar::WithName(const std::string& name) {
78 cp_model_->mutable_variables(index_)->set_name(name);
79 return *this;
80}
81
83 cp_model_ = var.cp_model_;
84 index_ = var.index_;
85}
86
88 CHECK_EQ(2, Proto().domain_size());
89 CHECK_GE(Proto().domain(0), 0);
90 CHECK_LE(Proto().domain(1), 1);
92 var.cp_model_ = cp_model_;
93 var.index_ = index();
94 return var;
95}
96
98 return LinearExpr(*this).AddConstant(value);
99}
100
101std::string IntVar::DebugString() const {
102 if (index_ < 0) {
103 return absl::StrFormat("Not(%s)",
104 IntVar(NegatedRef(index_), cp_model_).DebugString());
105 }
106 const IntegerVariableProto& var_proto = cp_model_->variables(index_);
107 // Special case for constant variables without names.
108 if (var_proto.name().empty() && var_proto.domain_size() == 2 &&
109 var_proto.domain(0) == var_proto.domain(1)) {
110 return absl::StrCat(var_proto.domain(0));
111 } else {
112 std::string output;
113 if (var_proto.name().empty()) {
114 absl::StrAppend(&output, "IntVar", index_, "(");
115 } else {
116 absl::StrAppend(&output, var_proto.name(), "(");
117 }
118 if (var_proto.domain_size() == 2 &&
119 var_proto.domain(0) == var_proto.domain(1)) {
120 absl::StrAppend(&output, var_proto.domain(0), ")");
121 } else {
122 // TODO(user): Use domain pretty print function.
123 absl::StrAppend(&output, var_proto.domain(0), ", ", var_proto.domain(1),
124 ")");
125 }
126 return output;
127 }
128}
129
130std::ostream& operator<<(std::ostream& os, const IntVar& var) {
131 os << var.DebugString();
132 return os;
133}
134
136
138
140
141LinearExpr::LinearExpr(int64 constant) { constant_ = constant; }
142
143LinearExpr LinearExpr::Sum(absl::Span<const IntVar> vars) {
144 LinearExpr result;
145 for (const IntVar& var : vars) {
146 result.AddVar(var);
147 }
148 return result;
149}
150
151LinearExpr LinearExpr::ScalProd(absl::Span<const IntVar> vars,
152 absl::Span<const int64> coeffs) {
153 CHECK_EQ(vars.size(), coeffs.size());
154 LinearExpr result;
155 for (int i = 0; i < vars.size(); ++i) {
156 result.AddTerm(vars[i], coeffs[i]);
157 }
158 return result;
159}
160
162 LinearExpr result;
163 result.AddTerm(var, coefficient);
164 return result;
165}
166
167LinearExpr LinearExpr::BooleanSum(absl::Span<const BoolVar> vars) {
168 LinearExpr result;
169 for (const IntVar& var : vars) {
170 result.AddVar(var);
171 }
172 return result;
173}
174
175LinearExpr LinearExpr::BooleanScalProd(absl::Span<const BoolVar> vars,
176 absl::Span<const int64> coeffs) {
177 CHECK_EQ(vars.size(), coeffs.size());
178 LinearExpr result;
179 for (int i = 0; i < vars.size(); ++i) {
180 result.AddTerm(vars[i], coeffs[i]);
181 }
182 return result;
183}
184
186 constant_ += value;
187 return *this;
188}
189
191
193 const int index = var.index_;
194 if (RefIsPositive(index)) {
195 variables_.push_back(var);
196 coefficients_.push_back(coeff);
197 } else {
198 variables_.push_back(IntVar(PositiveRef(var.index_), var.cp_model_));
199 coefficients_.push_back(-coeff);
200 constant_ += coeff;
201 }
202}
203
204Constraint::Constraint(ConstraintProto* proto) : proto_(proto) {}
205
207 proto_->set_name(name);
208 return *this;
209}
210
211const std::string& Constraint::Name() const { return proto_->name(); }
212
213Constraint Constraint::OnlyEnforceIf(absl::Span<const BoolVar> literals) {
214 for (const BoolVar& var : literals) {
215 proto_->add_enforcement_literal(var.index_);
216 }
217 return *this;
218}
219
221 proto_->add_enforcement_literal(literal.index_);
222 return *this;
223}
224
226 proto_->mutable_circuit()->add_tails(tail);
227 proto_->mutable_circuit()->add_heads(head);
228 proto_->mutable_circuit()->add_literals(literal.index_);
229}
230
232 proto_->mutable_routes()->add_tails(tail);
233 proto_->mutable_routes()->add_heads(head);
234 proto_->mutable_routes()->add_literals(literal.index_);
235}
236
237void TableConstraint::AddTuple(absl::Span<const int64> tuple) {
238 CHECK_EQ(tuple.size(), proto_->table().vars_size());
239 for (const int64 t : tuple) {
240 proto_->mutable_table()->add_values(t);
241 }
242}
243
244ReservoirConstraint::ReservoirConstraint(ConstraintProto* proto,
245 CpModelBuilder* builder)
246 : Constraint(proto), builder_(builder) {}
247
249 proto_->mutable_reservoir()->add_times(
250 builder_->GetOrCreateIntegerIndex(time.index_));
251 proto_->mutable_reservoir()->add_demands(demand);
252 proto_->mutable_reservoir()->add_actives(builder_->IndexFromConstant(1));
253}
254
256 BoolVar is_active) {
257 proto_->mutable_reservoir()->add_times(
258 builder_->GetOrCreateIntegerIndex(time.index_));
259 proto_->mutable_reservoir()->add_demands(demand);
260 proto_->mutable_reservoir()->add_actives(is_active.index_);
261}
262
264 int64 transition_label) {
265 proto_->mutable_automaton()->add_transition_tail(tail);
266 proto_->mutable_automaton()->add_transition_head(head);
267 proto_->mutable_automaton()->add_transition_label(transition_label);
268}
269
271 IntervalVar y_coordinate) {
272 proto_->mutable_no_overlap_2d()->add_x_intervals(x_coordinate.index_);
273 proto_->mutable_no_overlap_2d()->add_y_intervals(y_coordinate.index_);
274}
275
276CumulativeConstraint::CumulativeConstraint(ConstraintProto* proto,
277 CpModelBuilder* builder)
278 : Constraint(proto), builder_(builder) {}
279
281 proto_->mutable_cumulative()->add_intervals(interval.index_);
282 proto_->mutable_cumulative()->add_demands(
283 builder_->GetOrCreateIntegerIndex(demand.index_));
284}
285
286IntervalVar::IntervalVar() : cp_model_(nullptr), index_() {}
287
288IntervalVar::IntervalVar(int index, CpModelProto* cp_model)
289 : cp_model_(cp_model), index_(index) {}
290
292 cp_model_->mutable_constraints(index_)->set_name(name);
293 return *this;
294}
295
297 return IntVar(Proto().start(), cp_model_);
298}
299
301 return IntVar(Proto().size(), cp_model_);
302}
303
304IntVar IntervalVar::EndVar() const { return IntVar(Proto().end(), cp_model_); }
305
307 return BoolVar(cp_model_->constraints(index_).enforcement_literal(0),
308 cp_model_);
309}
310
311std::string IntervalVar::Name() const {
312 return cp_model_->constraints(index_).name();
313}
314
315std::string IntervalVar::DebugString() const {
316 CHECK_GE(index_, 0);
317 const ConstraintProto& ct_proto = cp_model_->constraints(index_);
318 std::string output;
319 if (ct_proto.name().empty()) {
320 absl::StrAppend(&output, "IntervalVar", index_, "(");
321 } else {
322 absl::StrAppend(&output, ct_proto.name(), "(");
323 }
324 absl::StrAppend(&output, StartVar().DebugString(), ", ",
325 SizeVar().DebugString(), ", ", EndVar().DebugString(), ", ",
327 return output;
328}
329
330std::ostream& operator<<(std::ostream& os, const IntervalVar& var) {
331 os << var.DebugString();
332 return os;
333}
334
335int CpModelBuilder::IndexFromConstant(int64 value) {
336 if (!gtl::ContainsKey(constant_to_index_map_, value)) {
337 const int index = cp_model_.variables_size();
338 IntegerVariableProto* const var_proto = cp_model_.add_variables();
339 var_proto->add_domain(value);
340 var_proto->add_domain(value);
341 constant_to_index_map_[value] = index;
342 }
343 return constant_to_index_map_[value];
344}
345
346int CpModelBuilder::GetOrCreateIntegerIndex(int index) {
347 if (index >= 0) {
348 return index;
349 }
350 if (!gtl::ContainsKey(bool_to_integer_index_map_, index)) {
351 const int var = PositiveRef(index);
352 const IntegerVariableProto& old_var = cp_model_.variables(var);
353 const int new_index = cp_model_.variables_size();
354 IntegerVariableProto* const new_var = cp_model_.add_variables();
355 new_var->add_domain(0);
356 new_var->add_domain(1);
357 if (!old_var.name().empty()) {
358 new_var->set_name(absl::StrCat("Not(", old_var.name(), ")"));
359 }
360 AddEquality(IntVar(new_index, &cp_model_), BoolVar(index, &cp_model_));
361 bool_to_integer_index_map_[index] = new_index;
362 return new_index;
363 }
364 return bool_to_integer_index_map_[index];
365}
366
368 const int index = cp_model_.variables_size();
369 IntegerVariableProto* const var_proto = cp_model_.add_variables();
370 for (const auto& interval : domain) {
371 var_proto->add_domain(interval.start);
372 var_proto->add_domain(interval.end);
373 }
374 return IntVar(index, &cp_model_);
375}
376
378 const int index = cp_model_.variables_size();
379 IntegerVariableProto* const var_proto = cp_model_.add_variables();
380 var_proto->add_domain(0);
381 var_proto->add_domain(1);
382 return BoolVar(index, &cp_model_);
383}
384
386 return IntVar(IndexFromConstant(value), &cp_model_);
387}
388
390 return BoolVar(IndexFromConstant(1), &cp_model_);
391}
392
394 return BoolVar(IndexFromConstant(0), &cp_model_);
395}
396
398 IntVar end) {
399 return NewOptionalIntervalVar(start, size, end, TrueVar());
400}
401
403 IntVar end,
404 BoolVar presence) {
405 const int index = cp_model_.constraints_size();
406 ConstraintProto* const ct = cp_model_.add_constraints();
407 ct->add_enforcement_literal(presence.index_);
408 IntervalConstraintProto* const interval = ct->mutable_interval();
409 interval->set_start(GetOrCreateIntegerIndex(start.index_));
410 interval->set_size(GetOrCreateIntegerIndex(size.index_));
411 interval->set_end(GetOrCreateIntegerIndex(end.index_));
412 return IntervalVar(index, &cp_model_);
413}
414
415Constraint CpModelBuilder::AddBoolOr(absl::Span<const BoolVar> literals) {
416 ConstraintProto* const proto = cp_model_.add_constraints();
417 for (const BoolVar& lit : literals) {
418 proto->mutable_bool_or()->add_literals(lit.index_);
419 }
420 return Constraint(proto);
421}
422
423Constraint CpModelBuilder::AddBoolAnd(absl::Span<const BoolVar> literals) {
424 ConstraintProto* const proto = cp_model_.add_constraints();
425 for (const BoolVar& lit : literals) {
426 proto->mutable_bool_and()->add_literals(lit.index_);
427 }
428 return Constraint(proto);
429}
430
431Constraint CpModelBuilder::AddBoolXor(absl::Span<const BoolVar> literals) {
432 ConstraintProto* const proto = cp_model_.add_constraints();
433 for (const BoolVar& lit : literals) {
434 proto->mutable_bool_xor()->add_literals(lit.index_);
435 }
436 return Constraint(proto);
437}
438
439void CpModelBuilder::FillLinearTerms(const LinearExpr& left,
440 const LinearExpr& right,
441 LinearConstraintProto* proto) {
442 for (const IntVar& x : left.variables()) {
443 proto->add_vars(x.index_);
444 }
445 for (const int64 coeff : left.coefficients()) {
446 proto->add_coeffs(coeff);
447 }
448 for (const IntVar& x : right.variables()) {
449 proto->add_vars(x.index_);
450 }
451 for (const int64 coeff : right.coefficients()) {
452 proto->add_coeffs(-coeff);
453 }
454}
455
457 const LinearExpr& right) {
458 ConstraintProto* const proto = cp_model_.add_constraints();
459 FillLinearTerms(left, right, proto->mutable_linear());
460 const int64 rhs = right.constant() - left.constant();
461 proto->mutable_linear()->add_domain(rhs);
462 proto->mutable_linear()->add_domain(rhs);
463 return Constraint(proto);
464}
465
467 const LinearExpr& right) {
468 ConstraintProto* const proto = cp_model_.add_constraints();
469 FillLinearTerms(left, right, proto->mutable_linear());
470 const int64 rhs = right.constant() - left.constant();
471 proto->mutable_linear()->add_domain(rhs);
472 proto->mutable_linear()->add_domain(kint64max);
473 return Constraint(proto);
474}
475
477 const LinearExpr& right) {
478 ConstraintProto* const proto = cp_model_.add_constraints();
479 FillLinearTerms(left, right, proto->mutable_linear());
480 const int64 rhs = right.constant() - left.constant();
481 proto->mutable_linear()->add_domain(kint64min);
482 proto->mutable_linear()->add_domain(rhs);
483 return Constraint(proto);
484}
485
487 const LinearExpr& right) {
488 ConstraintProto* const proto = cp_model_.add_constraints();
489 FillLinearTerms(left, right, proto->mutable_linear());
490 const int64 rhs = right.constant() - left.constant();
491 proto->mutable_linear()->add_domain(rhs + 1);
492 proto->mutable_linear()->add_domain(kint64max);
493 return Constraint(proto);
494}
495
497 const LinearExpr& right) {
498 ConstraintProto* const proto = cp_model_.add_constraints();
499 FillLinearTerms(left, right, proto->mutable_linear());
500 const int64 rhs = right.constant() - left.constant();
501 proto->mutable_linear()->add_domain(kint64min);
502 proto->mutable_linear()->add_domain(rhs - 1);
503 return Constraint(proto);
504}
505
507 const Domain& domain) {
508 ConstraintProto* const proto = cp_model_.add_constraints();
509 for (const IntVar& x : expr.variables()) {
510 proto->mutable_linear()->add_vars(x.index_);
511 }
512 for (const int64 coeff : expr.coefficients()) {
513 proto->mutable_linear()->add_coeffs(coeff);
514 }
515 const int64 cst = expr.constant();
516 for (const auto& i : domain) {
517 proto->mutable_linear()->add_domain(i.start - cst);
518 proto->mutable_linear()->add_domain(i.end - cst);
519 }
520 return Constraint(proto);
521}
522
524 const LinearExpr& right) {
525 ConstraintProto* const proto = cp_model_.add_constraints();
526 FillLinearTerms(left, right, proto->mutable_linear());
527 const int64 rhs = right.constant() - left.constant();
528 proto->mutable_linear()->add_domain(kint64min);
529 proto->mutable_linear()->add_domain(rhs - 1);
530 proto->mutable_linear()->add_domain(rhs + 1);
531 proto->mutable_linear()->add_domain(kint64max);
532 return Constraint(proto);
533}
534
535Constraint CpModelBuilder::AddAllDifferent(absl::Span<const IntVar> vars) {
536 ConstraintProto* const proto = cp_model_.add_constraints();
537 for (const IntVar& var : vars) {
538 proto->mutable_all_diff()->add_vars(GetOrCreateIntegerIndex(var.index_));
539 }
540 return Constraint(proto);
541}
542
544 IntVar index, absl::Span<const IntVar> variables, IntVar target) {
545 ConstraintProto* const proto = cp_model_.add_constraints();
546 proto->mutable_element()->set_index(GetOrCreateIntegerIndex(index.index_));
547 proto->mutable_element()->set_target(GetOrCreateIntegerIndex(target.index_));
548 for (const IntVar& var : variables) {
549 proto->mutable_element()->add_vars(GetOrCreateIntegerIndex(var.index_));
550 }
551 return Constraint(proto);
552}
553
555 absl::Span<const int64> values,
556 IntVar target) {
557 ConstraintProto* const proto = cp_model_.add_constraints();
558 proto->mutable_element()->set_index(GetOrCreateIntegerIndex(index.index_));
559 proto->mutable_element()->set_target(GetOrCreateIntegerIndex(target.index_));
560 for (int64 value : values) {
561 proto->mutable_element()->add_vars(IndexFromConstant(value));
562 }
563 return Constraint(proto);
564}
565
567 return CircuitConstraint(cp_model_.add_constraints());
568}
569
571 return MultipleCircuitConstraint(cp_model_.add_constraints());
572}
573
575 absl::Span<const IntVar> vars) {
576 ConstraintProto* const proto = cp_model_.add_constraints();
577 for (const IntVar& var : vars) {
578 proto->mutable_table()->add_vars(GetOrCreateIntegerIndex(var.index_));
579 }
580 return TableConstraint(proto);
581}
582
584 absl::Span<const IntVar> vars) {
585 ConstraintProto* const proto = cp_model_.add_constraints();
586 for (const IntVar& var : vars) {
587 proto->mutable_table()->add_vars(GetOrCreateIntegerIndex(var.index_));
588 }
589 proto->mutable_table()->set_negated(true);
590 return TableConstraint(proto);
591}
592
594 absl::Span<const IntVar> variables,
595 absl::Span<const IntVar> inverse_variables) {
596 ConstraintProto* const proto = cp_model_.add_constraints();
597 for (const IntVar& var : variables) {
598 proto->mutable_inverse()->add_f_direct(GetOrCreateIntegerIndex(var.index_));
599 }
600 for (const IntVar& var : inverse_variables) {
601 proto->mutable_inverse()->add_f_inverse(
602 GetOrCreateIntegerIndex(var.index_));
603 }
604 return Constraint(proto);
605}
606
608 int64 max_level) {
609 ConstraintProto* const proto = cp_model_.add_constraints();
610 proto->mutable_reservoir()->set_min_level(min_level);
611 proto->mutable_reservoir()->set_max_level(max_level);
612 return ReservoirConstraint(proto, this);
613}
614
616 absl::Span<const IntVar> transition_variables, int starting_state,
617 absl::Span<const int> final_states) {
618 ConstraintProto* const proto = cp_model_.add_constraints();
619 for (const IntVar& var : transition_variables) {
620 proto->mutable_automaton()->add_vars(GetOrCreateIntegerIndex(var.index_));
621 }
622 proto->mutable_automaton()->set_starting_state(starting_state);
623 for (const int final_state : final_states) {
624 proto->mutable_automaton()->add_final_states(final_state);
625 }
627}
628
630 absl::Span<const IntVar> vars) {
631 ConstraintProto* const proto = cp_model_.add_constraints();
632 proto->mutable_int_min()->set_target(GetOrCreateIntegerIndex(target.index_));
633 for (const IntVar& var : vars) {
634 proto->mutable_int_min()->add_vars(GetOrCreateIntegerIndex(var.index_));
635 }
636 return Constraint(proto);
637}
638
639void CpModelBuilder::LinearExprToProto(const LinearExpr& expr,
640 LinearExpressionProto* expr_proto) {
641 for (const IntVar var : expr.variables()) {
642 expr_proto->add_vars(GetOrCreateIntegerIndex(var.index_));
643 }
644 for (const int64 coeff : expr.coefficients()) {
645 expr_proto->add_coeffs(coeff);
646 }
647 expr_proto->set_offset(expr.constant());
648}
649
651 const LinearExpr& target, absl::Span<const LinearExpr> exprs) {
652 ConstraintProto* const proto = cp_model_.add_constraints();
653 LinearExprToProto(target, proto->mutable_lin_min()->mutable_target());
654 for (const LinearExpr& expr : exprs) {
655 LinearExpressionProto* expr_proto = proto->mutable_lin_min()->add_exprs();
656 LinearExprToProto(expr, expr_proto);
657 }
658 return Constraint(proto);
659}
660
662 absl::Span<const IntVar> vars) {
663 ConstraintProto* const proto = cp_model_.add_constraints();
664 proto->mutable_int_max()->set_target(GetOrCreateIntegerIndex(target.index_));
665 for (const IntVar& var : vars) {
666 proto->mutable_int_max()->add_vars(GetOrCreateIntegerIndex(var.index_));
667 }
668 return Constraint(proto);
669}
670
672 const LinearExpr& target, absl::Span<const LinearExpr> exprs) {
673 ConstraintProto* const proto = cp_model_.add_constraints();
674 LinearExprToProto(target, proto->mutable_lin_max()->mutable_target());
675 for (const LinearExpr& expr : exprs) {
676 LinearExpressionProto* expr_proto = proto->mutable_lin_max()->add_exprs();
677 LinearExprToProto(expr, expr_proto);
678 }
679 return Constraint(proto);
680}
681
683 IntVar denominator) {
684 ConstraintProto* const proto = cp_model_.add_constraints();
685 proto->mutable_int_div()->set_target(GetOrCreateIntegerIndex(target.index_));
686 proto->mutable_int_div()->add_vars(GetOrCreateIntegerIndex(numerator.index_));
687 proto->mutable_int_div()->add_vars(
688 GetOrCreateIntegerIndex(denominator.index_));
689 return Constraint(proto);
690}
691
693 ConstraintProto* const proto = cp_model_.add_constraints();
694 proto->mutable_int_max()->set_target(GetOrCreateIntegerIndex(target.index_));
695 proto->mutable_int_max()->add_vars(GetOrCreateIntegerIndex(var.index_));
696 proto->mutable_int_max()->add_vars(
697 NegatedRef(GetOrCreateIntegerIndex(var.index_)));
698 return Constraint(proto);
699}
700
702 IntVar mod) {
703 ConstraintProto* const proto = cp_model_.add_constraints();
704 proto->mutable_int_mod()->set_target(GetOrCreateIntegerIndex(target.index_));
705 proto->mutable_int_mod()->add_vars(GetOrCreateIntegerIndex(var.index_));
706 proto->mutable_int_mod()->add_vars(GetOrCreateIntegerIndex(mod.index_));
707 return Constraint(proto);
708}
709
711 absl::Span<const IntVar> vars) {
712 ConstraintProto* const proto = cp_model_.add_constraints();
713 proto->mutable_int_prod()->set_target(GetOrCreateIntegerIndex(target.index_));
714 for (const IntVar& var : vars) {
715 proto->mutable_int_prod()->add_vars(GetOrCreateIntegerIndex(var.index_));
716 }
717 return Constraint(proto);
718}
719
720Constraint CpModelBuilder::AddNoOverlap(absl::Span<const IntervalVar> vars) {
721 ConstraintProto* const proto = cp_model_.add_constraints();
722 for (const IntervalVar& var : vars) {
723 proto->mutable_no_overlap()->add_intervals(
724 GetOrCreateIntegerIndex(var.index_));
725 }
726 return Constraint(proto);
727}
728
730 return NoOverlap2DConstraint(cp_model_.add_constraints());
731}
732
734 ConstraintProto* const proto = cp_model_.add_constraints();
735 proto->mutable_cumulative()->set_capacity(
736 GetOrCreateIntegerIndex(capacity.index_));
737 return CumulativeConstraint(proto, this);
738}
739
741 cp_model_.mutable_objective()->Clear();
742 for (const IntVar& x : expr.variables()) {
743 cp_model_.mutable_objective()->add_vars(x.index_);
744 }
745 for (const int64 coeff : expr.coefficients()) {
746 cp_model_.mutable_objective()->add_coeffs(coeff);
747 }
748 cp_model_.mutable_objective()->set_offset(expr.constant());
749}
750
752 cp_model_.mutable_objective()->Clear();
753 for (const IntVar& x : expr.variables()) {
754 cp_model_.mutable_objective()->add_vars(x.index_);
755 }
756 for (const int64 coeff : expr.coefficients()) {
757 cp_model_.mutable_objective()->add_coeffs(-coeff);
758 }
759 cp_model_.mutable_objective()->set_offset(-expr.constant());
760 cp_model_.mutable_objective()->set_scaling_factor(-1.0);
761}
762
764 CHECK(cp_model_.has_objective());
765 cp_model_.mutable_objective()->set_scaling_factor(
766 scaling * cp_model_.objective().scaling_factor());
767}
768
770 absl::Span<const IntVar> variables,
771 DecisionStrategyProto::VariableSelectionStrategy var_strategy,
772 DecisionStrategyProto::DomainReductionStrategy domain_strategy) {
773 DecisionStrategyProto* const proto = cp_model_.add_search_strategy();
774 for (const IntVar& var : variables) {
775 proto->add_variables(var.index_);
776 }
777 proto->set_variable_selection_strategy(var_strategy);
778 proto->set_domain_reduction_strategy(domain_strategy);
779}
780
782 absl::Span<const BoolVar> variables,
783 DecisionStrategyProto::VariableSelectionStrategy var_strategy,
784 DecisionStrategyProto::DomainReductionStrategy domain_strategy) {
785 DecisionStrategyProto* const proto = cp_model_.add_search_strategy();
786 for (const BoolVar& var : variables) {
787 proto->add_variables(var.index_);
788 }
789 proto->set_variable_selection_strategy(var_strategy);
790 proto->set_domain_reduction_strategy(domain_strategy);
791}
792
794 cp_model_.mutable_solution_hint()->add_vars(
795 GetOrCreateIntegerIndex(var.index_));
796 cp_model_.mutable_solution_hint()->add_values(value);
797}
798
800 cp_model_.mutable_solution_hint()->Clear();
801}
802
804 cp_model_.mutable_assumptions()->Add(lit.index_);
805}
806
807void CpModelBuilder::AddAssumptions(absl::Span<const BoolVar> literals) {
808 for (const BoolVar& lit : literals) {
809 cp_model_.mutable_assumptions()->Add(lit.index_);
810 }
811}
812
814 cp_model_.mutable_assumptions()->Clear();
815}
816
817void CpModelBuilder::CopyFrom(const CpModelProto& model_proto) {
818 cp_model_ = model_proto;
819 // Rebuild constant to index map.
820 constant_to_index_map_.clear();
821 for (int i = 0; i < cp_model_.variables_size(); ++i) {
822 const IntegerVariableProto& var = cp_model_.variables(i);
823 if (var.domain_size() == 2 && var.domain(0) == var.domain(1)) {
824 constant_to_index_map_[var.domain(0)] = i;
825 }
826 }
827 // This one would be more complicated to rebuild. Let's just clear it.
828 bool_to_integer_index_map_.clear();
829}
830
832 CHECK_GE(index, 0);
833 CHECK_LT(index, cp_model_.variables_size());
834 const IntegerVariableProto& proto = cp_model_.variables(index);
835 CHECK_EQ(2, proto.domain_size())
836 << "CpModelBuilder::GetBoolVarFromProtoIndex: The domain of the variable "
837 "is not Boolean";
838 CHECK_GE(0, proto.domain(0))
839 << "CpModelBuilder::GetBoolVarFromProtoIndex: The domain of the variable "
840 "is not Boolean";
841 CHECK_LE(1, proto.domain(1))
842 << "CpModelBuilder::GetBoolVarFromProtoIndex: The domain of the variable "
843 "is not Boolean";
844 return BoolVar(index, &cp_model_);
845}
846
848 CHECK_GE(index, 0);
849 CHECK_LT(index, cp_model_.variables_size());
850 return IntVar(index, &cp_model_);
851}
852
854 CHECK_GE(index, 0);
855 CHECK_LT(index, cp_model_.constraints_size());
856 const ConstraintProto& ct = cp_model_.constraints(index);
857 CHECK_EQ(ct.constraint_case(), ConstraintProto::kInterval)
858 << "CpModelBuilder::GetIntervalVarFromProtoIndex: the referenced "
859 "object is not an interval variable";
860 return IntervalVar(index, &cp_model_);
861}
862
863int64 SolutionIntegerValue(const CpSolverResponse& r, const LinearExpr& expr) {
864 int64 result = expr.constant();
865 for (int i = 0; i < expr.variables().size(); ++i) {
866 result += r.solution(expr.variables()[i].index_) * expr.coefficients()[i];
867 }
868 return result;
869}
870
871int64 SolutionIntegerMin(const CpSolverResponse& r, IntVar x) {
872 if (r.solution_size() > 0) {
873 return r.solution(x.index_);
874 } else {
875 return r.solution_lower_bounds(x.index_);
876 }
877}
878
879int64 SolutionIntegerMax(const CpSolverResponse& r, IntVar x) {
880 if (r.solution_size() > 0) {
881 return r.solution(x.index_);
882 } else {
883 return r.solution_upper_bounds(x.index_);
884 }
885}
886
887bool SolutionBooleanValue(const CpSolverResponse& r, BoolVar x) {
888 const int ref = x.index_;
889 if (RefIsPositive(ref)) {
890 return r.solution(ref) == 1;
891 } else {
892 return r.solution(PositiveRef(ref)) == 0;
893 }
894}
895
896} // namespace sat
897} // namespace operations_research
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_LT(val1, val2)
Definition: base/logging.h:700
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
#define CHECK_LE(val1, val2)
Definition: base/logging.h:699
We call domain any subset of Int64 = [kint64min, kint64max].
Specialized automaton constraint.
Definition: cp_model.h:545
void AddTransition(int tail, int head, int64 transition_label)
Adds a transitions to the automaton.
Definition: cp_model.cc:263
A Boolean variable.
Definition: cp_model.h:67
BoolVar WithName(const std::string &name)
Sets the name of the variable.
Definition: cp_model.cc:31
std::string DebugString() const
Debug string.
Definition: cp_model.cc:36
BoolVar Not() const
Returns the logical negation of the current Boolean variable.
Definition: cp_model.h:78
Specialized circuit constraint.
Definition: cp_model.h:451
void AddArc(int tail, int head, BoolVar literal)
Add an arc to the circuit.
Definition: cp_model.cc:225
Constraint OnlyEnforceIf(absl::Span< const BoolVar > literals)
The constraint will be enforced iff all literals listed here are true.
Definition: cp_model.cc:213
Constraint WithName(const std::string &name)
Sets the name of the constraint.
Definition: cp_model.cc:206
const std::string & Name() const
Returns the name of the constraint (or the empty string if not set).
Definition: cp_model.cc:211
Constraint(ConstraintProto *proto)
Definition: cp_model.cc:204
Wrapper class around the cp_model proto.
Definition: cp_model.h:599
IntVar NewConstant(int64 value)
Creates a constant variable.
Definition: cp_model.cc:385
TableConstraint AddForbiddenAssignments(absl::Span< const IntVar > vars)
Adds an forbidden assignments constraint.
Definition: cp_model.cc:583
Constraint AddLinearConstraint(const LinearExpr &expr, const Domain &domain)
Adds expr in domain.
Definition: cp_model.cc:506
void ClearAssumptions()
Remove all assumptions from the model.
Definition: cp_model.cc:813
Constraint AddAbsEquality(IntVar target, IntVar var)
Adds target == abs(var).
Definition: cp_model.cc:692
void AddAssumptions(absl::Span< const BoolVar > literals)
Adds multiple literals to the model as assumptions.
Definition: cp_model.cc:807
ReservoirConstraint AddReservoirConstraint(int64 min_level, int64 max_level)
Adds a reservoir constraint with optional refill/emptying events.
Definition: cp_model.cc:607
MultipleCircuitConstraint AddMultipleCircuitConstraint()
Adds a multiple circuit constraint, aka the "VRP" (Vehicle Routing Problem) constraint.
Definition: cp_model.cc:570
Constraint AddMinEquality(IntVar target, absl::Span< const IntVar > vars)
Adds target == min(vars).
Definition: cp_model.cc:629
BoolVar TrueVar()
Creates an always true Boolean variable.
Definition: cp_model.cc:389
IntVar NewIntVar(const Domain &domain)
Creates an integer variable with the given domain.
Definition: cp_model.cc:367
Constraint AddMaxEquality(IntVar target, absl::Span< const IntVar > vars)
Adds target == max(vars).
Definition: cp_model.cc:661
Constraint AddDivisionEquality(IntVar target, IntVar numerator, IntVar denominator)
Adds target = num / denom (integer division rounded towards 0).
Definition: cp_model.cc:682
void ClearHints()
Remove all hints.
Definition: cp_model.cc:799
void Maximize(const LinearExpr &expr)
Adds a linear maximization objective.
Definition: cp_model.cc:751
IntervalVar NewOptionalIntervalVar(IntVar start, IntVar size, IntVar end, BoolVar presence)
Creates an optional interval variable.
Definition: cp_model.cc:402
BoolVar NewBoolVar()
Creates a Boolean variable.
Definition: cp_model.cc:377
void AddDecisionStrategy(absl::Span< const IntVar > variables, DecisionStrategyProto::VariableSelectionStrategy var_strategy, DecisionStrategyProto::DomainReductionStrategy domain_strategy)
Adds a decision strategy on a list of integer variables.
Definition: cp_model.cc:769
void ScaleObjectiveBy(double scaling)
Sets scaling of the objective.
Definition: cp_model.cc:763
CircuitConstraint AddCircuitConstraint()
Adds a circuit constraint.
Definition: cp_model.cc:566
Constraint AddVariableElement(IntVar index, absl::Span< const IntVar > variables, IntVar target)
Adds the element constraint: variables[index] == target.
Definition: cp_model.cc:543
CumulativeConstraint AddCumulative(IntVar capacity)
The cumulative constraint.
Definition: cp_model.cc:733
Constraint AddGreaterThan(const LinearExpr &left, const LinearExpr &right)
Adds left > right.
Definition: cp_model.cc:486
void CopyFrom(const CpModelProto &model_proto)
Replace the current model with the one from the given proto.
Definition: cp_model.cc:817
Constraint AddLessThan(const LinearExpr &left, const LinearExpr &right)
Adds left < right.
Definition: cp_model.cc:496
Constraint AddBoolXor(absl::Span< const BoolVar > literals)
Adds the constraint that a odd number of literal is true.
Definition: cp_model.cc:431
void AddAssumption(BoolVar lit)
Adds a literal to the model as assumptions.
Definition: cp_model.cc:803
void Minimize(const LinearExpr &expr)
Adds a linear minimization objective.
Definition: cp_model.cc:740
BoolVar FalseVar()
Creates an always false Boolean variable.
Definition: cp_model.cc:393
Constraint AddBoolAnd(absl::Span< const BoolVar > literals)
Adds the constraint that all literals must be true.
Definition: cp_model.cc:423
IntervalVar GetIntervalVarFromProtoIndex(int index)
Returns the interval variable from its index in the proto.
Definition: cp_model.cc:853
Constraint AddLessOrEqual(const LinearExpr &left, const LinearExpr &right)
Adds left <= right.
Definition: cp_model.cc:476
Constraint AddModuloEquality(IntVar target, IntVar var, IntVar mod)
Adds target = var % mod.
Definition: cp_model.cc:701
Constraint AddEquality(const LinearExpr &left, const LinearExpr &right)
Adds left == right.
Definition: cp_model.cc:456
NoOverlap2DConstraint AddNoOverlap2D()
The no_overlap_2d constraint prevents a set of boxes from overlapping.
Definition: cp_model.cc:729
Constraint AddElement(IntVar index, absl::Span< const int64 > values, IntVar target)
Adds the element constraint: values[index] == target.
Definition: cp_model.cc:554
Constraint AddGreaterOrEqual(const LinearExpr &left, const LinearExpr &right)
Adds left >= right.
Definition: cp_model.cc:466
Constraint AddBoolOr(absl::Span< const BoolVar > literals)
Adds the constraint that at least one of the literals must be true.
Definition: cp_model.cc:415
IntVar GetIntVarFromProtoIndex(int index)
Returns the integer variable from its index in the proto.
Definition: cp_model.cc:847
AutomatonConstraint AddAutomaton(absl::Span< const IntVar > transition_variables, int starting_state, absl::Span< const int > final_states)
An automaton constraint/.
Definition: cp_model.cc:615
void AddHint(IntVar var, int64 value)
Adds hinting to a variable.
Definition: cp_model.cc:793
Constraint AddLinMinEquality(const LinearExpr &target, absl::Span< const LinearExpr > exprs)
Adds target == min(exprs).
Definition: cp_model.cc:650
Constraint AddProductEquality(IntVar target, absl::Span< const IntVar > vars)
Adds target == prod(vars).
Definition: cp_model.cc:710
Constraint AddLinMaxEquality(const LinearExpr &target, absl::Span< const LinearExpr > exprs)
Adds target == max(exprs).
Definition: cp_model.cc:671
BoolVar GetBoolVarFromProtoIndex(int index)
Returns the Boolean variable from its index in the proto.
Definition: cp_model.cc:831
Constraint AddNotEqual(const LinearExpr &left, const LinearExpr &right)
Adds left != right.
Definition: cp_model.cc:523
Constraint AddAllDifferent(absl::Span< const IntVar > vars)
this constraint forces all variables to have different values.
Definition: cp_model.cc:535
TableConstraint AddAllowedAssignments(absl::Span< const IntVar > vars)
Adds an allowed assignments constraint.
Definition: cp_model.cc:574
Constraint AddInverseConstraint(absl::Span< const IntVar > variables, absl::Span< const IntVar > inverse_variables)
An inverse constraint.
Definition: cp_model.cc:593
IntervalVar NewIntervalVar(IntVar start, IntVar size, IntVar end)
Creates an interval variable.
Definition: cp_model.cc:397
Constraint AddNoOverlap(absl::Span< const IntervalVar > vars)
Adds a no-overlap constraint that ensures that all present intervals do not overlap in time.
Definition: cp_model.cc:720
Specialized cumulative constraint.
Definition: cp_model.h:579
void AddDemand(IntervalVar interval, IntVar demand)
Adds a pair (interval, demand) to the constraint.
Definition: cp_model.cc:280
An integer variable.
Definition: cp_model.h:146
BoolVar ToBoolVar() const
Cast IntVar -> BoolVar.
Definition: cp_model.cc:87
LinearExpr AddConstant(int64 value) const
Adds a constant value to an integer variable and returns a linear expression.
Definition: cp_model.cc:97
std::string DebugString() const
Returns a debug string.
Definition: cp_model.cc:101
IntVar WithName(const std::string &name)
Sets the name of the variable.
Definition: cp_model.cc:77
int index() const
Returns the index of the variable in the model.
Definition: cp_model.h:191
const IntegerVariableProto & Proto() const
Returns the underlying protobuf object (useful for testing).
Definition: cp_model.h:181
Represents a Interval variable.
Definition: cp_model.h:326
BoolVar PresenceBoolVar() const
Returns a BoolVar indicating the presence of this interval.
Definition: cp_model.cc:306
std::string Name() const
Returns the name of the interval (or the empty string if not set).
Definition: cp_model.cc:311
IntVar SizeVar() const
Returns the size variable.
Definition: cp_model.cc:300
const IntervalConstraintProto & Proto() const
Returns the underlying protobuf object (useful for testing).
Definition: cp_model.h:367
std::string DebugString() const
Returns a debug string.
Definition: cp_model.cc:315
IntervalVar WithName(const std::string &name)
Sets the name of the variable.
Definition: cp_model.cc:291
IntVar EndVar() const
Returns the end variable.
Definition: cp_model.cc:304
IntVar StartVar() const
Returns the start variable.
Definition: cp_model.cc:296
A dedicated container for linear expressions.
Definition: cp_model.h:248
static LinearExpr Term(IntVar var, int64 coefficient)
Construncts var * coefficient.
Definition: cp_model.cc:161
static LinearExpr ScalProd(absl::Span< const IntVar > vars, absl::Span< const int64 > coeffs)
Constructs the scalar product of variables and coefficients.
Definition: cp_model.cc:151
LinearExpr & AddConstant(int64 value)
Adds a constant value to the linear expression.
Definition: cp_model.cc:185
static LinearExpr BooleanScalProd(absl::Span< const BoolVar > vars, absl::Span< const int64 > coeffs)
Constructs the scalar product of Booleans and coefficients.
Definition: cp_model.cc:175
static LinearExpr Sum(absl::Span< const IntVar > vars)
Constructs the sum of a list of variables.
Definition: cp_model.cc:143
static LinearExpr BooleanSum(absl::Span< const BoolVar > vars)
Constructs the sum of a list of Booleans.
Definition: cp_model.cc:167
void AddTerm(IntVar var, int64 coeff)
Adds a term (var * coeff) to the linear expression.
Definition: cp_model.cc:192
void AddVar(IntVar var)
Adds a single integer variable to the linear expression.
Definition: cp_model.cc:190
const std::vector< IntVar > & variables() const
Returns the vector of variables.
Definition: cp_model.h:291
int64 constant() const
Returns the constant term.
Definition: cp_model.h:297
const std::vector< int64 > & coefficients() const
Returns the vector of coefficients.
Definition: cp_model.h:294
void AddArc(int tail, int head, BoolVar literal)
Add an arc to the circuit.
Definition: cp_model.cc:231
Specialized no_overlap2D constraint.
Definition: cp_model.h:562
void AddRectangle(IntervalVar x_coordinate, IntervalVar y_coordinate)
Adds a rectangle (parallel to the axis) to the constraint.
Definition: cp_model.cc:270
Specialized reservoir constraint.
Definition: cp_model.h:514
void AddEvent(IntVar time, int64 demand)
Adds a mandatory event.
Definition: cp_model.cc:248
void AddOptionalEvent(IntVar time, int64 demand, BoolVar is_active)
Adds a optional event.
Definition: cp_model.cc:255
Specialized assignment constraint.
Definition: cp_model.h:497
void AddTuple(absl::Span< const int64 > tuple)
Adds a tuple of possible values to the constraint.
Definition: cp_model.cc:237
This file implements a wrapper around the CP-SAT model proto.
CpModelProto proto
CpModelProto const * model_proto
const std::string name
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
static const int64 kint64max
int64_t int64
static const int64 kint64min
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
Definition: cp_model.cc:65
int64 SolutionIntegerValue(const CpSolverResponse &r, const LinearExpr &expr)
Evaluates the value of an linear expression in a solver response.
Definition: cp_model.cc:863
int64 SolutionIntegerMax(const CpSolverResponse &r, IntVar x)
Returns the max of an integer variable in a solution.
Definition: cp_model.cc:879
BoolVar Not(BoolVar x)
A convenient wrapper so we can write Not(x) instead of x.Not() which is sometimes clearer.
Definition: cp_model.cc:63
bool SolutionBooleanValue(const CpSolverResponse &r, BoolVar x)
Evaluates the value of a Boolean literal in a solver response.
Definition: cp_model.cc:887
int64 SolutionIntegerMin(const CpSolverResponse &r, IntVar x)
Returns the min of an integer variable in a solution.
Definition: cp_model.cc:871
bool RefIsPositive(int ref)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
int64 time
Definition: resource.cc:1683
int64 demand
Definition: resource.cc:123
IntervalVar * interval
Definition: resource.cc:98
int64 tail
int64 head
int64 capacity
int64 coefficient