Google OR-Tools v9.12
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
cp_model_utils.cc
Go to the documentation of this file.
1// Copyright 2010-2025 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
14#include "ortools/sat/cp_model_utils.h"
15
16#include <cstdint>
17#include <cstdlib>
18#include <functional>
19#include <numeric>
20#include <string>
21#include <utility>
22#include <vector>
23
24#include "absl/container/flat_hash_map.h"
25#include "absl/container/flat_hash_set.h"
26#include "absl/log/check.h"
27#include "absl/strings/str_cat.h"
28#include "absl/strings/string_view.h"
29#include "absl/types/span.h"
30#include "google/protobuf/descriptor.h"
31#include "google/protobuf/message.h"
32#include "google/protobuf/text_format.h"
33#include "ortools/base/stl_util.h"
34#include "ortools/sat/cp_model.pb.h"
35#include "ortools/sat/sat_base.h"
36#include "ortools/util/saturated_arithmetic.h"
37#include "ortools/util/sorted_interval_list.h"
38
39namespace operations_research {
40namespace sat {
41
42namespace {
43
44template <typename IntList>
45void AddIndices(const IntList& indices, std::vector<int>* output) {
46 output->insert(output->end(), indices.begin(), indices.end());
47}
48
49} // namespace
50
51int64_t LinearExpressionGcd(const LinearExpressionProto& expr, int64_t gcd) {
52 gcd = std::gcd(gcd, std::abs(expr.offset()));
53 for (const int64_t coeff : expr.coeffs()) {
54 gcd = std::gcd(gcd, std::abs(coeff));
55 }
56 return gcd;
57}
58
59void DivideLinearExpression(int64_t divisor, LinearExpressionProto* expr) {
60 CHECK_NE(divisor, 0);
61 if (divisor == 1) return;
62
63 DCHECK_EQ(expr->offset() % divisor, 0);
64 expr->set_offset(expr->offset() / divisor);
65 for (int i = 0; i < expr->vars_size(); ++i) {
66 DCHECK_EQ(expr->coeffs(i) % divisor, 0);
67 expr->set_coeffs(i, expr->coeffs(i) / divisor);
68 }
69}
70
71void SetToNegatedLinearExpression(const LinearExpressionProto& input_expr,
72 LinearExpressionProto* output_negated_expr) {
73 output_negated_expr->Clear();
74 for (int i = 0; i < input_expr.vars_size(); ++i) {
75 output_negated_expr->add_vars(NegatedRef(input_expr.vars(i)));
76 output_negated_expr->add_coeffs(input_expr.coeffs(i));
77 }
78 output_negated_expr->set_offset(-input_expr.offset());
79}
80
81IndexReferences GetReferencesUsedByConstraint(const ConstraintProto& ct) {
82 IndexReferences output;
83 GetReferencesUsedByConstraint(ct, &output.variables, &output.literals);
84 return output;
85}
86
87void GetReferencesUsedByConstraint(const ConstraintProto& ct,
88 std::vector<int>* variables,
89 std::vector<int>* literals) {
90 variables->clear();
91 literals->clear();
92 switch (ct.constraint_case()) {
93 case ConstraintProto::ConstraintCase::kBoolOr:
94 AddIndices(ct.bool_or().literals(), literals);
95 break;
96 case ConstraintProto::ConstraintCase::kBoolAnd:
97 AddIndices(ct.bool_and().literals(), literals);
98 break;
99 case ConstraintProto::ConstraintCase::kAtMostOne:
100 AddIndices(ct.at_most_one().literals(), literals);
101 break;
102 case ConstraintProto::ConstraintCase::kExactlyOne:
103 AddIndices(ct.exactly_one().literals(), literals);
104 break;
105 case ConstraintProto::ConstraintCase::kBoolXor:
106 AddIndices(ct.bool_xor().literals(), literals);
107 break;
108 case ConstraintProto::ConstraintCase::kIntDiv:
109 AddIndices(ct.int_div().target().vars(), variables);
110 for (const LinearExpressionProto& expr : ct.int_div().exprs()) {
111 AddIndices(expr.vars(), variables);
112 }
113 break;
114 case ConstraintProto::ConstraintCase::kIntMod:
115 AddIndices(ct.int_mod().target().vars(), variables);
116 for (const LinearExpressionProto& expr : ct.int_mod().exprs()) {
117 AddIndices(expr.vars(), variables);
118 }
119 break;
120 case ConstraintProto::ConstraintCase::kLinMax: {
121 AddIndices(ct.lin_max().target().vars(), variables);
122 for (const LinearExpressionProto& expr : ct.lin_max().exprs()) {
123 AddIndices(expr.vars(), variables);
124 }
125 break;
126 }
127 case ConstraintProto::ConstraintCase::kIntProd:
128 AddIndices(ct.int_prod().target().vars(), variables);
129 for (const LinearExpressionProto& expr : ct.int_prod().exprs()) {
130 AddIndices(expr.vars(), variables);
131 }
132 break;
133 case ConstraintProto::ConstraintCase::kLinear:
134 AddIndices(ct.linear().vars(), variables);
135 break;
136 case ConstraintProto::ConstraintCase::kAllDiff:
137 for (const LinearExpressionProto& expr : ct.all_diff().exprs()) {
138 AddIndices(expr.vars(), variables);
139 }
140 break;
141 case ConstraintProto::ConstraintCase::kDummyConstraint:
142 AddIndices(ct.dummy_constraint().vars(), variables);
143 break;
144 case ConstraintProto::ConstraintCase::kElement:
145 if (ct.element().index() != 0 || ct.element().target() != 0 ||
146 !ct.element().vars().empty()) {
147 variables->push_back(ct.element().index());
148 variables->push_back(ct.element().target());
149 AddIndices(ct.element().vars(), variables);
150 } else if (ct.element().has_linear_index() ||
151 ct.element().has_linear_target() ||
152 !ct.element().exprs().empty()) {
153 AddIndices(ct.element().linear_index().vars(), variables);
154 AddIndices(ct.element().linear_target().vars(), variables);
155 for (const LinearExpressionProto& expr : ct.element().exprs()) {
156 AddIndices(expr.vars(), variables);
157 }
158 }
159 break;
160 case ConstraintProto::ConstraintCase::kCircuit:
161 AddIndices(ct.circuit().literals(), literals);
162 break;
163 case ConstraintProto::ConstraintCase::kRoutes:
164 AddIndices(ct.routes().literals(), literals);
165 break;
166 case ConstraintProto::ConstraintCase::kInverse:
167 AddIndices(ct.inverse().f_direct(), variables);
168 AddIndices(ct.inverse().f_inverse(), variables);
169 break;
170 case ConstraintProto::ConstraintCase::kReservoir:
171 for (const LinearExpressionProto& time : ct.reservoir().time_exprs()) {
172 AddIndices(time.vars(), variables);
173 }
174 for (const LinearExpressionProto& level :
175 ct.reservoir().level_changes()) {
176 AddIndices(level.vars(), variables);
177 }
178 AddIndices(ct.reservoir().active_literals(), literals);
179 break;
180 case ConstraintProto::ConstraintCase::kTable:
181 if (!ct.table().vars().empty()) {
182 AddIndices(ct.table().vars(), variables);
183 } else {
184 for (const LinearExpressionProto& expr : ct.table().exprs()) {
185 AddIndices(expr.vars(), variables);
186 }
187 }
188 break;
189 case ConstraintProto::ConstraintCase::kAutomaton:
190 if (!ct.automaton().vars().empty()) {
191 AddIndices(ct.automaton().vars(), variables);
192 } else {
193 for (const LinearExpressionProto& expr : ct.automaton().exprs()) {
194 AddIndices(expr.vars(), variables);
195 }
196 }
197 break;
198 case ConstraintProto::ConstraintCase::kInterval:
199 AddIndices(ct.interval().start().vars(), variables);
200 AddIndices(ct.interval().size().vars(), variables);
201 AddIndices(ct.interval().end().vars(), variables);
202 break;
203 case ConstraintProto::ConstraintCase::kNoOverlap:
204 break;
205 case ConstraintProto::ConstraintCase::kNoOverlap2D:
206 break;
207 case ConstraintProto::ConstraintCase::kCumulative:
208 AddIndices(ct.cumulative().capacity().vars(), variables);
209 for (const LinearExpressionProto& demand : ct.cumulative().demands()) {
210 AddIndices(demand.vars(), variables);
211 }
212 break;
213 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
214 break;
215 }
216}
217
218#define APPLY_TO_SINGULAR_FIELD(ct_name, field_name) \
219 { \
220 int temp = ct->mutable_##ct_name()->field_name(); \
221 f(&temp); \
222 ct->mutable_##ct_name()->set_##field_name(temp); \
223 }
224
225#define APPLY_TO_REPEATED_FIELD(ct_name, field_name) \
226 { \
227 for (int& r : *ct->mutable_##ct_name()->mutable_##field_name()) f(&r); \
228 }
229
230void ApplyToAllLiteralIndices(const std::function<void(int*)>& f,
231 ConstraintProto* ct) {
232 for (int& r : *ct->mutable_enforcement_literal()) f(&r);
233 switch (ct->constraint_case()) {
234 case ConstraintProto::ConstraintCase::kBoolOr:
235 APPLY_TO_REPEATED_FIELD(bool_or, literals);
236 break;
237 case ConstraintProto::ConstraintCase::kBoolAnd:
238 APPLY_TO_REPEATED_FIELD(bool_and, literals);
239 break;
240 case ConstraintProto::ConstraintCase::kAtMostOne:
241 APPLY_TO_REPEATED_FIELD(at_most_one, literals);
242 break;
243 case ConstraintProto::ConstraintCase::kExactlyOne:
244 APPLY_TO_REPEATED_FIELD(exactly_one, literals);
245 break;
246 case ConstraintProto::ConstraintCase::kBoolXor:
247 APPLY_TO_REPEATED_FIELD(bool_xor, literals);
248 break;
249 case ConstraintProto::ConstraintCase::kIntDiv:
250 break;
251 case ConstraintProto::ConstraintCase::kIntMod:
252 break;
253 case ConstraintProto::ConstraintCase::kLinMax:
254 break;
255 case ConstraintProto::ConstraintCase::kIntProd:
256 break;
257 case ConstraintProto::ConstraintCase::kLinear:
258 break;
259 case ConstraintProto::ConstraintCase::kAllDiff:
260 break;
261 case ConstraintProto::ConstraintCase::kDummyConstraint:
262 break;
263 case ConstraintProto::ConstraintCase::kElement:
264 break;
265 case ConstraintProto::ConstraintCase::kCircuit:
266 APPLY_TO_REPEATED_FIELD(circuit, literals);
267 break;
268 case ConstraintProto::ConstraintCase::kRoutes:
269 APPLY_TO_REPEATED_FIELD(routes, literals);
270 break;
271 case ConstraintProto::ConstraintCase::kInverse:
272 break;
273 case ConstraintProto::ConstraintCase::kReservoir:
274 APPLY_TO_REPEATED_FIELD(reservoir, active_literals);
275 break;
276 case ConstraintProto::ConstraintCase::kTable:
277 break;
278 case ConstraintProto::ConstraintCase::kAutomaton:
279 break;
280 case ConstraintProto::ConstraintCase::kInterval:
281 break;
282 case ConstraintProto::ConstraintCase::kNoOverlap:
283 break;
284 case ConstraintProto::ConstraintCase::kNoOverlap2D:
285 break;
286 case ConstraintProto::ConstraintCase::kCumulative:
287 break;
288 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
289 break;
290 }
291}
292
293void ApplyToAllVariableIndices(const std::function<void(int*)>& f,
294 ConstraintProto* ct) {
295 switch (ct->constraint_case()) {
296 case ConstraintProto::ConstraintCase::kBoolOr:
297 break;
298 case ConstraintProto::ConstraintCase::kBoolAnd:
299 break;
300 case ConstraintProto::ConstraintCase::kAtMostOne:
301 break;
302 case ConstraintProto::ConstraintCase::kExactlyOne:
303 break;
304 case ConstraintProto::ConstraintCase::kBoolXor:
305 break;
306 case ConstraintProto::ConstraintCase::kIntDiv:
307 APPLY_TO_REPEATED_FIELD(int_div, target()->mutable_vars);
308 for (int i = 0; i < ct->int_div().exprs_size(); ++i) {
309 APPLY_TO_REPEATED_FIELD(int_div, exprs(i)->mutable_vars);
310 }
311 break;
312 case ConstraintProto::ConstraintCase::kIntMod:
313 APPLY_TO_REPEATED_FIELD(int_mod, target()->mutable_vars);
314 for (int i = 0; i < ct->int_mod().exprs_size(); ++i) {
315 APPLY_TO_REPEATED_FIELD(int_mod, exprs(i)->mutable_vars);
316 }
317 break;
318 case ConstraintProto::ConstraintCase::kLinMax:
319 APPLY_TO_REPEATED_FIELD(lin_max, target()->mutable_vars);
320 for (int i = 0; i < ct->lin_max().exprs_size(); ++i) {
321 APPLY_TO_REPEATED_FIELD(lin_max, exprs(i)->mutable_vars);
322 }
323 break;
324 case ConstraintProto::ConstraintCase::kIntProd:
325 APPLY_TO_REPEATED_FIELD(int_prod, target()->mutable_vars);
326 for (int i = 0; i < ct->int_prod().exprs_size(); ++i) {
327 APPLY_TO_REPEATED_FIELD(int_prod, exprs(i)->mutable_vars);
328 }
329 break;
330 case ConstraintProto::ConstraintCase::kLinear:
331 APPLY_TO_REPEATED_FIELD(linear, vars);
332 break;
333 case ConstraintProto::ConstraintCase::kAllDiff:
334 for (int i = 0; i < ct->all_diff().exprs_size(); ++i) {
335 APPLY_TO_REPEATED_FIELD(all_diff, exprs(i)->mutable_vars);
336 }
337 break;
338 case ConstraintProto::ConstraintCase::kDummyConstraint:
339 APPLY_TO_REPEATED_FIELD(dummy_constraint, vars);
340 break;
341 case ConstraintProto::ConstraintCase::kElement:
342 if (ct->element().index() != 0 || ct->element().target() != 0 ||
343 !ct->element().vars().empty()) {
344 APPLY_TO_SINGULAR_FIELD(element, index);
345 APPLY_TO_SINGULAR_FIELD(element, target);
346 APPLY_TO_REPEATED_FIELD(element, vars);
347 } else if (ct->element().has_linear_index() ||
348 ct->element().has_linear_target() ||
349 !ct->element().exprs().empty()) {
350 APPLY_TO_REPEATED_FIELD(element, linear_index()->mutable_vars);
351 APPLY_TO_REPEATED_FIELD(element, linear_target()->mutable_vars);
352 for (int i = 0; i < ct->element().exprs_size(); ++i) {
353 APPLY_TO_REPEATED_FIELD(element, exprs(i)->mutable_vars);
354 }
355 }
356 break;
357 case ConstraintProto::ConstraintCase::kCircuit:
358 break;
359 case ConstraintProto::ConstraintCase::kRoutes:
360 break;
361 case ConstraintProto::ConstraintCase::kInverse:
362 APPLY_TO_REPEATED_FIELD(inverse, f_direct);
363 APPLY_TO_REPEATED_FIELD(inverse, f_inverse);
364 break;
365 case ConstraintProto::ConstraintCase::kReservoir:
366 for (int i = 0; i < ct->reservoir().time_exprs_size(); ++i) {
367 APPLY_TO_REPEATED_FIELD(reservoir, time_exprs(i)->mutable_vars);
368 }
369 for (int i = 0; i < ct->reservoir().level_changes_size(); ++i) {
370 APPLY_TO_REPEATED_FIELD(reservoir, level_changes(i)->mutable_vars);
371 }
372 break;
373 case ConstraintProto::ConstraintCase::kTable:
374 if (!ct->table().vars().empty()) {
375 APPLY_TO_REPEATED_FIELD(table, vars);
376 } else {
377 for (int i = 0; i < ct->table().exprs_size(); ++i) {
378 APPLY_TO_REPEATED_FIELD(table, exprs(i)->mutable_vars);
379 }
380 }
381 break;
382 case ConstraintProto::ConstraintCase::kAutomaton:
383 if (!ct->automaton().vars().empty()) {
384 APPLY_TO_REPEATED_FIELD(automaton, vars);
385 } else {
386 for (int i = 0; i < ct->automaton().exprs_size(); ++i) {
387 APPLY_TO_REPEATED_FIELD(automaton, exprs(i)->mutable_vars);
388 }
389 }
390 break;
391 case ConstraintProto::ConstraintCase::kInterval:
392 APPLY_TO_REPEATED_FIELD(interval, start()->mutable_vars);
393 APPLY_TO_REPEATED_FIELD(interval, size()->mutable_vars);
394 APPLY_TO_REPEATED_FIELD(interval, end()->mutable_vars);
395 break;
396 case ConstraintProto::ConstraintCase::kNoOverlap:
397 break;
398 case ConstraintProto::ConstraintCase::kNoOverlap2D:
399 break;
400 case ConstraintProto::ConstraintCase::kCumulative:
401 APPLY_TO_REPEATED_FIELD(cumulative, capacity()->mutable_vars);
402 for (int i = 0; i < ct->cumulative().demands_size(); ++i) {
403 for (int& r :
404 *ct->mutable_cumulative()->mutable_demands(i)->mutable_vars()) {
405 f(&r);
406 }
407 }
408 break;
409 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
410 break;
411 }
412}
413
414void ApplyToAllIntervalIndices(const std::function<void(int*)>& f,
415 ConstraintProto* ct) {
416 switch (ct->constraint_case()) {
417 case ConstraintProto::ConstraintCase::kBoolOr:
418 break;
419 case ConstraintProto::ConstraintCase::kBoolAnd:
420 break;
421 case ConstraintProto::ConstraintCase::kAtMostOne:
422 break;
423 case ConstraintProto::ConstraintCase::kExactlyOne:
424 break;
425 case ConstraintProto::ConstraintCase::kBoolXor:
426 break;
427 case ConstraintProto::ConstraintCase::kIntDiv:
428 break;
429 case ConstraintProto::ConstraintCase::kIntMod:
430 break;
431 case ConstraintProto::ConstraintCase::kLinMax:
432 break;
433 case ConstraintProto::ConstraintCase::kIntProd:
434 break;
435 case ConstraintProto::ConstraintCase::kLinear:
436 break;
437 case ConstraintProto::ConstraintCase::kAllDiff:
438 break;
439 case ConstraintProto::ConstraintCase::kDummyConstraint:
440 break;
441 case ConstraintProto::ConstraintCase::kElement:
442 break;
443 case ConstraintProto::ConstraintCase::kCircuit:
444 break;
445 case ConstraintProto::ConstraintCase::kRoutes:
446 break;
447 case ConstraintProto::ConstraintCase::kInverse:
448 break;
449 case ConstraintProto::ConstraintCase::kReservoir:
450 break;
451 case ConstraintProto::ConstraintCase::kTable:
452 break;
453 case ConstraintProto::ConstraintCase::kAutomaton:
454 break;
455 case ConstraintProto::ConstraintCase::kInterval:
456 break;
457 case ConstraintProto::ConstraintCase::kNoOverlap:
458 APPLY_TO_REPEATED_FIELD(no_overlap, intervals);
459 break;
460 case ConstraintProto::ConstraintCase::kNoOverlap2D:
461 APPLY_TO_REPEATED_FIELD(no_overlap_2d, x_intervals);
462 APPLY_TO_REPEATED_FIELD(no_overlap_2d, y_intervals);
463 break;
464 case ConstraintProto::ConstraintCase::kCumulative:
465 APPLY_TO_REPEATED_FIELD(cumulative, intervals);
466 break;
467 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
468 break;
469 }
470}
471
472#undef APPLY_TO_SINGULAR_FIELD
473#undef APPLY_TO_REPEATED_FIELD
474
475absl::string_view ConstraintCaseName(
476 ConstraintProto::ConstraintCase constraint_case) {
477 switch (constraint_case) {
478 case ConstraintProto::ConstraintCase::kBoolOr:
479 return "kBoolOr";
480 case ConstraintProto::ConstraintCase::kBoolAnd:
481 return "kBoolAnd";
482 case ConstraintProto::ConstraintCase::kAtMostOne:
483 return "kAtMostOne";
484 case ConstraintProto::ConstraintCase::kExactlyOne:
485 return "kExactlyOne";
486 case ConstraintProto::ConstraintCase::kBoolXor:
487 return "kBoolXor";
488 case ConstraintProto::ConstraintCase::kIntDiv:
489 return "kIntDiv";
490 case ConstraintProto::ConstraintCase::kIntMod:
491 return "kIntMod";
492 case ConstraintProto::ConstraintCase::kLinMax:
493 return "kLinMax";
494 case ConstraintProto::ConstraintCase::kIntProd:
495 return "kIntProd";
496 case ConstraintProto::ConstraintCase::kLinear:
497 return "kLinear";
498 case ConstraintProto::ConstraintCase::kAllDiff:
499 return "kAllDiff";
500 case ConstraintProto::ConstraintCase::kDummyConstraint:
501 return "kDummyConstraint";
502 case ConstraintProto::ConstraintCase::kElement:
503 return "kElement";
504 case ConstraintProto::ConstraintCase::kCircuit:
505 return "kCircuit";
506 case ConstraintProto::ConstraintCase::kRoutes:
507 return "kRoutes";
508 case ConstraintProto::ConstraintCase::kInverse:
509 return "kInverse";
510 case ConstraintProto::ConstraintCase::kReservoir:
511 return "kReservoir";
512 case ConstraintProto::ConstraintCase::kTable:
513 return "kTable";
514 case ConstraintProto::ConstraintCase::kAutomaton:
515 return "kAutomaton";
516 case ConstraintProto::ConstraintCase::kInterval:
517 return "kInterval";
518 case ConstraintProto::ConstraintCase::kNoOverlap:
519 return "kNoOverlap";
520 case ConstraintProto::ConstraintCase::kNoOverlap2D:
521 return "kNoOverlap2D";
522 case ConstraintProto::ConstraintCase::kCumulative:
523 return "kCumulative";
524 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
525 return "kEmpty";
526 }
527}
528
529std::vector<int> UsedVariables(const ConstraintProto& ct) {
530 std::vector<int> result;
531 GetReferencesUsedByConstraint(ct, &result, &result);
532 for (int& ref : result) {
533 ref = PositiveRef(ref);
534 }
535 for (const int lit : ct.enforcement_literal()) {
536 result.push_back(PositiveRef(lit));
537 }
538 gtl::STLSortAndRemoveDuplicates(&result);
539 return result;
540}
541
542std::vector<int> UsedIntervals(const ConstraintProto& ct) {
543 std::vector<int> used_intervals;
544 switch (ct.constraint_case()) {
545 case ConstraintProto::ConstraintCase::kBoolOr:
546 break;
547 case ConstraintProto::ConstraintCase::kBoolAnd:
548 break;
549 case ConstraintProto::ConstraintCase::kAtMostOne:
550 break;
551 case ConstraintProto::ConstraintCase::kExactlyOne:
552 break;
553 case ConstraintProto::ConstraintCase::kBoolXor:
554 break;
555 case ConstraintProto::ConstraintCase::kIntDiv:
556 break;
557 case ConstraintProto::ConstraintCase::kIntMod:
558 break;
559 case ConstraintProto::ConstraintCase::kLinMax:
560 break;
561 case ConstraintProto::ConstraintCase::kIntProd:
562 break;
563 case ConstraintProto::ConstraintCase::kLinear:
564 break;
565 case ConstraintProto::ConstraintCase::kAllDiff:
566 break;
567 case ConstraintProto::ConstraintCase::kDummyConstraint:
568 break;
569 case ConstraintProto::ConstraintCase::kElement:
570 break;
571 case ConstraintProto::ConstraintCase::kCircuit:
572 break;
573 case ConstraintProto::ConstraintCase::kRoutes:
574 break;
575 case ConstraintProto::ConstraintCase::kInverse:
576 break;
577 case ConstraintProto::ConstraintCase::kReservoir:
578 break;
579 case ConstraintProto::ConstraintCase::kTable:
580 break;
581 case ConstraintProto::ConstraintCase::kAutomaton:
582 break;
583 case ConstraintProto::ConstraintCase::kInterval:
584 break;
585 case ConstraintProto::ConstraintCase::kNoOverlap:
586 AddIndices(ct.no_overlap().intervals(), &used_intervals);
587 break;
588 case ConstraintProto::ConstraintCase::kNoOverlap2D:
589 AddIndices(ct.no_overlap_2d().x_intervals(), &used_intervals);
590 AddIndices(ct.no_overlap_2d().y_intervals(), &used_intervals);
591 break;
592 case ConstraintProto::ConstraintCase::kCumulative:
593 AddIndices(ct.cumulative().intervals(), &used_intervals);
594 break;
595 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
596 break;
597 }
598 gtl::STLSortAndRemoveDuplicates(&used_intervals);
599 return used_intervals;
600}
601
602int64_t ComputeInnerObjective(const CpObjectiveProto& objective,
603 absl::Span<const int64_t> solution) {
604 int64_t objective_value = 0;
605 for (int i = 0; i < objective.vars_size(); ++i) {
606 int64_t coeff = objective.coeffs(i);
607 const int ref = objective.vars(i);
608 const int var = PositiveRef(ref);
609 if (!RefIsPositive(ref)) coeff = -coeff;
610 objective_value += coeff * solution[var];
611 }
612 return objective_value;
613}
614
615bool ExpressionContainsSingleRef(const LinearExpressionProto& expr) {
616 return expr.offset() == 0 && expr.vars_size() == 1 &&
617 std::abs(expr.coeffs(0)) == 1;
618}
619
620bool ExpressionIsAffine(const LinearExpressionProto& expr) {
621 return expr.vars_size() <= 1;
622}
623
624// Returns the reference the expression can be reduced to. It will DCHECK that
625// ExpressionContainsSingleRef(expr) is true.
626int GetSingleRefFromExpression(const LinearExpressionProto& expr) {
627 DCHECK(ExpressionContainsSingleRef(expr));
628 return expr.coeffs(0) == 1 ? expr.vars(0) : NegatedRef(expr.vars(0));
629}
630
631void AddLinearExpressionToLinearConstraint(const LinearExpressionProto& expr,
632 int64_t coefficient,
633 LinearConstraintProto* linear) {
634 for (int i = 0; i < expr.vars_size(); ++i) {
635 linear->add_vars(expr.vars(i));
636 linear->add_coeffs(expr.coeffs(i) * coefficient);
637 }
638 DCHECK(!linear->domain().empty());
639 const int64_t shift = coefficient * expr.offset();
640 if (shift != 0) {
641 FillDomainInProto(ReadDomainFromProto(*linear).AdditionWith(Domain(-shift)),
642 linear);
643 }
644}
645
646void AddWeightedLiteralToLinearConstraint(int lit, int64_t coeff,
647 LinearConstraintProto* linear,
648 int64_t* offset) {
649 if (coeff == 0) return;
650 if (RefIsPositive(lit)) {
651 linear->add_vars(lit);
652 linear->add_coeffs(coeff);
653 } else {
654 linear->add_vars(NegatedRef(lit));
655 linear->add_coeffs(-coeff);
656 *offset += coeff;
657 }
658}
659
660bool SafeAddLinearExpressionToLinearConstraint(
661 const LinearExpressionProto& expr, int64_t coefficient,
662 LinearConstraintProto* linear) {
663 for (int i = 0; i < expr.vars_size(); ++i) {
664 linear->add_vars(expr.vars(i));
665 const int64_t prod = CapProd(expr.coeffs(i), coefficient);
666 if (AtMinOrMaxInt64(prod)) return false;
667 linear->add_coeffs(prod);
668 }
669 DCHECK(!linear->domain().empty());
670
671 const int64_t shift = CapProd(coefficient, expr.offset());
672 if (AtMinOrMaxInt64(shift)) return false;
673 Domain d = ReadDomainFromProto(*linear).AdditionWith(Domain(-shift));
674 if (AtMinOrMaxInt64(d.Min()) || AtMinOrMaxInt64(d.Max())) return false;
675 FillDomainInProto(d, linear);
676 return true;
677}
678
679bool LinearExpressionProtosAreEqual(const LinearExpressionProto& a,
680 const LinearExpressionProto& b,
681 int64_t b_scaling) {
682 if (a.vars_size() != b.vars_size()) return false;
683 if (a.offset() != b.offset() * b_scaling) return false;
684 absl::flat_hash_map<int, int64_t> coeffs;
685 for (int i = 0; i < a.vars_size(); ++i) {
686 coeffs[a.vars(i)] += a.coeffs(i);
687 coeffs[b.vars(i)] += -b.coeffs(i) * b_scaling;
688 }
689
690 for (const auto [var, coeff] : coeffs) {
691 if (coeff != 0) return false;
692 }
693 return true;
694}
695
696uint64_t FingerprintExpression(const LinearExpressionProto& lin,
697 uint64_t seed) {
698 uint64_t fp = seed;
699 if (!lin.vars().empty()) {
700 fp = FingerprintRepeatedField(lin.vars(), fp);
701 fp = FingerprintRepeatedField(lin.coeffs(), fp);
702 }
703 fp = FingerprintSingleField(lin.offset(), fp);
704 return fp;
705}
706
707uint64_t FingerprintModel(const CpModelProto& model, uint64_t seed) {
708 uint64_t fp = seed;
709 for (const IntegerVariableProto& var_proto : model.variables()) {
710 fp = FingerprintRepeatedField(var_proto.domain(), fp);
711 }
712 for (const ConstraintProto& ct : model.constraints()) {
713 if (!ct.enforcement_literal().empty()) {
714 fp = FingerprintRepeatedField(ct.enforcement_literal(), fp);
715 }
716 switch (ct.constraint_case()) {
717 case ConstraintProto::ConstraintCase::kBoolOr:
718 fp = FingerprintRepeatedField(ct.bool_or().literals(), fp);
719 break;
720 case ConstraintProto::ConstraintCase::kBoolAnd:
721 fp = FingerprintRepeatedField(ct.bool_and().literals(), fp);
722 break;
723 case ConstraintProto::ConstraintCase::kAtMostOne:
724 fp = FingerprintRepeatedField(ct.at_most_one().literals(), fp);
725 break;
726 case ConstraintProto::ConstraintCase::kExactlyOne:
727 fp = FingerprintRepeatedField(ct.exactly_one().literals(), fp);
728 break;
729 case ConstraintProto::ConstraintCase::kBoolXor:
730 fp = FingerprintRepeatedField(ct.bool_xor().literals(), fp);
731 break;
732 case ConstraintProto::ConstraintCase::kIntDiv:
733 fp = FingerprintExpression(ct.int_div().target(), fp);
734 for (const LinearExpressionProto& expr : ct.int_div().exprs()) {
735 fp = FingerprintExpression(expr, fp);
736 }
737 break;
738 case ConstraintProto::ConstraintCase::kIntMod:
739 fp = FingerprintExpression(ct.int_mod().target(), fp);
740 for (const LinearExpressionProto& expr : ct.int_mod().exprs()) {
741 fp = FingerprintExpression(expr, fp);
742 }
743 break;
744 case ConstraintProto::ConstraintCase::kLinMax: {
745 fp = FingerprintExpression(ct.lin_max().target(), fp);
746 for (const LinearExpressionProto& expr : ct.lin_max().exprs()) {
747 fp = FingerprintExpression(expr, fp);
748 }
749 break;
750 }
751 case ConstraintProto::ConstraintCase::kIntProd:
752 fp = FingerprintExpression(ct.int_prod().target(), fp);
753 for (const LinearExpressionProto& expr : ct.int_prod().exprs()) {
754 fp = FingerprintExpression(expr, fp);
755 }
756 break;
757 case ConstraintProto::ConstraintCase::kLinear:
758 fp = FingerprintRepeatedField(ct.linear().vars(), fp);
759 fp = FingerprintRepeatedField(ct.linear().coeffs(), fp);
760 fp = FingerprintRepeatedField(ct.linear().domain(), fp);
761 break;
762 case ConstraintProto::ConstraintCase::kAllDiff:
763 for (const LinearExpressionProto& expr : ct.all_diff().exprs()) {
764 fp = FingerprintExpression(expr, fp);
765 }
766 break;
767 case ConstraintProto::ConstraintCase::kDummyConstraint:
768 break;
769 case ConstraintProto::ConstraintCase::kElement:
770 fp = FingerprintSingleField(ct.element().index(), fp);
771 fp = FingerprintSingleField(ct.element().target(), fp);
772 fp = FingerprintRepeatedField(ct.element().vars(), fp);
773 fp = FingerprintExpression(ct.element().linear_index(), fp);
774 fp = FingerprintExpression(ct.element().linear_target(), fp);
775 for (const LinearExpressionProto& expr : ct.element().exprs()) {
776 fp = FingerprintExpression(expr, fp);
777 }
778 break;
779 case ConstraintProto::ConstraintCase::kCircuit:
780 fp = FingerprintRepeatedField(ct.circuit().heads(), fp);
781 fp = FingerprintRepeatedField(ct.circuit().tails(), fp);
782 fp = FingerprintRepeatedField(ct.circuit().literals(), fp);
783 break;
784 case ConstraintProto::ConstraintCase::kRoutes:
785 fp = FingerprintRepeatedField(ct.routes().heads(), fp);
786 fp = FingerprintRepeatedField(ct.routes().tails(), fp);
787 fp = FingerprintRepeatedField(ct.routes().literals(), fp);
788 break;
789 case ConstraintProto::ConstraintCase::kInverse:
790 fp = FingerprintRepeatedField(ct.inverse().f_direct(), fp);
791 fp = FingerprintRepeatedField(ct.inverse().f_inverse(), fp);
792 break;
793 case ConstraintProto::ConstraintCase::kReservoir:
794 fp = FingerprintSingleField(ct.reservoir().min_level(), fp);
795 fp = FingerprintSingleField(ct.reservoir().max_level(), fp);
796 for (const LinearExpressionProto& expr : ct.reservoir().time_exprs()) {
797 fp = FingerprintExpression(expr, fp);
798 }
799 for (const LinearExpressionProto& expr :
800 ct.reservoir().level_changes()) {
801 fp = FingerprintExpression(expr, fp);
802 }
803 break;
804 case ConstraintProto::ConstraintCase::kTable:
805 if (!ct.table().vars().empty()) {
806 fp = FingerprintRepeatedField(ct.table().vars(), fp);
807 } else {
808 for (const LinearExpressionProto& expr : ct.table().exprs()) {
809 fp = FingerprintExpression(expr, fp);
810 }
811 }
812 fp = FingerprintRepeatedField(ct.table().values(), fp);
813 fp = FingerprintSingleField(ct.table().negated(), fp);
814 break;
815 case ConstraintProto::ConstraintCase::kAutomaton:
816 fp = FingerprintSingleField(ct.automaton().starting_state(), fp);
817 fp = FingerprintRepeatedField(ct.automaton().final_states(), fp);
818 fp = FingerprintRepeatedField(ct.automaton().transition_tail(), fp);
819 fp = FingerprintRepeatedField(ct.automaton().transition_head(), fp);
820 fp = FingerprintRepeatedField(ct.automaton().transition_label(), fp);
821 if (!ct.automaton().vars().empty()) {
822 fp = FingerprintRepeatedField(ct.automaton().vars(), fp);
823 } else {
824 for (const LinearExpressionProto& expr : ct.automaton().exprs()) {
825 fp = FingerprintExpression(expr, fp);
826 }
827 }
828 break;
829 case ConstraintProto::ConstraintCase::kInterval:
830 fp = FingerprintExpression(ct.interval().start(), fp);
831 fp = FingerprintExpression(ct.interval().size(), fp);
832 fp = FingerprintExpression(ct.interval().end(), fp);
833 break;
834 case ConstraintProto::ConstraintCase::kNoOverlap:
835 fp = FingerprintRepeatedField(ct.no_overlap().intervals(), fp);
836 break;
837 case ConstraintProto::ConstraintCase::kNoOverlap2D:
838 fp = FingerprintRepeatedField(ct.no_overlap_2d().x_intervals(), fp);
839 fp = FingerprintRepeatedField(ct.no_overlap_2d().y_intervals(), fp);
840 break;
841 case ConstraintProto::ConstraintCase::kCumulative:
842 fp = FingerprintRepeatedField(ct.cumulative().intervals(), fp);
843 fp = FingerprintExpression(ct.cumulative().capacity(), fp);
844 for (const LinearExpressionProto& demand : ct.cumulative().demands()) {
845 fp = FingerprintExpression(demand, fp);
846 }
847 break;
848 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
849 break;
850 }
851 }
852
853 // Fingerprint the objective.
854 if (model.has_objective()) {
855 fp = FingerprintRepeatedField(model.objective().vars(), fp);
856 fp = FingerprintRepeatedField(model.objective().coeffs(), fp);
857 fp = FingerprintSingleField(model.objective().offset(), fp);
858 fp = FingerprintSingleField(model.objective().scaling_factor(), fp);
859 fp = FingerprintRepeatedField(model.objective().domain(), fp);
860 } else if (model.has_floating_point_objective()) {
861 fp = FingerprintRepeatedField(model.floating_point_objective().vars(), fp);
862 fp =
863 FingerprintRepeatedField(model.floating_point_objective().coeffs(), fp);
864 fp = FingerprintSingleField(model.floating_point_objective().offset(), fp);
865 fp =
866 FingerprintSingleField(model.floating_point_objective().maximize(), fp);
867 }
868
869 if (model.has_solution_hint()) {
870 fp = FingerprintRepeatedField(model.solution_hint().vars(), fp);
871 fp = FingerprintRepeatedField(model.solution_hint().values(), fp);
872 }
873
874 // TODO(user): Should we fingerprint decision strategies?
875
876 return fp;
877}
878
879#if !defined(__PORTABLE_PLATFORM__)
880namespace {
881
882// We need to print " { " instead of " {\n" to inline our variables like:
883//
884// variables { domain: [0, 1] }
885//
886// instead of
887//
888// variables {
889// domain: [0, 1] }
890class InlineFieldPrinter
891 : public google::protobuf::TextFormat::FastFieldValuePrinter {
892 void PrintMessageStart(const google::protobuf::Message& /*message*/,
893 int /*field_index*/, int /*field_count*/,
894 bool /*single_line_mode*/,
895 google::protobuf::TextFormat::BaseTextGenerator*
896 generator) const override {
897 generator->PrintLiteral(" { ");
898 }
899};
900
901class InlineMessagePrinter
902 : public google::protobuf::TextFormat::MessagePrinter {
903 public:
904 InlineMessagePrinter() {
905 printer_.SetSingleLineMode(true);
906 printer_.SetUseShortRepeatedPrimitives(true);
907 }
908
909 void Print(const google::protobuf::Message& message,
910 bool /*single_line_mode*/,
911 google::protobuf::TextFormat::BaseTextGenerator* generator)
912 const override {
913 buffer_.clear();
914 printer_.PrintToString(message, &buffer_);
915 generator->Print(buffer_.data(), buffer_.size());
916 }
917
918 private:
919 google::protobuf::TextFormat::Printer printer_;
920 mutable std::string buffer_;
921};
922
923// Register a InlineFieldPrinter() for all the fields containing the message we
924// want to print in one line.
925void RegisterFieldPrinters(
926 const google::protobuf::Descriptor* descriptor,
927 absl::flat_hash_set<const google::protobuf::Descriptor*>* descriptors,
928 google::protobuf::TextFormat::Printer* printer) {
929 // Recursion stopper.
930 if (!descriptors->insert(descriptor).second) return;
931
932 for (int i = 0; i < descriptor->field_count(); ++i) {
933 const google::protobuf::FieldDescriptor* field = descriptor->field(i);
934 if (field->type() == google::protobuf::FieldDescriptor::TYPE_MESSAGE) {
935 if (field->message_type() == IntegerVariableProto::descriptor() ||
936 field->message_type() == LinearExpressionProto::descriptor()) {
937 printer->RegisterFieldValuePrinter(field, new InlineFieldPrinter());
938 } else {
939 RegisterFieldPrinters(field->message_type(), descriptors, printer);
940 }
941 }
942 }
943}
944
945} // namespace
946
947void SetupTextFormatPrinter(google::protobuf::TextFormat::Printer* printer) {
948 printer->SetUseShortRepeatedPrimitives(true);
949 absl::flat_hash_set<const google::protobuf::Descriptor*> descriptors;
950 RegisterFieldPrinters(CpModelProto::descriptor(), &descriptors, printer);
951 printer->RegisterMessagePrinter(IntegerVariableProto::descriptor(),
952 new InlineMessagePrinter());
953 printer->RegisterMessagePrinter(LinearExpressionProto::descriptor(),
954 new InlineMessagePrinter());
955}
956#endif // !defined(__PORTABLE_PLATFORM__)
957
958bool ConvertCpModelProtoToCnf(const CpModelProto& cp_model, std::string* out) {
959 out->clear();
960
961 // We should have no objective, only unassigned Boolean, and only bool_or and
962 // bool_and.
963 if (cp_model.has_objective()) return false;
964 const int num_vars = cp_model.variables().size();
965 for (int v = 0; v < num_vars; ++v) {
966 if (cp_model.variables(v).domain().size() != 2) return false;
967 if (cp_model.variables(v).domain(0) != 0) return false;
968 if (cp_model.variables(v).domain(1) != 1) return false;
969 }
970 int num_clauses = 0;
971 for (const ConstraintProto& ct : cp_model.constraints()) {
972 if (ct.constraint_case() == ConstraintProto::kBoolOr) {
973 ++num_clauses;
974 } else if (ct.constraint_case() == ConstraintProto::kBoolAnd) {
975 num_clauses += ct.bool_and().literals().size();
976 } else {
977 return false;
978 }
979 }
980
981 // We can convert.
982 std::string start;
983 absl::StrAppend(out, "p cnf ", num_vars, " ", num_clauses, "\n");
984 for (const ConstraintProto& ct : cp_model.constraints()) {
985 if (ct.constraint_case() == ConstraintProto::kBoolOr) {
986 CHECK(ct.enforcement_literal().empty());
987 for (const int lit : ct.bool_or().literals()) {
988 const int value =
989 Literal(BooleanVariable(PositiveRef(lit)), RefIsPositive(lit))
990 .SignedValue();
991 absl::StrAppend(out, value, " ");
992 }
993 absl::StrAppend(out, "0\n");
994 } else if (ct.constraint_case() == ConstraintProto::kBoolAnd) {
995 CHECK(!ct.enforcement_literal().empty());
996 start.clear();
997 for (const int lit : ct.enforcement_literal()) {
998 const int value =
999 Literal(BooleanVariable(PositiveRef(lit)), RefIsPositive(lit))
1000 .SignedValue();
1001 absl::StrAppend(&start, -value, " ");
1002 }
1003 for (const int lit : ct.bool_and().literals()) {
1004 const int value =
1005 Literal(BooleanVariable(PositiveRef(lit)), RefIsPositive(lit))
1006 .SignedValue();
1007 absl::StrAppend(out, start, value, " 0\n");
1008 }
1009 }
1010 }
1011
1012 return true;
1013}
1014
1015int CombineSeed(int base_seed, int64_t delta) {
1016 CHECK_GE(delta, 0);
1017 const uint64_t fp = FingerprintSingleField(delta, kDefaultFingerprintSeed);
1018 return static_cast<int>(FingerprintSingleField(base_seed, fp) & (0x7FFFFFFF));
1019}
1020
1021} // namespace sat
1022} // namespace operations_research
operations_research::Domain
Definition sorted_interval_list.h:87
operations_research::Domain::Max
int64_t Max() const
Definition sorted_interval_list.cc:235
operations_research::Domain::Min
int64_t Min() const
Definition sorted_interval_list.cc:230
operations_research::Domain::AdditionWith
Domain AdditionWith(const Domain &domain) const
Definition sorted_interval_list.cc:439
operations_research::sat::Literal
Definition sat_base.h:66
operations_research::sat::Literal::SignedValue
int SignedValue() const
Definition sat_base.h:94
APPLY_TO_SINGULAR_FIELD
#define APPLY_TO_SINGULAR_FIELD(ct_name, field_name)
Definition cp_model_utils.cc:218
APPLY_TO_REPEATED_FIELD
#define APPLY_TO_REPEATED_FIELD(ct_name, field_name)
Definition cp_model_utils.cc:225
cp_model_utils.h
gtl::STLSortAndRemoveDuplicates
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition stl_util.h:58
operations_research::sat
Definition routing_sat.cc:45
operations_research::sat::SetToNegatedLinearExpression
void SetToNegatedLinearExpression(const LinearExpressionProto &input_expr, LinearExpressionProto *output_negated_expr)
Fills the target as negated ref.
Definition cp_model_utils.cc:71
operations_research::sat::kDefaultFingerprintSeed
constexpr uint64_t kDefaultFingerprintSeed
Default seed for fingerprints.
Definition cp_model_utils.h:286
operations_research::sat::FingerprintRepeatedField
uint64_t FingerprintRepeatedField(const google::protobuf::RepeatedField< T > &sequence, uint64_t seed)
Definition cp_model_utils.h:289
operations_research::sat::RefIsPositive
bool RefIsPositive(int ref)
Definition cp_model_utils.h:46
operations_research::sat::ComputeInnerObjective
int64_t ComputeInnerObjective(const CpObjectiveProto &objective, absl::Span< const int64_t > solution)
Definition cp_model_utils.cc:602
operations_research::sat::CombineSeed
int CombineSeed(int base_seed, int64_t delta)
We assume delta >= 0 and we only use the low bit of delta.
Definition cp_model_utils.cc:1015
operations_research::sat::ApplyToAllIntervalIndices
void ApplyToAllIntervalIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
Definition cp_model_utils.cc:414
operations_research::sat::SafeAddLinearExpressionToLinearConstraint
bool SafeAddLinearExpressionToLinearConstraint(const LinearExpressionProto &expr, int64_t coefficient, LinearConstraintProto *linear)
Same method, but returns if the addition was possible without overflowing.
Definition cp_model_utils.cc:660
operations_research::sat::FingerprintSingleField
uint64_t FingerprintSingleField(const T &field, uint64_t seed)
Definition cp_model_utils.h:297
operations_research::sat::ConvertCpModelProtoToCnf
bool ConvertCpModelProtoToCnf(const CpModelProto &cp_model, std::string *out)
Definition cp_model_utils.cc:958
operations_research::sat::FingerprintExpression
uint64_t FingerprintExpression(const LinearExpressionProto &lin, uint64_t seed)
Returns a stable fingerprint of a linear expression.
Definition cp_model_utils.cc:696
operations_research::sat::FingerprintModel
uint64_t FingerprintModel(const CpModelProto &model, uint64_t seed)
Returns a stable fingerprint of a model.
Definition cp_model_utils.cc:707
operations_research::sat::ExpressionIsAffine
bool ExpressionIsAffine(const LinearExpressionProto &expr)
Checks if the expression is affine or constant.
Definition cp_model_utils.cc:620
operations_research::sat::UsedVariables
std::vector< int > UsedVariables(const ConstraintProto &ct)
Definition cp_model_utils.cc:529
operations_research::sat::UsedIntervals
std::vector< int > UsedIntervals(const ConstraintProto &ct)
Returns the sorted list of interval used by a constraint.
Definition cp_model_utils.cc:542
operations_research::sat::FillDomainInProto
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
Serializes a Domain into the domain field of a proto.
Definition cp_model_utils.h:133
operations_research::sat::i
for i
Definition diophantine.h:100
operations_research::sat::ReadDomainFromProto
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
Definition cp_model_utils.h:144
operations_research::sat::SetupTextFormatPrinter
void SetupTextFormatPrinter(google::protobuf::TextFormat::Printer *printer)
Definition cp_model_utils.cc:947
operations_research::sat::ConstraintCaseName
absl::string_view ConstraintCaseName(ConstraintProto::ConstraintCase constraint_case)
Definition cp_model_utils.cc:475
operations_research::sat::ExpressionContainsSingleRef
bool ExpressionContainsSingleRef(const LinearExpressionProto &expr)
Returns true if a linear expression can be reduced to a single ref.
Definition cp_model_utils.cc:615
operations_research::sat::LinearExpressionGcd
int64_t LinearExpressionGcd(const LinearExpressionProto &expr, int64_t gcd)
Definition cp_model_utils.cc:51
operations_research::sat::ApplyToAllLiteralIndices
void ApplyToAllLiteralIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
Definition cp_model_utils.cc:230
operations_research::sat::PositiveRef
int PositiveRef(int ref)
Definition cp_model_utils.h:45
operations_research::sat::DivideLinearExpression
void DivideLinearExpression(int64_t divisor, LinearExpressionProto *expr)
Definition cp_model_utils.cc:59
operations_research::sat::AddLinearExpressionToLinearConstraint
void AddLinearExpressionToLinearConstraint(const LinearExpressionProto &expr, int64_t coefficient, LinearConstraintProto *linear)
Definition cp_model_utils.cc:631
operations_research::sat::GetSingleRefFromExpression
int GetSingleRefFromExpression(const LinearExpressionProto &expr)
Definition cp_model_utils.cc:626
operations_research::sat::NegatedRef
int NegatedRef(int ref)
Small utility functions to deal with negative variable/literal references.
Definition cp_model_utils.h:44
operations_research::sat::LinearExpressionProtosAreEqual
bool LinearExpressionProtosAreEqual(const LinearExpressionProto &a, const LinearExpressionProto &b, int64_t b_scaling)
Returns true iff a == b * b_scaling.
Definition cp_model_utils.cc:679
operations_research::sat::b
for b[i][j]
Definition diophantine.h:100
operations_research::sat::GetReferencesUsedByConstraint
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto &ct)
Definition cp_model_utils.cc:81
operations_research::sat::ApplyToAllVariableIndices
void ApplyToAllVariableIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
Definition cp_model_utils.cc:293
operations_research::sat::AddWeightedLiteralToLinearConstraint
void AddWeightedLiteralToLinearConstraint(int lit, int64_t coeff, LinearConstraintProto *linear, int64_t *offset)
Definition cp_model_utils.cc:646
operations_research
In SWIG mode, we don't want anything besides these top-level includes.
Definition binary_indexed_tree.h:21
operations_research::AtMinOrMaxInt64
bool AtMinOrMaxInt64(int64_t x)
Checks if x is equal to the min or the max value of an int64_t.
Definition saturated_arithmetic.h:53
operations_research::solution
Select next search node to expand Select next item_i to add this new search node to the search Generate a new search node where item_i is not in the knapsack Check validity of this new partial solution(using propagators) - If valid
operations_research::CapProd
int64_t CapProd(int64_t x, int64_t y)
Definition saturated_arithmetic.h:332
sat_base.h
saturated_arithmetic.h
sorted_interval_list.h
stl_util.h
operations_research::sat::IndexReferences
Definition cp_model_utils.h:72
operations_research::sat::IndexReferences::variables
std::vector< int > variables
Definition cp_model_utils.h:73
operations_research::sat::IndexReferences::literals
std::vector< int > literals
Definition cp_model_utils.h:74