Google OR-Tools v9.14
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
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/flags/flag.h"
27#include "absl/log/check.h"
28#include "absl/strings/str_cat.h"
29#include "absl/strings/string_view.h"
30#include "absl/types/span.h"
31#include "google/protobuf/descriptor.h"
32#include "google/protobuf/message.h"
33#include "google/protobuf/text_format.h"
39
40ABSL_FLAG(bool, cp_model_dump_models, false,
41 "DEBUG ONLY. When set to true, SolveCpModel() will dump its model "
42 "protos (original model, presolved model, mapping model) in text "
43 "format to 'FLAGS_cp_model_dump_prefix'{model|presolved_model|"
44 "mapping_model}.pb.txt.");
45
46#if defined(_MSC_VER)
47ABSL_FLAG(std::string, cp_model_dump_prefix, ".\\",
48 "Prefix filename for all dumped files");
49#else
50ABSL_FLAG(std::string, cp_model_dump_prefix, "/tmp/",
51 "Prefix filename for all dumped files");
52#endif
53
54ABSL_FLAG(bool, cp_model_dump_submodels, false,
55 "DEBUG ONLY. When set to true, solve will dump all "
56 "lns or objective_shaving submodels proto in text format to "
57 "'FLAGS_cp_model_dump_prefix'xxx.pb.txt.");
58
59namespace operations_research {
60namespace sat {
61
62namespace {
63
64template <typename IntList>
65void AddIndices(const IntList& indices, std::vector<int>* output) {
66 output->insert(output->end(), indices.begin(), indices.end());
67}
68
69} // namespace
70
71int64_t LinearExpressionGcd(const LinearExpressionProto& expr, int64_t gcd) {
72 gcd = std::gcd(gcd, std::abs(expr.offset()));
73 for (const int64_t coeff : expr.coeffs()) {
74 gcd = std::gcd(gcd, std::abs(coeff));
75 }
76 return gcd;
77}
78
79void DivideLinearExpression(int64_t divisor, LinearExpressionProto* expr) {
80 CHECK_NE(divisor, 0);
81 if (divisor == 1) return;
82
83 DCHECK_EQ(expr->offset() % divisor, 0);
84 expr->set_offset(expr->offset() / divisor);
85 for (int i = 0; i < expr->vars_size(); ++i) {
86 DCHECK_EQ(expr->coeffs(i) % divisor, 0);
87 expr->set_coeffs(i, expr->coeffs(i) / divisor);
88 }
89}
90
92 LinearExpressionProto* output_negated_expr) {
93 output_negated_expr->Clear();
94 for (int i = 0; i < input_expr.vars_size(); ++i) {
95 output_negated_expr->add_vars(NegatedRef(input_expr.vars(i)));
96 output_negated_expr->add_coeffs(input_expr.coeffs(i));
97 }
98 output_negated_expr->set_offset(-input_expr.offset());
99}
100
102 IndexReferences output;
104 return output;
105}
106
108 std::vector<int>* variables,
109 std::vector<int>* literals) {
110 variables->clear();
111 literals->clear();
112 switch (ct.constraint_case()) {
114 AddIndices(ct.bool_or().literals(), literals);
115 break;
117 AddIndices(ct.bool_and().literals(), literals);
118 break;
120 AddIndices(ct.at_most_one().literals(), literals);
121 break;
123 AddIndices(ct.exactly_one().literals(), literals);
124 break;
126 AddIndices(ct.bool_xor().literals(), literals);
127 break;
129 AddIndices(ct.int_div().target().vars(), variables);
130 for (const LinearExpressionProto& expr : ct.int_div().exprs()) {
131 AddIndices(expr.vars(), variables);
132 }
133 break;
135 AddIndices(ct.int_mod().target().vars(), variables);
136 for (const LinearExpressionProto& expr : ct.int_mod().exprs()) {
137 AddIndices(expr.vars(), variables);
138 }
139 break;
141 AddIndices(ct.lin_max().target().vars(), variables);
142 for (const LinearExpressionProto& expr : ct.lin_max().exprs()) {
143 AddIndices(expr.vars(), variables);
144 }
145 break;
146 }
148 AddIndices(ct.int_prod().target().vars(), variables);
149 for (const LinearExpressionProto& expr : ct.int_prod().exprs()) {
150 AddIndices(expr.vars(), variables);
151 }
152 break;
154 AddIndices(ct.linear().vars(), variables);
155 break;
157 for (const LinearExpressionProto& expr : ct.all_diff().exprs()) {
158 AddIndices(expr.vars(), variables);
159 }
160 break;
162 AddIndices(ct.dummy_constraint().vars(), variables);
163 break;
165 if (ct.element().index() != 0 || ct.element().target() != 0 ||
166 !ct.element().vars().empty()) {
167 variables->push_back(ct.element().index());
168 variables->push_back(ct.element().target());
169 AddIndices(ct.element().vars(), variables);
170 } else if (ct.element().has_linear_index() ||
171 ct.element().has_linear_target() ||
172 !ct.element().exprs().empty()) {
173 AddIndices(ct.element().linear_index().vars(), variables);
174 AddIndices(ct.element().linear_target().vars(), variables);
175 for (const LinearExpressionProto& expr : ct.element().exprs()) {
176 AddIndices(expr.vars(), variables);
177 }
178 }
179 break;
181 AddIndices(ct.circuit().literals(), literals);
182 break;
184 AddIndices(ct.routes().literals(), literals);
185 // The node expressions are not used by the constraint itself.
186 break;
188 AddIndices(ct.inverse().f_direct(), variables);
189 AddIndices(ct.inverse().f_inverse(), variables);
190 break;
192 for (const LinearExpressionProto& time : ct.reservoir().time_exprs()) {
193 AddIndices(time.vars(), variables);
194 }
195 for (const LinearExpressionProto& level :
196 ct.reservoir().level_changes()) {
197 AddIndices(level.vars(), variables);
198 }
199 AddIndices(ct.reservoir().active_literals(), literals);
200 break;
202 if (!ct.table().vars().empty()) {
203 AddIndices(ct.table().vars(), variables);
204 } else {
205 for (const LinearExpressionProto& expr : ct.table().exprs()) {
206 AddIndices(expr.vars(), variables);
207 }
208 }
209 break;
211 if (!ct.automaton().vars().empty()) {
212 AddIndices(ct.automaton().vars(), variables);
213 } else {
214 for (const LinearExpressionProto& expr : ct.automaton().exprs()) {
215 AddIndices(expr.vars(), variables);
216 }
217 }
218 break;
220 AddIndices(ct.interval().start().vars(), variables);
221 AddIndices(ct.interval().size().vars(), variables);
222 AddIndices(ct.interval().end().vars(), variables);
223 break;
225 break;
227 break;
229 AddIndices(ct.cumulative().capacity().vars(), variables);
230 for (const LinearExpressionProto& demand : ct.cumulative().demands()) {
231 AddIndices(demand.vars(), variables);
232 }
233 break;
235 break;
236 }
237}
238
239#define APPLY_TO_SINGULAR_FIELD(ct_name, field_name) \
240 { \
241 int temp = ct->mutable_##ct_name()->field_name(); \
242 f(&temp); \
243 ct->mutable_##ct_name()->set_##field_name(temp); \
244 }
245
246#define APPLY_TO_REPEATED_FIELD(ct_name, field_name) \
247 { \
248 for (int& r : *ct->mutable_##ct_name()->mutable_##field_name()) f(&r); \
249 }
250
251void ApplyToAllLiteralIndices(const std::function<void(int*)>& f,
252 ConstraintProto* ct) {
253 for (int& r : *ct->mutable_enforcement_literal()) f(&r);
254 switch (ct->constraint_case()) {
256 APPLY_TO_REPEATED_FIELD(bool_or, literals);
257 break;
259 APPLY_TO_REPEATED_FIELD(bool_and, literals);
260 break;
262 APPLY_TO_REPEATED_FIELD(at_most_one, literals);
263 break;
265 APPLY_TO_REPEATED_FIELD(exactly_one, literals);
266 break;
268 APPLY_TO_REPEATED_FIELD(bool_xor, literals);
269 break;
271 break;
273 break;
275 break;
277 break;
279 break;
281 break;
283 break;
285 break;
287 APPLY_TO_REPEATED_FIELD(circuit, literals);
288 break;
290 APPLY_TO_REPEATED_FIELD(routes, literals);
291 break;
293 break;
295 APPLY_TO_REPEATED_FIELD(reservoir, active_literals);
296 break;
298 break;
300 break;
302 break;
304 break;
306 break;
308 break;
310 break;
311 }
312}
313
314void ApplyToAllVariableIndices(const std::function<void(int*)>& f,
315 ConstraintProto* ct) {
316 switch (ct->constraint_case()) {
318 break;
320 break;
322 break;
324 break;
326 break;
328 APPLY_TO_REPEATED_FIELD(int_div, target()->mutable_vars);
329 for (int i = 0; i < ct->int_div().exprs_size(); ++i) {
330 APPLY_TO_REPEATED_FIELD(int_div, exprs(i)->mutable_vars);
331 }
332 break;
334 APPLY_TO_REPEATED_FIELD(int_mod, target()->mutable_vars);
335 for (int i = 0; i < ct->int_mod().exprs_size(); ++i) {
336 APPLY_TO_REPEATED_FIELD(int_mod, exprs(i)->mutable_vars);
337 }
338 break;
340 APPLY_TO_REPEATED_FIELD(lin_max, target()->mutable_vars);
341 for (int i = 0; i < ct->lin_max().exprs_size(); ++i) {
342 APPLY_TO_REPEATED_FIELD(lin_max, exprs(i)->mutable_vars);
343 }
344 break;
346 APPLY_TO_REPEATED_FIELD(int_prod, target()->mutable_vars);
347 for (int i = 0; i < ct->int_prod().exprs_size(); ++i) {
348 APPLY_TO_REPEATED_FIELD(int_prod, exprs(i)->mutable_vars);
349 }
350 break;
352 APPLY_TO_REPEATED_FIELD(linear, vars);
353 break;
355 for (int i = 0; i < ct->all_diff().exprs_size(); ++i) {
356 APPLY_TO_REPEATED_FIELD(all_diff, exprs(i)->mutable_vars);
357 }
358 break;
360 APPLY_TO_REPEATED_FIELD(dummy_constraint, vars);
361 break;
363 if (ct->element().index() != 0 || ct->element().target() != 0 ||
364 !ct->element().vars().empty()) {
365 APPLY_TO_SINGULAR_FIELD(element, index);
366 APPLY_TO_SINGULAR_FIELD(element, target);
367 APPLY_TO_REPEATED_FIELD(element, vars);
368 } else if (ct->element().has_linear_index() ||
369 ct->element().has_linear_target() ||
370 !ct->element().exprs().empty()) {
371 APPLY_TO_REPEATED_FIELD(element, linear_index()->mutable_vars);
372 APPLY_TO_REPEATED_FIELD(element, linear_target()->mutable_vars);
373 for (int i = 0; i < ct->element().exprs_size(); ++i) {
374 APPLY_TO_REPEATED_FIELD(element, exprs(i)->mutable_vars);
375 }
376 }
377 break;
379 break;
381 break;
383 APPLY_TO_REPEATED_FIELD(inverse, f_direct);
384 APPLY_TO_REPEATED_FIELD(inverse, f_inverse);
385 break;
387 for (int i = 0; i < ct->reservoir().time_exprs_size(); ++i) {
388 APPLY_TO_REPEATED_FIELD(reservoir, time_exprs(i)->mutable_vars);
389 }
390 for (int i = 0; i < ct->reservoir().level_changes_size(); ++i) {
391 APPLY_TO_REPEATED_FIELD(reservoir, level_changes(i)->mutable_vars);
392 }
393 break;
395 if (!ct->table().vars().empty()) {
396 APPLY_TO_REPEATED_FIELD(table, vars);
397 } else {
398 for (int i = 0; i < ct->table().exprs_size(); ++i) {
399 APPLY_TO_REPEATED_FIELD(table, exprs(i)->mutable_vars);
400 }
401 }
402 break;
404 if (!ct->automaton().vars().empty()) {
405 APPLY_TO_REPEATED_FIELD(automaton, vars);
406 } else {
407 for (int i = 0; i < ct->automaton().exprs_size(); ++i) {
408 APPLY_TO_REPEATED_FIELD(automaton, exprs(i)->mutable_vars);
409 }
410 }
411 break;
413 APPLY_TO_REPEATED_FIELD(interval, start()->mutable_vars);
414 APPLY_TO_REPEATED_FIELD(interval, size()->mutable_vars);
415 APPLY_TO_REPEATED_FIELD(interval, end()->mutable_vars);
416 break;
418 break;
420 break;
422 APPLY_TO_REPEATED_FIELD(cumulative, capacity()->mutable_vars);
423 for (int i = 0; i < ct->cumulative().demands_size(); ++i) {
424 for (int& r :
426 f(&r);
427 }
428 }
429 break;
431 break;
432 }
433}
434
435void ApplyToAllIntervalIndices(const std::function<void(int*)>& f,
436 ConstraintProto* ct) {
437 switch (ct->constraint_case()) {
439 break;
441 break;
443 break;
445 break;
447 break;
449 break;
451 break;
453 break;
455 break;
457 break;
459 break;
461 break;
463 break;
465 break;
467 break;
469 break;
471 break;
473 break;
475 break;
477 break;
479 APPLY_TO_REPEATED_FIELD(no_overlap, intervals);
480 break;
482 APPLY_TO_REPEATED_FIELD(no_overlap_2d, x_intervals);
483 APPLY_TO_REPEATED_FIELD(no_overlap_2d, y_intervals);
484 break;
486 APPLY_TO_REPEATED_FIELD(cumulative, intervals);
487 break;
489 break;
490 }
491}
492
493#undef APPLY_TO_SINGULAR_FIELD
494#undef APPLY_TO_REPEATED_FIELD
495
496absl::string_view ConstraintCaseName(
497 ConstraintProto::ConstraintCase constraint_case) {
498 switch (constraint_case) {
500 return "kBoolOr";
502 return "kBoolAnd";
504 return "kAtMostOne";
506 return "kExactlyOne";
508 return "kBoolXor";
510 return "kIntDiv";
512 return "kIntMod";
514 return "kLinMax";
516 return "kIntProd";
518 return "kLinear";
520 return "kAllDiff";
522 return "kDummyConstraint";
524 return "kElement";
526 return "kCircuit";
528 return "kRoutes";
530 return "kInverse";
532 return "kReservoir";
534 return "kTable";
536 return "kAutomaton";
538 return "kInterval";
540 return "kNoOverlap";
542 return "kNoOverlap2D";
544 return "kCumulative";
546 return "kEmpty";
547 }
548}
549
550std::vector<int> UsedVariables(const ConstraintProto& ct) {
551 std::vector<int> result;
552 GetReferencesUsedByConstraint(ct, &result, &result);
553 for (int& ref : result) {
554 ref = PositiveRef(ref);
555 }
556 for (const int lit : ct.enforcement_literal()) {
557 result.push_back(PositiveRef(lit));
558 }
560 return result;
561}
562
563std::vector<int> UsedIntervals(const ConstraintProto& ct) {
564 std::vector<int> used_intervals;
565 switch (ct.constraint_case()) {
567 break;
569 break;
571 break;
573 break;
575 break;
577 break;
579 break;
581 break;
583 break;
585 break;
587 break;
589 break;
591 break;
593 break;
595 break;
597 break;
599 break;
601 break;
603 break;
605 break;
607 AddIndices(ct.no_overlap().intervals(), &used_intervals);
608 break;
610 AddIndices(ct.no_overlap_2d().x_intervals(), &used_intervals);
611 AddIndices(ct.no_overlap_2d().y_intervals(), &used_intervals);
612 break;
614 AddIndices(ct.cumulative().intervals(), &used_intervals);
615 break;
617 break;
618 }
619 gtl::STLSortAndRemoveDuplicates(&used_intervals);
620 return used_intervals;
621}
622
624 absl::Span<const int64_t> solution) {
625 int64_t objective_value = 0;
626 for (int i = 0; i < objective.vars_size(); ++i) {
627 int64_t coeff = objective.coeffs(i);
628 const int ref = objective.vars(i);
629 const int var = PositiveRef(ref);
630 if (!RefIsPositive(ref)) coeff = -coeff;
631 objective_value += coeff * solution[var];
632 }
633 return objective_value;
634}
635
637 return expr.offset() == 0 && expr.vars_size() == 1 &&
638 std::abs(expr.coeffs(0)) == 1;
639}
640
642 return expr.vars_size() <= 1;
643}
644
645// Returns the reference the expression can be reduced to. It will DCHECK that
646// ExpressionContainsSingleRef(expr) is true.
648 DCHECK(ExpressionContainsSingleRef(expr));
649 return expr.coeffs(0) == 1 ? expr.vars(0) : NegatedRef(expr.vars(0));
650}
651
653 int64_t coefficient,
654 LinearConstraintProto* linear) {
655 for (int i = 0; i < expr.vars_size(); ++i) {
656 linear->add_vars(expr.vars(i));
657 linear->add_coeffs(expr.coeffs(i) * coefficient);
658 }
659 DCHECK(!linear->domain().empty());
660 const int64_t shift = coefficient * expr.offset();
661 if (shift != 0) {
663 linear);
664 }
665}
666
667void AddWeightedLiteralToLinearConstraint(int lit, int64_t coeff,
668 LinearConstraintProto* linear,
669 int64_t* offset) {
670 if (coeff == 0) return;
671 if (RefIsPositive(lit)) {
672 linear->add_vars(lit);
673 linear->add_coeffs(coeff);
674 } else {
675 linear->add_vars(NegatedRef(lit));
676 linear->add_coeffs(-coeff);
677 *offset += coeff;
678 }
679}
680
682 const LinearExpressionProto& expr, int64_t coefficient,
683 LinearConstraintProto* linear) {
684 for (int i = 0; i < expr.vars_size(); ++i) {
685 linear->add_vars(expr.vars(i));
686 const int64_t prod = CapProd(expr.coeffs(i), coefficient);
687 if (AtMinOrMaxInt64(prod)) return false;
688 linear->add_coeffs(prod);
689 }
690 DCHECK(!linear->domain().empty());
691
692 const int64_t shift = CapProd(coefficient, expr.offset());
693 if (AtMinOrMaxInt64(shift)) return false;
694 Domain d = ReadDomainFromProto(*linear).AdditionWith(Domain(-shift));
695 if (AtMinOrMaxInt64(d.Min()) || AtMinOrMaxInt64(d.Max())) return false;
696 FillDomainInProto(d, linear);
697 return true;
698}
699
702 int64_t b_scaling) {
703 if (a.vars_size() != b.vars_size()) return false;
704 if (a.offset() != b.offset() * b_scaling) return false;
705 absl::flat_hash_map<int, int64_t> coeffs;
706 for (int i = 0; i < a.vars_size(); ++i) {
707 coeffs[a.vars(i)] += a.coeffs(i);
708 coeffs[b.vars(i)] += -b.coeffs(i) * b_scaling;
709 }
710
711 for (const auto [var, coeff] : coeffs) {
712 if (coeff != 0) return false;
713 }
714 return true;
715}
716
718 uint64_t seed) {
719 uint64_t fp = seed;
720 if (!lin.vars().empty()) {
721 fp = FingerprintRepeatedField(lin.vars(), fp);
722 fp = FingerprintRepeatedField(lin.coeffs(), fp);
723 }
724 fp = FingerprintSingleField(lin.offset(), fp);
725 return fp;
726}
727
728uint64_t FingerprintModel(const CpModelProto& model, uint64_t seed) {
729 uint64_t fp = seed;
730 for (const IntegerVariableProto& var_proto : model.variables()) {
731 fp = FingerprintRepeatedField(var_proto.domain(), fp);
732 }
733 for (const ConstraintProto& ct : model.constraints()) {
734 if (!ct.enforcement_literal().empty()) {
735 fp = FingerprintRepeatedField(ct.enforcement_literal(), fp);
736 }
737 switch (ct.constraint_case()) {
739 fp = FingerprintRepeatedField(ct.bool_or().literals(), fp);
740 break;
742 fp = FingerprintRepeatedField(ct.bool_and().literals(), fp);
743 break;
745 fp = FingerprintRepeatedField(ct.at_most_one().literals(), fp);
746 break;
748 fp = FingerprintRepeatedField(ct.exactly_one().literals(), fp);
749 break;
751 fp = FingerprintRepeatedField(ct.bool_xor().literals(), fp);
752 break;
754 fp = FingerprintExpression(ct.int_div().target(), fp);
755 for (const LinearExpressionProto& expr : ct.int_div().exprs()) {
756 fp = FingerprintExpression(expr, fp);
757 }
758 break;
760 fp = FingerprintExpression(ct.int_mod().target(), fp);
761 for (const LinearExpressionProto& expr : ct.int_mod().exprs()) {
762 fp = FingerprintExpression(expr, fp);
763 }
764 break;
766 fp = FingerprintExpression(ct.lin_max().target(), fp);
767 for (const LinearExpressionProto& expr : ct.lin_max().exprs()) {
768 fp = FingerprintExpression(expr, fp);
769 }
770 break;
771 }
773 fp = FingerprintExpression(ct.int_prod().target(), fp);
774 for (const LinearExpressionProto& expr : ct.int_prod().exprs()) {
775 fp = FingerprintExpression(expr, fp);
776 }
777 break;
779 fp = FingerprintRepeatedField(ct.linear().vars(), fp);
780 fp = FingerprintRepeatedField(ct.linear().coeffs(), fp);
781 fp = FingerprintRepeatedField(ct.linear().domain(), fp);
782 break;
784 for (const LinearExpressionProto& expr : ct.all_diff().exprs()) {
785 fp = FingerprintExpression(expr, fp);
786 }
787 break;
789 break;
791 fp = FingerprintSingleField(ct.element().index(), fp);
792 fp = FingerprintSingleField(ct.element().target(), fp);
793 fp = FingerprintRepeatedField(ct.element().vars(), fp);
794 fp = FingerprintExpression(ct.element().linear_index(), fp);
795 fp = FingerprintExpression(ct.element().linear_target(), fp);
796 for (const LinearExpressionProto& expr : ct.element().exprs()) {
797 fp = FingerprintExpression(expr, fp);
798 }
799 break;
801 fp = FingerprintRepeatedField(ct.circuit().heads(), fp);
802 fp = FingerprintRepeatedField(ct.circuit().tails(), fp);
803 fp = FingerprintRepeatedField(ct.circuit().literals(), fp);
804 break;
806 fp = FingerprintRepeatedField(ct.routes().heads(), fp);
807 fp = FingerprintRepeatedField(ct.routes().tails(), fp);
808 fp = FingerprintRepeatedField(ct.routes().literals(), fp);
809 break;
811 fp = FingerprintRepeatedField(ct.inverse().f_direct(), fp);
812 fp = FingerprintRepeatedField(ct.inverse().f_inverse(), fp);
813 break;
815 fp = FingerprintSingleField(ct.reservoir().min_level(), fp);
816 fp = FingerprintSingleField(ct.reservoir().max_level(), fp);
817 for (const LinearExpressionProto& expr : ct.reservoir().time_exprs()) {
818 fp = FingerprintExpression(expr, fp);
819 }
820 for (const LinearExpressionProto& expr :
821 ct.reservoir().level_changes()) {
822 fp = FingerprintExpression(expr, fp);
823 }
824 break;
826 if (!ct.table().vars().empty()) {
827 fp = FingerprintRepeatedField(ct.table().vars(), fp);
828 } else {
829 for (const LinearExpressionProto& expr : ct.table().exprs()) {
830 fp = FingerprintExpression(expr, fp);
831 }
832 }
833 fp = FingerprintRepeatedField(ct.table().values(), fp);
834 fp = FingerprintSingleField(ct.table().negated(), fp);
835 break;
837 fp = FingerprintSingleField(ct.automaton().starting_state(), fp);
838 fp = FingerprintRepeatedField(ct.automaton().final_states(), fp);
839 fp = FingerprintRepeatedField(ct.automaton().transition_tail(), fp);
840 fp = FingerprintRepeatedField(ct.automaton().transition_head(), fp);
841 fp = FingerprintRepeatedField(ct.automaton().transition_label(), fp);
842 if (!ct.automaton().vars().empty()) {
843 fp = FingerprintRepeatedField(ct.automaton().vars(), fp);
844 } else {
845 for (const LinearExpressionProto& expr : ct.automaton().exprs()) {
846 fp = FingerprintExpression(expr, fp);
847 }
848 }
849 break;
851 fp = FingerprintExpression(ct.interval().start(), fp);
852 fp = FingerprintExpression(ct.interval().size(), fp);
853 fp = FingerprintExpression(ct.interval().end(), fp);
854 break;
856 fp = FingerprintRepeatedField(ct.no_overlap().intervals(), fp);
857 break;
859 fp = FingerprintRepeatedField(ct.no_overlap_2d().x_intervals(), fp);
860 fp = FingerprintRepeatedField(ct.no_overlap_2d().y_intervals(), fp);
861 break;
863 fp = FingerprintRepeatedField(ct.cumulative().intervals(), fp);
864 fp = FingerprintExpression(ct.cumulative().capacity(), fp);
865 for (const LinearExpressionProto& demand : ct.cumulative().demands()) {
866 fp = FingerprintExpression(demand, fp);
867 }
868 break;
870 break;
871 }
872 }
873
874 // Fingerprint the objective.
875 if (model.has_objective()) {
876 fp = FingerprintRepeatedField(model.objective().vars(), fp);
877 fp = FingerprintRepeatedField(model.objective().coeffs(), fp);
878 fp = FingerprintSingleField(model.objective().offset(), fp);
880 fp = FingerprintRepeatedField(model.objective().domain(), fp);
881 } else if (model.has_floating_point_objective()) {
883 fp =
886 fp =
888 }
889
890 if (model.has_solution_hint()) {
891 fp = FingerprintRepeatedField(model.solution_hint().vars(), fp);
893 }
894
895 // TODO(user): Should we fingerprint decision strategies?
896
897 return fp;
898}
899
900#if !defined(__PORTABLE_PLATFORM__)
901namespace {
902
903// We need to print " { " instead of " {\n" to inline our variables like:
904//
905// variables { domain: [0, 1] }
906//
907// instead of
908//
909// variables {
910// domain: [0, 1] }
911class InlineFieldPrinter
912 : public google::protobuf::TextFormat::FastFieldValuePrinter {
913 void PrintMessageStart(const google::protobuf::Message& /*message*/,
914 int /*field_index*/, int /*field_count*/,
915 bool /*single_line_mode*/,
916 google::protobuf::TextFormat::BaseTextGenerator*
917 generator) const override {
918 generator->PrintLiteral(" { ");
919 }
920};
921
922class InlineMessagePrinter
923 : public google::protobuf::TextFormat::MessagePrinter {
924 public:
925 InlineMessagePrinter() {
926 printer_.SetSingleLineMode(true);
927 printer_.SetUseShortRepeatedPrimitives(true);
928 }
929
930 void Print(const google::protobuf::Message& message,
931 bool /*single_line_mode*/,
932 google::protobuf::TextFormat::BaseTextGenerator* generator)
933 const override {
934 buffer_.clear();
935 printer_.PrintToString(message, &buffer_);
936 generator->Print(buffer_.data(), buffer_.size());
937 }
938
939 private:
940 google::protobuf::TextFormat::Printer printer_;
941 mutable std::string buffer_;
942};
943
944// Register a InlineFieldPrinter() for all the fields containing the message we
945// want to print in one line.
946void RegisterFieldPrinters(
947 const google::protobuf::Descriptor* descriptor,
948 absl::flat_hash_set<const google::protobuf::Descriptor*>* descriptors,
949 google::protobuf::TextFormat::Printer* printer) {
950 // Recursion stopper.
951 if (!descriptors->insert(descriptor).second) return;
952
953 for (int i = 0; i < descriptor->field_count(); ++i) {
954 const google::protobuf::FieldDescriptor* field = descriptor->field(i);
955 if (field->type() == google::protobuf::FieldDescriptor::TYPE_MESSAGE) {
956 if (field->message_type() == IntegerVariableProto::descriptor() ||
957 field->message_type() == LinearExpressionProto::descriptor()) {
958 printer->RegisterFieldValuePrinter(field, new InlineFieldPrinter());
959 } else {
960 RegisterFieldPrinters(field->message_type(), descriptors, printer);
961 }
962 }
963 }
964}
965
966} // namespace
967
968void SetupTextFormatPrinter(google::protobuf::TextFormat::Printer* printer) {
969 printer->SetUseShortRepeatedPrimitives(true);
970 absl::flat_hash_set<const google::protobuf::Descriptor*> descriptors;
971 RegisterFieldPrinters(CpModelProto::descriptor(), &descriptors, printer);
972 printer->RegisterMessagePrinter(IntegerVariableProto::descriptor(),
973 new InlineMessagePrinter());
974 printer->RegisterMessagePrinter(LinearExpressionProto::descriptor(),
975 new InlineMessagePrinter());
976}
977#endif // !defined(__PORTABLE_PLATFORM__)
978
979bool ConvertCpModelProtoToCnf(const CpModelProto& cp_model, std::string* out) {
980 out->clear();
981
982 // We should have no objective, only unassigned Boolean, and only bool_or and
983 // bool_and.
984 if (cp_model.has_objective()) return false;
985 const int num_vars = cp_model.variables().size();
986 for (int v = 0; v < num_vars; ++v) {
987 if (cp_model.variables(v).domain().size() != 2) return false;
988 if (cp_model.variables(v).domain(0) != 0) return false;
989 if (cp_model.variables(v).domain(1) != 1) return false;
990 }
991 int num_clauses = 0;
992 for (const ConstraintProto& ct : cp_model.constraints()) {
993 if (ct.constraint_case() == ConstraintProto::kBoolOr) {
994 ++num_clauses;
995 } else if (ct.constraint_case() == ConstraintProto::kBoolAnd) {
996 num_clauses += ct.bool_and().literals().size();
997 } else {
998 return false;
999 }
1000 }
1001
1002 // We can convert.
1003 std::string start;
1004 absl::StrAppend(out, "p cnf ", num_vars, " ", num_clauses, "\n");
1005 for (const ConstraintProto& ct : cp_model.constraints()) {
1006 if (ct.constraint_case() == ConstraintProto::kBoolOr) {
1007 CHECK(ct.enforcement_literal().empty());
1008 for (const int lit : ct.bool_or().literals()) {
1009 const int value =
1010 Literal(BooleanVariable(PositiveRef(lit)), RefIsPositive(lit))
1011 .SignedValue();
1012 absl::StrAppend(out, value, " ");
1013 }
1014 absl::StrAppend(out, "0\n");
1015 } else if (ct.constraint_case() == ConstraintProto::kBoolAnd) {
1016 CHECK(!ct.enforcement_literal().empty());
1017 start.clear();
1018 for (const int lit : ct.enforcement_literal()) {
1019 const int value =
1020 Literal(BooleanVariable(PositiveRef(lit)), RefIsPositive(lit))
1021 .SignedValue();
1022 absl::StrAppend(&start, -value, " ");
1023 }
1024 for (const int lit : ct.bool_and().literals()) {
1025 const int value =
1026 Literal(BooleanVariable(PositiveRef(lit)), RefIsPositive(lit))
1027 .SignedValue();
1028 absl::StrAppend(out, start, value, " 0\n");
1029 }
1030 }
1031 }
1032
1033 return true;
1034}
1035
1036int CombineSeed(int base_seed, int64_t delta) {
1037 CHECK_GE(delta, 0);
1038 const uint64_t fp = FingerprintSingleField(delta, kDefaultFingerprintSeed);
1039 return static_cast<int>(FingerprintSingleField(base_seed, fp) & (0x7FFFFFFF));
1040}
1041
1042} // namespace sat
1043} // namespace operations_research
Domain AdditionWith(const Domain &domain) const
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
const ::operations_research::sat::TableConstraintProto & table() const
const ::operations_research::sat::BoolArgumentProto & bool_xor() const
const ::operations_research::sat::InverseConstraintProto & inverse() const
::operations_research::sat::CumulativeConstraintProto *PROTOBUF_NONNULL mutable_cumulative()
::int32_t enforcement_literal(int index) const
const ::operations_research::sat::BoolArgumentProto & exactly_one() const
const ::operations_research::sat::NoOverlapConstraintProto & no_overlap() const
const ::operations_research::sat::ListOfVariablesProto & dummy_constraint() const
const ::operations_research::sat::AllDifferentConstraintProto & all_diff() const
const ::operations_research::sat::LinearConstraintProto & linear() const
const ::operations_research::sat::BoolArgumentProto & at_most_one() const
const ::operations_research::sat::IntervalConstraintProto & interval() const
const ::operations_research::sat::RoutesConstraintProto & routes() const
const ::operations_research::sat::LinearArgumentProto & lin_max() const
const ::operations_research::sat::ElementConstraintProto & element() const
const ::operations_research::sat::BoolArgumentProto & bool_and() const
const ::operations_research::sat::BoolArgumentProto & bool_or() const
const ::operations_research::sat::LinearArgumentProto & int_mod() const
::google::protobuf::RepeatedField<::int32_t > *PROTOBUF_NONNULL mutable_enforcement_literal()
const ::operations_research::sat::LinearArgumentProto & int_prod() const
const ::operations_research::sat::LinearArgumentProto & int_div() const
const ::operations_research::sat::AutomatonConstraintProto & automaton() const
const ::operations_research::sat::CircuitConstraintProto & circuit() const
const ::operations_research::sat::CumulativeConstraintProto & cumulative() const
const ::operations_research::sat::ReservoirConstraintProto & reservoir() const
const ::operations_research::sat::NoOverlap2DConstraintProto & no_overlap_2d() const
bool has_solution_hint() const
.operations_research.sat.PartialVariableAssignment solution_hint = 6;
bool has_floating_point_objective() const
.operations_research.sat.FloatObjectiveProto floating_point_objective = 9;
static const ::google::protobuf::Descriptor *PROTOBUF_NONNULL descriptor()
const ::operations_research::sat::IntegerVariableProto & variables(int index) const
const ::operations_research::sat::FloatObjectiveProto & floating_point_objective() const
const ::operations_research::sat::ConstraintProto & constraints(int index) const
bool has_objective() const
.operations_research.sat.CpObjectiveProto objective = 4;
const ::operations_research::sat::PartialVariableAssignment & solution_hint() const
const ::operations_research::sat::CpObjectiveProto & objective() const
int vars_size() const
repeated int32 vars = 1;
const ::operations_research::sat::LinearExpressionProto & demands(int index) const
::operations_research::sat::LinearExpressionProto *PROTOBUF_NONNULL mutable_demands(int index)
const ::operations_research::sat::LinearExpressionProto & capacity() const
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
const ::operations_research::sat::LinearExpressionProto & linear_target() const
bool has_linear_index() const
.operations_research.sat.LinearExpressionProto linear_index = 4;
bool has_linear_target() const
.operations_research.sat.LinearExpressionProto linear_target = 5;
const ::operations_research::sat::LinearExpressionProto & linear_index() const
static const ::google::protobuf::Descriptor *PROTOBUF_NONNULL descriptor()
const ::operations_research::sat::LinearExpressionProto & size() const
const ::operations_research::sat::LinearExpressionProto & end() const
const ::operations_research::sat::LinearExpressionProto & start() const
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
const ::operations_research::sat::LinearExpressionProto & target() const
ABSL_ATTRIBUTE_REINITIALIZES void Clear() PROTOBUF_FINAL
::google::protobuf::RepeatedField<::int32_t > *PROTOBUF_NONNULL mutable_vars()
void set_coeffs(int index, ::int64_t value)
static const ::google::protobuf::Descriptor *PROTOBUF_NONNULL descriptor()
int vars_size() const
repeated int32 vars = 1;
const ::operations_research::sat::LinearExpressionProto & time_exprs(int index) const
const ::operations_research::sat::LinearExpressionProto & level_changes(int index) const
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
#define APPLY_TO_SINGULAR_FIELD(ct_name, field_name)
ABSL_FLAG(bool, cp_model_dump_models, false, "DEBUG ONLY. When set to true, SolveCpModel() will dump its model " "protos (original model, presolved model, mapping model) in text " "format to 'FLAGS_cp_model_dump_prefix'{model|presolved_model|" "mapping_model}.pb.txt.")
#define APPLY_TO_REPEATED_FIELD(ct_name, field_name)
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition stl_util.h:55
void SetToNegatedLinearExpression(const LinearExpressionProto &input_expr, LinearExpressionProto *output_negated_expr)
Fills the target as negated ref.
constexpr uint64_t kDefaultFingerprintSeed
Default seed for fingerprints.
uint64_t FingerprintRepeatedField(const google::protobuf::RepeatedField< T > &sequence, uint64_t seed)
int64_t ComputeInnerObjective(const CpObjectiveProto &objective, absl::Span< const int64_t > solution)
int CombineSeed(int base_seed, int64_t delta)
We assume delta >= 0 and we only use the low bit of delta.
void ApplyToAllIntervalIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
bool SafeAddLinearExpressionToLinearConstraint(const LinearExpressionProto &expr, int64_t coefficient, LinearConstraintProto *linear)
Same method, but returns if the addition was possible without overflowing.
uint64_t FingerprintSingleField(const T &field, uint64_t seed)
bool ConvertCpModelProtoToCnf(const CpModelProto &cp_model, std::string *out)
uint64_t FingerprintExpression(const LinearExpressionProto &lin, uint64_t seed)
Returns a stable fingerprint of a linear expression.
uint64_t FingerprintModel(const CpModelProto &model, uint64_t seed)
Returns a stable fingerprint of a model.
bool ExpressionIsAffine(const LinearExpressionProto &expr)
Checks if the expression is affine or constant.
std::vector< int > UsedVariables(const ConstraintProto &ct)
std::vector< int > UsedIntervals(const ConstraintProto &ct)
Returns the sorted list of interval used by a constraint.
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
Serializes a Domain into the domain field of a proto.
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
void SetupTextFormatPrinter(google::protobuf::TextFormat::Printer *printer)
absl::string_view ConstraintCaseName(ConstraintProto::ConstraintCase constraint_case)
bool ExpressionContainsSingleRef(const LinearExpressionProto &expr)
Returns true if a linear expression can be reduced to a single ref.
int64_t LinearExpressionGcd(const LinearExpressionProto &expr, int64_t gcd)
void ApplyToAllLiteralIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
void DivideLinearExpression(int64_t divisor, LinearExpressionProto *expr)
void AddLinearExpressionToLinearConstraint(const LinearExpressionProto &expr, int64_t coefficient, LinearConstraintProto *linear)
int GetSingleRefFromExpression(const LinearExpressionProto &expr)
int NegatedRef(int ref)
Small utility functions to deal with negative variable/literal references.
bool LinearExpressionProtosAreEqual(const LinearExpressionProto &a, const LinearExpressionProto &b, int64_t b_scaling)
Returns true iff a == b * b_scaling.
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto &ct)
void ApplyToAllVariableIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
void AddWeightedLiteralToLinearConstraint(int lit, int64_t coeff, LinearConstraintProto *linear, int64_t *offset)
In SWIG mode, we don't want anything besides these top-level includes.
bool AtMinOrMaxInt64(int64_t x)
Checks if x is equal to the min or the max value of an int64_t.
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
ClosedInterval::Iterator end(ClosedInterval interval)
int64_t CapProd(int64_t x, int64_t y)