OR-Tools  8.2
cp_model_checker.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 <algorithm>
17#include <memory>
18#include <utility>
19
20#include "absl/container/flat_hash_map.h"
21#include "absl/container/flat_hash_set.h"
22#include "absl/strings/str_cat.h"
23#include "ortools/base/hash.h"
27#include "ortools/sat/cp_model.pb.h"
31
32namespace operations_research {
33namespace sat {
34namespace {
35
36// =============================================================================
37// CpModelProto validation.
38// =============================================================================
39
40// If the string returned by "statement" is not empty, returns it.
41#define RETURN_IF_NOT_EMPTY(statement) \
42 do { \
43 const std::string error_message = statement; \
44 if (!error_message.empty()) return error_message; \
45 } while (false)
46
47template <typename ProtoWithDomain>
48bool DomainInProtoIsValid(const ProtoWithDomain& proto) {
49 if (proto.domain().size() % 2) return false;
50 std::vector<ClosedInterval> domain;
51 for (int i = 0; i < proto.domain_size(); i += 2) {
52 if (proto.domain(i) > proto.domain(i + 1)) return false;
53 domain.push_back({proto.domain(i), proto.domain(i + 1)});
54 }
56}
57
58bool VariableReferenceIsValid(const CpModelProto& model, int reference) {
59 // We do it this way to avoid overflow if reference is kint64min for instance.
60 if (reference >= model.variables_size()) return false;
61 return reference >= -static_cast<int>(model.variables_size());
62}
63
64bool LiteralReferenceIsValid(const CpModelProto& model, int reference) {
65 if (!VariableReferenceIsValid(model, reference)) return false;
66 const auto& var_proto = model.variables(PositiveRef(reference));
67 const int64 min_domain = var_proto.domain(0);
68 const int64 max_domain = var_proto.domain(var_proto.domain_size() - 1);
69 return min_domain >= 0 && max_domain <= 1;
70}
71
72std::string ValidateIntegerVariable(const CpModelProto& model, int v) {
73 const IntegerVariableProto& proto = model.variables(v);
74 if (proto.domain_size() == 0) {
75 return absl::StrCat("var #", v,
76 " has no domain(): ", ProtobufShortDebugString(proto));
77 }
78 if (proto.domain_size() % 2 != 0) {
79 return absl::StrCat("var #", v, " has an odd domain() size: ",
81 }
82 if (!DomainInProtoIsValid(proto)) {
83 return absl::StrCat("var #", v, " has and invalid domain() format: ",
85 }
86
87 // Internally, we often take the negation of a domain, and we also want to
88 // have sentinel values greater than the min/max of a variable domain, so
89 // the domain must fall in [kint64min + 2, kint64max - 1].
90 const int64 lb = proto.domain(0);
91 const int64 ub = proto.domain(proto.domain_size() - 1);
92 if (lb < kint64min + 2 || ub > kint64max - 1) {
93 return absl::StrCat(
94 "var #", v, " domain do not fall in [kint64min + 2, kint64max - 1]. ",
96 }
97
98 // We do compute ub - lb in some place in the code and do not want to deal
99 // with overflow everywhere. This seems like a reasonable precondition anyway.
100 if (lb < 0 && lb + kint64max < ub) {
101 return absl::StrCat(
102 "var #", v,
103 " has a domain that is too large, i.e. |UB - LB| overflow an int64: ",
105 }
106
107 return "";
108}
109
110std::string ValidateArgumentReferencesInConstraint(const CpModelProto& model,
111 int c) {
112 const ConstraintProto& ct = model.constraints(c);
113 IndexReferences references = GetReferencesUsedByConstraint(ct);
114 for (const int v : references.variables) {
115 if (!VariableReferenceIsValid(model, v)) {
116 return absl::StrCat("Out of bound integer variable ", v,
117 " in constraint #", c, " : ",
119 }
120 }
121 for (const int lit : ct.enforcement_literal()) {
122 if (!LiteralReferenceIsValid(model, lit)) {
123 return absl::StrCat("Invalid enforcement literal ", lit,
124 " in constraint #", c, " : ",
126 }
127 }
128 for (const int lit : references.literals) {
129 if (!LiteralReferenceIsValid(model, lit)) {
130 return absl::StrCat("Invalid literal ", lit, " in constraint #", c, " : ",
132 }
133 }
134 for (const int i : UsedIntervals(ct)) {
135 if (i < 0 || i >= model.constraints_size()) {
136 return absl::StrCat("Out of bound interval ", i, " in constraint #", c,
138 }
139 if (model.constraints(i).constraint_case() !=
140 ConstraintProto::ConstraintCase::kInterval) {
141 return absl::StrCat(
142 "Interval ", i,
143 " does not refer to an interval constraint. Problematic constraint #",
144 c, " : ", ProtobufShortDebugString(ct));
145 }
146 }
147 return "";
148}
149
150template <class LinearExpressionProto>
151bool PossibleIntegerOverflow(const CpModelProto& model,
152 const LinearExpressionProto& proto) {
153 int64 sum_min = 0;
154 int64 sum_max = 0;
155 for (int i = 0; i < proto.vars_size(); ++i) {
156 const int ref = proto.vars(i);
157 const auto& var_proto = model.variables(PositiveRef(ref));
158 const int64 min_domain = var_proto.domain(0);
159 const int64 max_domain = var_proto.domain(var_proto.domain_size() - 1);
160 if (proto.coeffs(i) == kint64min) return true;
161 const int64 coeff = RefIsPositive(ref) ? proto.coeffs(i) : -proto.coeffs(i);
162 const int64 prod1 = CapProd(min_domain, coeff);
163 const int64 prod2 = CapProd(max_domain, coeff);
164
165 // Note that we use min/max with zero to disallow "alternative" terms and
166 // be sure that we cannot have an overflow if we do the computation in a
167 // different order.
168 sum_min = CapAdd(sum_min, std::min(int64{0}, std::min(prod1, prod2)));
169 sum_max = CapAdd(sum_max, std::max(int64{0}, std::max(prod1, prod2)));
170 for (const int64 v : {prod1, prod2, sum_min, sum_max}) {
171 if (v == kint64max || v == kint64min) return true;
172 }
173 }
174
175 // In addition to computing the min/max possible sum, we also often compare
176 // it with the constraint bounds, so we do not want max - min to overflow.
177 if (sum_min < 0 && sum_min + kint64max < sum_max) {
178 return true;
179 }
180 return false;
181}
182
183std::string ValidateLinearExpression(const CpModelProto& model,
184 const LinearExpressionProto& expr) {
185 if (expr.coeffs_size() != expr.vars_size()) {
186 return absl::StrCat("coeffs_size() != vars_size() in linear expression: ",
188 }
189 if (PossibleIntegerOverflow(model, expr)) {
190 return absl::StrCat("Possible overflow in linear expression: ",
192 }
193 return "";
194}
195
196std::string ValidateIntervalConstraint(const CpModelProto& model,
197 const ConstraintProto& ct) {
198 const IntervalConstraintProto& arg = ct.interval();
199 int num_view = 0;
200 if (arg.has_start_view()) {
201 ++num_view;
202 RETURN_IF_NOT_EMPTY(ValidateLinearExpression(model, arg.start_view()));
203 }
204 if (arg.has_size_view()) {
205 ++num_view;
206 RETURN_IF_NOT_EMPTY(ValidateLinearExpression(model, arg.size_view()));
207 }
208 if (arg.has_end_view()) {
209 ++num_view;
210 RETURN_IF_NOT_EMPTY(ValidateLinearExpression(model, arg.end_view()));
211 }
212 if (num_view != 0 && num_view != 3) {
213 return absl::StrCat(
214 "Interval must use either the var or the view representation, but not "
215 "both: ",
217 }
218 if (num_view > 0) return "";
219 if (arg.size() < 0) {
220 const IntegerVariableProto& size_var_proto =
221 model.variables(NegatedRef(arg.size()));
222 if (size_var_proto.domain(size_var_proto.domain_size() - 1) > 0) {
223 return absl::StrCat(
224 "Negative value in interval size domain: ", ProtobufDebugString(ct),
225 "negation of size var: ", ProtobufDebugString(size_var_proto));
226 }
227 } else {
228 const IntegerVariableProto& size_var_proto = model.variables(arg.size());
229 if (size_var_proto.domain(0) < 0) {
230 return absl::StrCat(
231 "Negative value in interval size domain: ", ProtobufDebugString(ct),
232 "size var: ", ProtobufDebugString(size_var_proto));
233 }
234 }
235 return "";
236}
237
238std::string ValidateLinearConstraint(const CpModelProto& model,
239 const ConstraintProto& ct) {
240 const LinearConstraintProto& arg = ct.linear();
241 if (PossibleIntegerOverflow(model, arg)) {
242 return "Possible integer overflow in constraint: " +
244 }
245 return "";
246}
247
248std::string ValidateTableConstraint(const CpModelProto& model,
249 const ConstraintProto& ct) {
250 const TableConstraintProto& arg = ct.table();
251 if (arg.vars().empty()) return "";
252 if (arg.values().size() % arg.vars().size() != 0) {
253 return absl::StrCat(
254 "The flat encoding of a table constraint must be a multiple of the "
255 "number of variable: ",
257 }
258 return "";
259}
260
261std::string ValidateCircuitConstraint(const CpModelProto& model,
262 const ConstraintProto& ct) {
263 const int size = ct.circuit().tails().size();
264 if (ct.circuit().heads().size() != size ||
265 ct.circuit().literals().size() != size) {
266 return absl::StrCat("Wrong field sizes in circuit: ",
268 }
269 return "";
270}
271
272std::string ValidateRoutesConstraint(const CpModelProto& model,
273 const ConstraintProto& ct) {
274 const int size = ct.routes().tails().size();
275 if (ct.routes().heads().size() != size ||
276 ct.routes().literals().size() != size) {
277 return absl::StrCat("Wrong field sizes in routes: ",
279 }
280 return "";
281}
282
283std::string ValidateNoOverlap2DConstraint(const CpModelProto& model,
284 const ConstraintProto& ct) {
285 const int size_x = ct.no_overlap_2d().x_intervals().size();
286 const int size_y = ct.no_overlap_2d().y_intervals().size();
287 if (size_x != size_y) {
288 return absl::StrCat("The two lists of intervals must have the same size: ",
290 }
291 return "";
292}
293
294std::string ValidateAutomatonConstraint(const CpModelProto& model,
295 const ConstraintProto& ct) {
296 const int num_transistions = ct.automaton().transition_tail().size();
297 if (num_transistions != ct.automaton().transition_head().size() ||
298 num_transistions != ct.automaton().transition_label().size()) {
299 return absl::StrCat(
300 "The transitions repeated fields must have the same size: ",
302 }
303 return "";
304}
305
306std::string ValidateReservoirConstraint(const CpModelProto& model,
307 const ConstraintProto& ct) {
308 if (ct.enforcement_literal_size() > 0) {
309 return "Reservoir does not support enforcement literals.";
310 }
311 if (ct.reservoir().times().size() != ct.reservoir().demands().size()) {
312 return absl::StrCat("Times and demands fields must be of the same size: ",
314 }
315 if (ct.reservoir().min_level() > 0) {
316 return absl::StrCat(
317 "The min level of a reservoir must be <= 0. Please use fixed events to "
318 "setup initial state: ",
320 }
321 if (ct.reservoir().max_level() < 0) {
322 return absl::StrCat(
323 "The max level of a reservoir must be >= 0. Please use fixed events to "
324 "setup initial state: ",
326 }
327
328 int64 sum_abs = 0;
329 for (const int64 demand : ct.reservoir().demands()) {
330 sum_abs = CapAdd(sum_abs, std::abs(demand));
331 if (sum_abs == kint64max) {
332 return "Possible integer overflow in constraint: " +
334 }
335 }
336 if (ct.reservoir().actives_size() > 0 &&
337 ct.reservoir().actives_size() != ct.reservoir().times_size()) {
338 return "Wrong array length of actives variables";
339 }
340 if (ct.reservoir().demands_size() > 0 &&
341 ct.reservoir().demands_size() != ct.reservoir().times_size()) {
342 return "Wrong array length of demands variables";
343 }
344 return "";
345}
346
347std::string ValidateIntModConstraint(const CpModelProto& model,
348 const ConstraintProto& ct) {
349 if (ct.int_mod().vars().size() != 2) {
350 return absl::StrCat("An int_mod constraint should have exactly 2 terms: ",
352 }
353 const int mod_var = ct.int_mod().vars(1);
354 const IntegerVariableProto& mod_proto = model.variables(PositiveRef(mod_var));
355 if ((RefIsPositive(mod_var) && mod_proto.domain(0) <= 0) ||
356 (!RefIsPositive(mod_var) && mod_proto.domain(0) >= 0)) {
357 return absl::StrCat(
358 "An int_mod must have a strictly positive modulo argument: ",
360 }
361 return "";
362}
363
364std::string ValidateIntDivConstraint(const CpModelProto& model,
365 const ConstraintProto& ct) {
366 if (ct.int_div().vars().size() != 2) {
367 return absl::StrCat("An int_div constraint should have exactly 2 terms: ",
369 }
370 return "";
371}
372
373std::string ValidateObjective(const CpModelProto& model,
374 const CpObjectiveProto& obj) {
375 if (!DomainInProtoIsValid(obj)) {
376 return absl::StrCat("The objective has and invalid domain() format: ",
378 }
379 if (obj.vars().size() != obj.coeffs().size()) {
380 return absl::StrCat("vars and coeffs size do not match in objective: ",
382 }
383 for (const int v : obj.vars()) {
384 if (!VariableReferenceIsValid(model, v)) {
385 return absl::StrCat("Out of bound integer variable ", v,
386 " in objective: ", ProtobufShortDebugString(obj));
387 }
388 }
389 if (PossibleIntegerOverflow(model, obj)) {
390 return "Possible integer overflow in objective: " +
392 }
393 return "";
394}
395
396std::string ValidateSearchStrategies(const CpModelProto& model) {
397 for (const DecisionStrategyProto& strategy : model.search_strategy()) {
398 const int vss = strategy.variable_selection_strategy();
399 if (vss != DecisionStrategyProto::CHOOSE_FIRST &&
400 vss != DecisionStrategyProto::CHOOSE_LOWEST_MIN &&
401 vss != DecisionStrategyProto::CHOOSE_HIGHEST_MAX &&
402 vss != DecisionStrategyProto::CHOOSE_MIN_DOMAIN_SIZE &&
403 vss != DecisionStrategyProto::CHOOSE_MAX_DOMAIN_SIZE) {
404 return absl::StrCat(
405 "Unknown or unsupported variable_selection_strategy: ", vss);
406 }
407 const int drs = strategy.domain_reduction_strategy();
408 if (drs != DecisionStrategyProto::SELECT_MIN_VALUE &&
409 drs != DecisionStrategyProto::SELECT_MAX_VALUE &&
410 drs != DecisionStrategyProto::SELECT_LOWER_HALF &&
411 drs != DecisionStrategyProto::SELECT_UPPER_HALF &&
412 drs != DecisionStrategyProto::SELECT_MEDIAN_VALUE) {
413 return absl::StrCat("Unknown or unsupported domain_reduction_strategy: ",
414 drs);
415 }
416 for (const int ref : strategy.variables()) {
417 if (!VariableReferenceIsValid(model, ref)) {
418 return absl::StrCat("Invalid variable reference in strategy: ",
419 ProtobufShortDebugString(strategy));
420 }
421 }
422 for (const auto& transformation : strategy.transformations()) {
423 if (transformation.positive_coeff() <= 0) {
424 return absl::StrCat("Affine transformation coeff should be positive: ",
425 ProtobufShortDebugString(transformation));
426 }
427 if (!VariableReferenceIsValid(model, transformation.var())) {
428 return absl::StrCat(
429 "Invalid variable reference in affine transformation: ",
430 ProtobufShortDebugString(transformation));
431 }
432 }
433 }
434 return "";
435}
436
437std::string ValidateSolutionHint(const CpModelProto& model) {
438 if (!model.has_solution_hint()) return "";
439 const auto& hint = model.solution_hint();
440 if (hint.vars().size() != hint.values().size()) {
441 return "Invalid solution hint: vars and values do not have the same size.";
442 }
443 for (const int ref : hint.vars()) {
444 if (!VariableReferenceIsValid(model, ref)) {
445 return absl::StrCat("Invalid variable reference in solution hint: ", ref);
446 }
447 }
448 return "";
449}
450
451} // namespace
452
453std::string ValidateCpModel(const CpModelProto& model) {
454 for (int v = 0; v < model.variables_size(); ++v) {
455 RETURN_IF_NOT_EMPTY(ValidateIntegerVariable(model, v));
456 }
457 for (int c = 0; c < model.constraints_size(); ++c) {
458 RETURN_IF_NOT_EMPTY(ValidateArgumentReferencesInConstraint(model, c));
459
460 // By default, a constraint does not support enforcement literals except if
461 // explicitly stated by setting this to true below.
462 bool support_enforcement = false;
463
464 // Other non-generic validations.
465 // TODO(user): validate all constraints.
466 const ConstraintProto& ct = model.constraints(c);
467 const ConstraintProto::ConstraintCase type = ct.constraint_case();
468 switch (type) {
469 case ConstraintProto::ConstraintCase::kIntDiv:
470 RETURN_IF_NOT_EMPTY(ValidateIntDivConstraint(model, ct));
471 break;
472 case ConstraintProto::ConstraintCase::kIntMod:
473 RETURN_IF_NOT_EMPTY(ValidateIntModConstraint(model, ct));
474 break;
475 case ConstraintProto::ConstraintCase::kTable:
476 RETURN_IF_NOT_EMPTY(ValidateTableConstraint(model, ct));
477 break;
478 case ConstraintProto::ConstraintCase::kBoolOr:
479 support_enforcement = true;
480 break;
481 case ConstraintProto::ConstraintCase::kBoolAnd:
482 support_enforcement = true;
483 break;
484 case ConstraintProto::ConstraintCase::kLinear:
485 support_enforcement = true;
486 if (!DomainInProtoIsValid(ct.linear())) {
487 return absl::StrCat("Invalid domain in constraint #", c, " : ",
489 }
490 if (ct.linear().coeffs_size() != ct.linear().vars_size()) {
491 return absl::StrCat("coeffs_size() != vars_size() in constraint #", c,
493 }
494 RETURN_IF_NOT_EMPTY(ValidateLinearConstraint(model, ct));
495 break;
496 case ConstraintProto::ConstraintCase::kLinMax: {
497 const std::string target_error =
498 ValidateLinearExpression(model, ct.lin_max().target());
499 if (!target_error.empty()) return target_error;
500 for (int i = 0; i < ct.lin_max().exprs_size(); ++i) {
501 const std::string expr_error =
502 ValidateLinearExpression(model, ct.lin_max().exprs(i));
503 if (!expr_error.empty()) return expr_error;
504 }
505 break;
506 }
507 case ConstraintProto::ConstraintCase::kLinMin: {
508 const std::string target_error =
509 ValidateLinearExpression(model, ct.lin_min().target());
510 if (!target_error.empty()) return target_error;
511 for (int i = 0; i < ct.lin_min().exprs_size(); ++i) {
512 const std::string expr_error =
513 ValidateLinearExpression(model, ct.lin_min().exprs(i));
514 if (!expr_error.empty()) return expr_error;
515 }
516 break;
517 }
518 case ConstraintProto::ConstraintCase::kInterval:
519 support_enforcement = true;
520 RETURN_IF_NOT_EMPTY(ValidateIntervalConstraint(model, ct));
521 break;
522 case ConstraintProto::ConstraintCase::kCumulative:
523 if (ct.cumulative().intervals_size() !=
524 ct.cumulative().demands_size()) {
525 return absl::StrCat(
526 "intervals_size() != demands_size() in constraint #", c, " : ",
528 }
529 break;
530 case ConstraintProto::ConstraintCase::kInverse:
531 if (ct.inverse().f_direct().size() != ct.inverse().f_inverse().size()) {
532 return absl::StrCat("Non-matching fields size in inverse: ",
534 }
535 break;
536 case ConstraintProto::ConstraintCase::kAutomaton:
537 RETURN_IF_NOT_EMPTY(ValidateAutomatonConstraint(model, ct));
538 break;
539 case ConstraintProto::ConstraintCase::kCircuit:
540 RETURN_IF_NOT_EMPTY(ValidateCircuitConstraint(model, ct));
541 break;
542 case ConstraintProto::ConstraintCase::kRoutes:
543 RETURN_IF_NOT_EMPTY(ValidateRoutesConstraint(model, ct));
544 break;
545 case ConstraintProto::ConstraintCase::kNoOverlap2D:
546 RETURN_IF_NOT_EMPTY(ValidateNoOverlap2DConstraint(model, ct));
547 break;
548 case ConstraintProto::ConstraintCase::kReservoir:
549 RETURN_IF_NOT_EMPTY(ValidateReservoirConstraint(model, ct));
550 break;
551 default:
552 break;
553 }
554
555 // Because some client set fixed enforcement literal which are supported
556 // in the presolve for all constraints, we just check that there is no
557 // non-fixed enforcement.
558 if (!support_enforcement && !ct.enforcement_literal().empty()) {
559 for (const int ref : ct.enforcement_literal()) {
560 const int var = PositiveRef(ref);
561 const Domain domain = ReadDomainFromProto(model.variables(var));
562 if (domain.Size() != 1) {
563 return absl::StrCat(
564 "Enforcement literal not supported in constraint: ",
566 }
567 }
568 }
569 }
570 if (model.has_objective()) {
571 RETURN_IF_NOT_EMPTY(ValidateObjective(model, model.objective()));
572 }
573 RETURN_IF_NOT_EMPTY(ValidateSearchStrategies(model));
574 RETURN_IF_NOT_EMPTY(ValidateSolutionHint(model));
575 for (const int ref : model.assumptions()) {
576 if (!LiteralReferenceIsValid(model, ref)) {
577 return absl::StrCat("Invalid literal reference ", ref,
578 " in the 'assumptions' field.");
579 }
580 }
581 return "";
582}
583
584#undef RETURN_IF_NOT_EMPTY
585
586// =============================================================================
587// Solution Feasibility.
588// =============================================================================
589
590namespace {
591
592class ConstraintChecker {
593 public:
594 explicit ConstraintChecker(const std::vector<int64>& variable_values)
595 : variable_values_(variable_values) {}
596
597 bool LiteralIsTrue(int l) const {
598 if (l >= 0) return variable_values_[l] != 0;
599 return variable_values_[-l - 1] == 0;
600 }
601
602 bool LiteralIsFalse(int l) const { return !LiteralIsTrue(l); }
603
604 int64 Value(int var) const {
605 if (var >= 0) return variable_values_[var];
606 return -variable_values_[-var - 1];
607 }
608
609 bool ConstraintIsEnforced(const ConstraintProto& ct) {
610 for (const int lit : ct.enforcement_literal()) {
611 if (LiteralIsFalse(lit)) return false;
612 }
613 return true;
614 }
615
616 bool BoolOrConstraintIsFeasible(const ConstraintProto& ct) {
617 for (const int lit : ct.bool_or().literals()) {
618 if (LiteralIsTrue(lit)) return true;
619 }
620 return false;
621 }
622
623 bool BoolAndConstraintIsFeasible(const ConstraintProto& ct) {
624 for (const int lit : ct.bool_and().literals()) {
625 if (LiteralIsFalse(lit)) return false;
626 }
627 return true;
628 }
629
630 bool AtMostOneConstraintIsFeasible(const ConstraintProto& ct) {
631 int num_true_literals = 0;
632 for (const int lit : ct.at_most_one().literals()) {
633 if (LiteralIsTrue(lit)) ++num_true_literals;
634 }
635 return num_true_literals <= 1;
636 }
637
638 bool ExactlyOneConstraintIsFeasible(const ConstraintProto& ct) {
639 int num_true_literals = 0;
640 for (const int lit : ct.exactly_one().literals()) {
641 if (LiteralIsTrue(lit)) ++num_true_literals;
642 }
643 return num_true_literals == 1;
644 }
645
646 bool BoolXorConstraintIsFeasible(const ConstraintProto& ct) {
647 int sum = 0;
648 for (const int lit : ct.bool_xor().literals()) {
649 sum ^= LiteralIsTrue(lit) ? 1 : 0;
650 }
651 return sum == 1;
652 }
653
654 bool LinearConstraintIsFeasible(const ConstraintProto& ct) {
655 int64 sum = 0;
656 const int num_variables = ct.linear().coeffs_size();
657 for (int i = 0; i < num_variables; ++i) {
658 sum += Value(ct.linear().vars(i)) * ct.linear().coeffs(i);
659 }
660 return DomainInProtoContains(ct.linear(), sum);
661 }
662
663 bool IntMaxConstraintIsFeasible(const ConstraintProto& ct) {
664 const int64 max = Value(ct.int_max().target());
665 int64 actual_max = kint64min;
666 for (int i = 0; i < ct.int_max().vars_size(); ++i) {
667 actual_max = std::max(actual_max, Value(ct.int_max().vars(i)));
668 }
669 return max == actual_max;
670 }
671
672 int64 LinearExpressionValue(const LinearExpressionProto& expr) const {
673 int64 sum = expr.offset();
674 const int num_variables = expr.vars_size();
675 for (int i = 0; i < num_variables; ++i) {
676 sum += Value(expr.vars(i)) * expr.coeffs(i);
677 }
678 return sum;
679 }
680
681 bool LinMaxConstraintIsFeasible(const ConstraintProto& ct) {
682 const int64 max = LinearExpressionValue(ct.lin_max().target());
683 int64 actual_max = kint64min;
684 for (int i = 0; i < ct.lin_max().exprs_size(); ++i) {
685 const int64 expr_value = LinearExpressionValue(ct.lin_max().exprs(i));
686 actual_max = std::max(actual_max, expr_value);
687 }
688 return max == actual_max;
689 }
690
691 bool IntProdConstraintIsFeasible(const ConstraintProto& ct) {
692 const int64 prod = Value(ct.int_prod().target());
693 int64 actual_prod = 1;
694 for (int i = 0; i < ct.int_prod().vars_size(); ++i) {
695 actual_prod *= Value(ct.int_prod().vars(i));
696 }
697 return prod == actual_prod;
698 }
699
700 bool IntDivConstraintIsFeasible(const ConstraintProto& ct) {
701 return Value(ct.int_div().target()) ==
702 Value(ct.int_div().vars(0)) / Value(ct.int_div().vars(1));
703 }
704
705 bool IntModConstraintIsFeasible(const ConstraintProto& ct) {
706 return Value(ct.int_mod().target()) ==
707 Value(ct.int_mod().vars(0)) % Value(ct.int_mod().vars(1));
708 }
709
710 bool IntMinConstraintIsFeasible(const ConstraintProto& ct) {
711 const int64 min = Value(ct.int_min().target());
712 int64 actual_min = kint64max;
713 for (int i = 0; i < ct.int_min().vars_size(); ++i) {
714 actual_min = std::min(actual_min, Value(ct.int_min().vars(i)));
715 }
716 return min == actual_min;
717 }
718
719 bool LinMinConstraintIsFeasible(const ConstraintProto& ct) {
720 const int64 min = LinearExpressionValue(ct.lin_min().target());
721 int64 actual_min = kint64max;
722 for (int i = 0; i < ct.lin_min().exprs_size(); ++i) {
723 const int64 expr_value = LinearExpressionValue(ct.lin_min().exprs(i));
724 actual_min = std::min(actual_min, expr_value);
725 }
726 return min == actual_min;
727 }
728
729 bool AllDiffConstraintIsFeasible(const ConstraintProto& ct) {
730 absl::flat_hash_set<int64> values;
731 for (const int v : ct.all_diff().vars()) {
732 if (gtl::ContainsKey(values, Value(v))) return false;
733 values.insert(Value(v));
734 }
735 return true;
736 }
737
738 int64 IntervalStart(const IntervalConstraintProto& interval) const {
739 return interval.has_start_view()
740 ? LinearExpressionValue(interval.start_view())
741 : Value(interval.start());
742 }
743
744 int64 IntervalSize(const IntervalConstraintProto& interval) const {
745 return interval.has_size_view()
746 ? LinearExpressionValue(interval.size_view())
747 : Value(interval.size());
748 }
749
750 int64 IntervalEnd(const IntervalConstraintProto& interval) const {
751 return interval.has_end_view() ? LinearExpressionValue(interval.end_view())
752 : Value(interval.end());
753 }
754
755 bool IntervalConstraintIsFeasible(const ConstraintProto& ct) {
756 const int64 size = IntervalSize(ct.interval());
757 if (size < 0) return false;
758 return IntervalStart(ct.interval()) + size == IntervalEnd(ct.interval());
759 }
760
761 bool NoOverlapConstraintIsFeasible(const CpModelProto& model,
762 const ConstraintProto& ct) {
763 std::vector<std::pair<int64, int64>> start_durations_pairs;
764 for (const int i : ct.no_overlap().intervals()) {
765 const ConstraintProto& interval_constraint = model.constraints(i);
766 if (ConstraintIsEnforced(interval_constraint)) {
767 const IntervalConstraintProto& interval =
768 interval_constraint.interval();
769 start_durations_pairs.push_back(
770 {IntervalStart(interval), IntervalSize(interval)});
771 }
772 }
773 std::sort(start_durations_pairs.begin(), start_durations_pairs.end());
774 int64 previous_end = kint64min;
775 for (const auto pair : start_durations_pairs) {
776 if (pair.first < previous_end) return false;
777 previous_end = pair.first + pair.second;
778 }
779 return true;
780 }
781
782 bool IntervalsAreDisjoint(const IntervalConstraintProto& interval1,
783 const IntervalConstraintProto& interval2) {
784 return IntervalEnd(interval1) <= IntervalStart(interval2) ||
785 IntervalEnd(interval2) <= IntervalStart(interval1);
786 }
787
788 bool IntervalIsEmpty(const IntervalConstraintProto& interval) {
789 return IntervalStart(interval) == IntervalEnd(interval);
790 }
791
792 bool NoOverlap2DConstraintIsFeasible(const CpModelProto& model,
793 const ConstraintProto& ct) {
794 const auto& arg = ct.no_overlap_2d();
795 // Those intervals from arg.x_intervals and arg.y_intervals where both
796 // the x and y intervals are enforced.
797 std::vector<std::pair<const IntervalConstraintProto* const,
798 const IntervalConstraintProto* const>>
799 enforced_intervals_xy;
800 {
801 const int num_intervals = arg.x_intervals_size();
802 CHECK_EQ(arg.y_intervals_size(), num_intervals);
803 for (int i = 0; i < num_intervals; ++i) {
804 const ConstraintProto& x = model.constraints(arg.x_intervals(i));
805 const ConstraintProto& y = model.constraints(arg.y_intervals(i));
806 if (ConstraintIsEnforced(x) && ConstraintIsEnforced(y) &&
807 (!arg.boxes_with_null_area_can_overlap() ||
808 (!IntervalIsEmpty(x.interval()) &&
809 !IntervalIsEmpty(y.interval())))) {
810 enforced_intervals_xy.push_back({&x.interval(), &y.interval()});
811 }
812 }
813 }
814 const int num_enforced_intervals = enforced_intervals_xy.size();
815 for (int i = 0; i < num_enforced_intervals; ++i) {
816 for (int j = i + 1; j < num_enforced_intervals; ++j) {
817 const auto& xi = *enforced_intervals_xy[i].first;
818 const auto& yi = *enforced_intervals_xy[i].second;
819 const auto& xj = *enforced_intervals_xy[j].first;
820 const auto& yj = *enforced_intervals_xy[j].second;
821 if (!IntervalsAreDisjoint(xi, xj) && !IntervalsAreDisjoint(yi, yj) &&
822 !IntervalIsEmpty(xi) && !IntervalIsEmpty(xj) &&
823 !IntervalIsEmpty(yi) && !IntervalIsEmpty(yj)) {
824 VLOG(1) << "Interval " << i << "(x=[" << IntervalStart(xi) << ", "
825 << IntervalEnd(xi) << "], y=[" << IntervalStart(yi) << ", "
826 << IntervalEnd(yi) << "]) and " << j << "("
827 << "(x=[" << IntervalStart(xj) << ", " << IntervalEnd(xj)
828 << "], y=[" << IntervalStart(yj) << ", " << IntervalEnd(yj)
829 << "]) are not disjoint.";
830 return false;
831 }
832 }
833 }
834 return true;
835 }
836
837 bool CumulativeConstraintIsFeasible(const CpModelProto& model,
838 const ConstraintProto& ct) {
839 // TODO(user,user): Improve complexity for large durations.
840 const int64 capacity = Value(ct.cumulative().capacity());
841 const int num_intervals = ct.cumulative().intervals_size();
842 absl::flat_hash_map<int64, int64> usage;
843 for (int i = 0; i < num_intervals; ++i) {
844 const ConstraintProto& interval_constraint =
845 model.constraints(ct.cumulative().intervals(i));
846 if (ConstraintIsEnforced(interval_constraint)) {
847 const IntervalConstraintProto& interval =
848 interval_constraint.interval();
849 const int64 start = IntervalStart(interval);
850 const int64 duration = IntervalSize(interval);
851 const int64 demand = Value(ct.cumulative().demands(i));
852 for (int64 t = start; t < start + duration; ++t) {
853 usage[t] += demand;
854 if (usage[t] > capacity) return false;
855 }
856 }
857 }
858 return true;
859 }
860
861 bool ElementConstraintIsFeasible(const ConstraintProto& ct) {
862 const int index = Value(ct.element().index());
863 return Value(ct.element().vars(index)) == Value(ct.element().target());
864 }
865
866 bool TableConstraintIsFeasible(const ConstraintProto& ct) {
867 const int size = ct.table().vars_size();
868 if (size == 0) return true;
869 for (int row_start = 0; row_start < ct.table().values_size();
870 row_start += size) {
871 int i = 0;
872 while (Value(ct.table().vars(i)) == ct.table().values(row_start + i)) {
873 ++i;
874 if (i == size) return !ct.table().negated();
875 }
876 }
877 return ct.table().negated();
878 }
879
880 bool AutomatonConstraintIsFeasible(const ConstraintProto& ct) {
881 // Build the transition table {tail, label} -> head.
882 absl::flat_hash_map<std::pair<int64, int64>, int64> transition_map;
883 const int num_transitions = ct.automaton().transition_tail().size();
884 for (int i = 0; i < num_transitions; ++i) {
885 transition_map[{ct.automaton().transition_tail(i),
886 ct.automaton().transition_label(i)}] =
887 ct.automaton().transition_head(i);
888 }
889
890 // Walk the automaton.
891 int64 current_state = ct.automaton().starting_state();
892 const int num_steps = ct.automaton().vars_size();
893 for (int i = 0; i < num_steps; ++i) {
894 const std::pair<int64, int64> key = {current_state,
895 Value(ct.automaton().vars(i))};
896 if (!gtl::ContainsKey(transition_map, key)) {
897 return false;
898 }
899 current_state = transition_map[key];
900 }
901
902 // Check we are now in a final state.
903 for (const int64 final : ct.automaton().final_states()) {
904 if (current_state == final) return true;
905 }
906 return false;
907 }
908
909 bool CircuitConstraintIsFeasible(const ConstraintProto& ct) {
910 // Compute the set of relevant nodes for the constraint and set the next of
911 // each of them. This also detects duplicate nexts.
912 const int num_arcs = ct.circuit().tails_size();
913 absl::flat_hash_set<int> nodes;
914 absl::flat_hash_map<int, int> nexts;
915 for (int i = 0; i < num_arcs; ++i) {
916 const int tail = ct.circuit().tails(i);
917 const int head = ct.circuit().heads(i);
918 nodes.insert(tail);
919 nodes.insert(head);
920 if (LiteralIsFalse(ct.circuit().literals(i))) continue;
921 if (nexts.contains(tail)) return false; // Duplicate.
922 nexts[tail] = head;
923 }
924
925 // All node must have a next.
926 int in_cycle;
927 int cycle_size = 0;
928 for (const int node : nodes) {
929 if (!nexts.contains(node)) return false; // No next.
930 if (nexts[node] == node) continue; // skip self-loop.
931 in_cycle = node;
932 ++cycle_size;
933 }
934 if (cycle_size == 0) return true;
935
936 // Check that we have only one cycle. visited is used to not loop forever if
937 // we have a "rho" shape instead of a cycle.
938 absl::flat_hash_set<int> visited;
939 int current = in_cycle;
940 int num_visited = 0;
941 while (!visited.contains(current)) {
942 ++num_visited;
943 visited.insert(current);
944 current = nexts[current];
945 }
946 if (current != in_cycle) return false; // Rho shape.
947 return num_visited == cycle_size; // Another cycle somewhere if false.
948 }
949
950 bool RoutesConstraintIsFeasible(const ConstraintProto& ct) {
951 const int num_arcs = ct.routes().tails_size();
952 int num_used_arcs = 0;
953 int num_self_arcs = 0;
954 int num_nodes = 0;
955 std::vector<int> tail_to_head;
956 std::vector<int> depot_nexts;
957 for (int i = 0; i < num_arcs; ++i) {
958 const int tail = ct.routes().tails(i);
959 const int head = ct.routes().heads(i);
960 num_nodes = std::max(num_nodes, 1 + tail);
961 num_nodes = std::max(num_nodes, 1 + head);
962 tail_to_head.resize(num_nodes, -1);
963 if (LiteralIsTrue(ct.routes().literals(i))) {
964 if (tail == head) {
965 if (tail == 0) return false;
966 ++num_self_arcs;
967 continue;
968 }
969 ++num_used_arcs;
970 if (tail == 0) {
971 depot_nexts.push_back(head);
972 } else {
973 if (tail_to_head[tail] != -1) return false;
974 tail_to_head[tail] = head;
975 }
976 }
977 }
978
979 // An empty constraint with no node to visit should be feasible.
980 if (num_nodes == 0) return true;
981
982 // Make sure each routes from the depot go back to it, and count such arcs.
983 int count = 0;
984 for (int start : depot_nexts) {
985 ++count;
986 while (start != 0) {
987 if (tail_to_head[start] == -1) return false;
988 start = tail_to_head[start];
989 ++count;
990 }
991 }
992
993 if (count != num_used_arcs) {
994 VLOG(1) << "count: " << count << " != num_used_arcs:" << num_used_arcs;
995 return false;
996 }
997
998 // Each routes cover as many node as there is arcs, but this way we count
999 // multiple times the depot. So the number of nodes covered are:
1000 // count - depot_nexts.size() + 1.
1001 // And this number + the self arcs should be num_nodes.
1002 if (count - depot_nexts.size() + 1 + num_self_arcs != num_nodes) {
1003 VLOG(1) << "Not all nodes are covered!";
1004 return false;
1005 }
1006
1007 return true;
1008 }
1009
1010 bool InverseConstraintIsFeasible(const ConstraintProto& ct) {
1011 const int num_variables = ct.inverse().f_direct_size();
1012 if (num_variables != ct.inverse().f_inverse_size()) return false;
1013 // Check that f_inverse(f_direct(i)) == i; this is sufficient.
1014 for (int i = 0; i < num_variables; i++) {
1015 const int fi = Value(ct.inverse().f_direct(i));
1016 if (fi < 0 || num_variables <= fi) return false;
1017 if (i != Value(ct.inverse().f_inverse(fi))) return false;
1018 }
1019 return true;
1020 }
1021
1022 bool ReservoirConstraintIsFeasible(const ConstraintProto& ct) {
1023 const int num_variables = ct.reservoir().times_size();
1024 const int64 min_level = ct.reservoir().min_level();
1025 const int64 max_level = ct.reservoir().max_level();
1026 std::map<int64, int64> deltas;
1027 deltas[0] = 0;
1028 const bool has_active_variables = ct.reservoir().actives_size() > 0;
1029 for (int i = 0; i < num_variables; i++) {
1030 const int64 time = Value(ct.reservoir().times(i));
1031 if (time < 0) {
1032 VLOG(1) << "reservoir times(" << i << ") is negative.";
1033 return false;
1034 }
1035 if (!has_active_variables || Value(ct.reservoir().actives(i)) == 1) {
1036 deltas[time] += ct.reservoir().demands(i);
1037 }
1038 }
1039 int64 current_level = 0;
1040 for (const auto& delta : deltas) {
1041 current_level += delta.second;
1042 if (current_level < min_level || current_level > max_level) {
1043 VLOG(1) << "Reservoir level " << current_level
1044 << " is out of bounds at time" << delta.first;
1045 return false;
1046 }
1047 }
1048 return true;
1049 }
1050
1051 private:
1052 std::vector<int64> variable_values_;
1053};
1054
1055} // namespace
1056
1057bool SolutionIsFeasible(const CpModelProto& model,
1058 const std::vector<int64>& variable_values,
1059 const CpModelProto* mapping_proto,
1060 const std::vector<int>* postsolve_mapping) {
1061 if (variable_values.size() != model.variables_size()) {
1062 VLOG(1) << "Wrong number of variables in the solution vector";
1063 return false;
1064 }
1065
1066 // Check that all values fall in the variable domains.
1067 for (int i = 0; i < model.variables_size(); ++i) {
1068 if (!DomainInProtoContains(model.variables(i), variable_values[i])) {
1069 VLOG(1) << "Variable #" << i << " has value " << variable_values[i]
1070 << " which do not fall in its domain: "
1071 << ProtobufShortDebugString(model.variables(i));
1072 return false;
1073 }
1074 }
1075
1076 CHECK_EQ(variable_values.size(), model.variables_size());
1077 ConstraintChecker checker(variable_values);
1078
1079 for (int c = 0; c < model.constraints_size(); ++c) {
1080 const ConstraintProto& ct = model.constraints(c);
1081
1082 if (!checker.ConstraintIsEnforced(ct)) continue;
1083
1084 bool is_feasible = true;
1085 const ConstraintProto::ConstraintCase type = ct.constraint_case();
1086 switch (type) {
1087 case ConstraintProto::ConstraintCase::kBoolOr:
1088 is_feasible = checker.BoolOrConstraintIsFeasible(ct);
1089 break;
1090 case ConstraintProto::ConstraintCase::kBoolAnd:
1091 is_feasible = checker.BoolAndConstraintIsFeasible(ct);
1092 break;
1093 case ConstraintProto::ConstraintCase::kAtMostOne:
1094 is_feasible = checker.AtMostOneConstraintIsFeasible(ct);
1095 break;
1096 case ConstraintProto::ConstraintCase::kExactlyOne:
1097 is_feasible = checker.ExactlyOneConstraintIsFeasible(ct);
1098 break;
1099 case ConstraintProto::ConstraintCase::kBoolXor:
1100 is_feasible = checker.BoolXorConstraintIsFeasible(ct);
1101 break;
1102 case ConstraintProto::ConstraintCase::kLinear:
1103 is_feasible = checker.LinearConstraintIsFeasible(ct);
1104 break;
1105 case ConstraintProto::ConstraintCase::kIntProd:
1106 is_feasible = checker.IntProdConstraintIsFeasible(ct);
1107 break;
1108 case ConstraintProto::ConstraintCase::kIntDiv:
1109 is_feasible = checker.IntDivConstraintIsFeasible(ct);
1110 break;
1111 case ConstraintProto::ConstraintCase::kIntMod:
1112 is_feasible = checker.IntModConstraintIsFeasible(ct);
1113 break;
1114 case ConstraintProto::ConstraintCase::kIntMin:
1115 is_feasible = checker.IntMinConstraintIsFeasible(ct);
1116 break;
1117 case ConstraintProto::ConstraintCase::kLinMin:
1118 is_feasible = checker.LinMinConstraintIsFeasible(ct);
1119 break;
1120 case ConstraintProto::ConstraintCase::kIntMax:
1121 is_feasible = checker.IntMaxConstraintIsFeasible(ct);
1122 break;
1123 case ConstraintProto::ConstraintCase::kLinMax:
1124 is_feasible = checker.LinMaxConstraintIsFeasible(ct);
1125 break;
1126 case ConstraintProto::ConstraintCase::kAllDiff:
1127 is_feasible = checker.AllDiffConstraintIsFeasible(ct);
1128 break;
1129 case ConstraintProto::ConstraintCase::kInterval:
1130 is_feasible = checker.IntervalConstraintIsFeasible(ct);
1131 break;
1132 case ConstraintProto::ConstraintCase::kNoOverlap:
1133 is_feasible = checker.NoOverlapConstraintIsFeasible(model, ct);
1134 break;
1135 case ConstraintProto::ConstraintCase::kNoOverlap2D:
1136 is_feasible = checker.NoOverlap2DConstraintIsFeasible(model, ct);
1137 break;
1138 case ConstraintProto::ConstraintCase::kCumulative:
1139 is_feasible = checker.CumulativeConstraintIsFeasible(model, ct);
1140 break;
1141 case ConstraintProto::ConstraintCase::kElement:
1142 is_feasible = checker.ElementConstraintIsFeasible(ct);
1143 break;
1144 case ConstraintProto::ConstraintCase::kTable:
1145 is_feasible = checker.TableConstraintIsFeasible(ct);
1146 break;
1147 case ConstraintProto::ConstraintCase::kAutomaton:
1148 is_feasible = checker.AutomatonConstraintIsFeasible(ct);
1149 break;
1150 case ConstraintProto::ConstraintCase::kCircuit:
1151 is_feasible = checker.CircuitConstraintIsFeasible(ct);
1152 break;
1153 case ConstraintProto::ConstraintCase::kRoutes:
1154 is_feasible = checker.RoutesConstraintIsFeasible(ct);
1155 break;
1156 case ConstraintProto::ConstraintCase::kInverse:
1157 is_feasible = checker.InverseConstraintIsFeasible(ct);
1158 break;
1159 case ConstraintProto::ConstraintCase::kReservoir:
1160 is_feasible = checker.ReservoirConstraintIsFeasible(ct);
1161 break;
1162 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
1163 // Empty constraint is always feasible.
1164 break;
1165 default:
1166 LOG(FATAL) << "Unuspported constraint: " << ConstraintCaseName(type);
1167 }
1168
1169 // Display a message to help debugging.
1170 if (!is_feasible) {
1171 VLOG(1) << "Failing constraint #" << c << " : "
1172 << ProtobufShortDebugString(model.constraints(c));
1173 if (mapping_proto != nullptr && postsolve_mapping != nullptr) {
1174 std::vector<int> reverse_map(mapping_proto->variables().size(), -1);
1175 for (int var = 0; var < postsolve_mapping->size(); ++var) {
1176 reverse_map[(*postsolve_mapping)[var]] = var;
1177 }
1178 for (const int var : UsedVariables(model.constraints(c))) {
1179 VLOG(1) << "var: " << var << " mapped_to: " << reverse_map[var]
1180 << " value: " << variable_values[var] << " initial_domain: "
1181 << ReadDomainFromProto(model.variables(var))
1182 << " postsolved_domain: "
1183 << ReadDomainFromProto(mapping_proto->variables(var));
1184 }
1185 } else {
1186 for (const int var : UsedVariables(model.constraints(c))) {
1187 VLOG(1) << "var: " << var << " value: " << variable_values[var];
1188 }
1189 }
1190 return false;
1191 }
1192 }
1193 return true;
1194}
1195
1196} // namespace sat
1197} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define LOG(severity)
Definition: base/logging.h:420
#define VLOG(verboselevel)
Definition: base/logging.h:978
We call domain any subset of Int64 = [kint64min, kint64max].
int64 Size() const
Returns the number of elements in the domain.
#define RETURN_IF_NOT_EMPTY(statement)
CpModelProto proto
const Constraint * ct
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
static const int64 kint64max
int64_t int64
static const int64 kint64min
const int FATAL
Definition: log_severity.h:32
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
std::vector< int > UsedVariables(const ConstraintProto &ct)
std::vector< int > UsedIntervals(const ConstraintProto &ct)
bool SolutionIsFeasible(const CpModelProto &model, const std::vector< int64 > &variable_values, const CpModelProto *mapping_proto, const std::vector< int > *postsolve_mapping)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
std::function< int64(const Model &)> Value(IntegerVariable v)
Definition: integer.h:1487
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto &ct)
std::string ConstraintCaseName(ConstraintProto::ConstraintCase constraint_case)
bool RefIsPositive(int ref)
bool DomainInProtoContains(const ProtoWithDomain &proto, int64 value)
std::string ValidateCpModel(const CpModelProto &model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 CapAdd(int64 x, int64 y)
int64 CapProd(int64 x, int64 y)
std::string ProtobufDebugString(const P &message)
std::string ProtobufShortDebugString(const P &message)
bool IntervalsAreSortedAndNonAdjacent(absl::Span< const ClosedInterval > intervals)
Returns true iff we have:
int index
Definition: pack.cc:508
int64 time
Definition: resource.cc:1683
int64 demand
Definition: resource.cc:123
int64 delta
Definition: resource.cc:1684
IntervalVar * interval
Definition: resource.cc:98
int64 tail
int64 head
int64 capacity