Google OR-Tools v9.11
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-2024 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 variables->push_back(ct.element().index());
146 variables->push_back(ct.element().target());
147 AddIndices(ct.element().vars(), variables);
148 break;
149 case ConstraintProto::ConstraintCase::kCircuit:
150 AddIndices(ct.circuit().literals(), literals);
151 break;
152 case ConstraintProto::ConstraintCase::kRoutes:
153 AddIndices(ct.routes().literals(), literals);
154 break;
155 case ConstraintProto::ConstraintCase::kInverse:
156 AddIndices(ct.inverse().f_direct(), variables);
157 AddIndices(ct.inverse().f_inverse(), variables);
158 break;
159 case ConstraintProto::ConstraintCase::kReservoir:
160 for (const LinearExpressionProto& time : ct.reservoir().time_exprs()) {
161 AddIndices(time.vars(), variables);
162 }
163 for (const LinearExpressionProto& level :
164 ct.reservoir().level_changes()) {
165 AddIndices(level.vars(), variables);
166 }
167 AddIndices(ct.reservoir().active_literals(), literals);
168 break;
169 case ConstraintProto::ConstraintCase::kTable:
170 AddIndices(ct.table().vars(), variables);
171 break;
172 case ConstraintProto::ConstraintCase::kAutomaton:
173 AddIndices(ct.automaton().vars(), variables);
174 break;
175 case ConstraintProto::ConstraintCase::kInterval:
176 AddIndices(ct.interval().start().vars(), variables);
177 AddIndices(ct.interval().size().vars(), variables);
178 AddIndices(ct.interval().end().vars(), variables);
179 break;
180 case ConstraintProto::ConstraintCase::kNoOverlap:
181 break;
182 case ConstraintProto::ConstraintCase::kNoOverlap2D:
183 break;
184 case ConstraintProto::ConstraintCase::kCumulative:
185 AddIndices(ct.cumulative().capacity().vars(), variables);
186 for (const LinearExpressionProto& demand : ct.cumulative().demands()) {
187 AddIndices(demand.vars(), variables);
188 }
189 break;
190 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
191 break;
192 }
193}
194
195#define APPLY_TO_SINGULAR_FIELD(ct_name, field_name) \
196 { \
197 int temp = ct->mutable_##ct_name()->field_name(); \
198 f(&temp); \
199 ct->mutable_##ct_name()->set_##field_name(temp); \
200 }
201
202#define APPLY_TO_REPEATED_FIELD(ct_name, field_name) \
203 { \
204 for (int& r : *ct->mutable_##ct_name()->mutable_##field_name()) f(&r); \
205 }
206
207void ApplyToAllLiteralIndices(const std::function<void(int*)>& f,
208 ConstraintProto* ct) {
209 for (int& r : *ct->mutable_enforcement_literal()) f(&r);
210 switch (ct->constraint_case()) {
211 case ConstraintProto::ConstraintCase::kBoolOr:
212 APPLY_TO_REPEATED_FIELD(bool_or, literals);
213 break;
214 case ConstraintProto::ConstraintCase::kBoolAnd:
215 APPLY_TO_REPEATED_FIELD(bool_and, literals);
216 break;
217 case ConstraintProto::ConstraintCase::kAtMostOne:
218 APPLY_TO_REPEATED_FIELD(at_most_one, literals);
219 break;
220 case ConstraintProto::ConstraintCase::kExactlyOne:
221 APPLY_TO_REPEATED_FIELD(exactly_one, literals);
222 break;
223 case ConstraintProto::ConstraintCase::kBoolXor:
224 APPLY_TO_REPEATED_FIELD(bool_xor, literals);
225 break;
226 case ConstraintProto::ConstraintCase::kIntDiv:
227 break;
228 case ConstraintProto::ConstraintCase::kIntMod:
229 break;
230 case ConstraintProto::ConstraintCase::kLinMax:
231 break;
232 case ConstraintProto::ConstraintCase::kIntProd:
233 break;
234 case ConstraintProto::ConstraintCase::kLinear:
235 break;
236 case ConstraintProto::ConstraintCase::kAllDiff:
237 break;
238 case ConstraintProto::ConstraintCase::kDummyConstraint:
239 break;
240 case ConstraintProto::ConstraintCase::kElement:
241 break;
242 case ConstraintProto::ConstraintCase::kCircuit:
243 APPLY_TO_REPEATED_FIELD(circuit, literals);
244 break;
245 case ConstraintProto::ConstraintCase::kRoutes:
246 APPLY_TO_REPEATED_FIELD(routes, literals);
247 break;
248 case ConstraintProto::ConstraintCase::kInverse:
249 break;
250 case ConstraintProto::ConstraintCase::kReservoir:
251 APPLY_TO_REPEATED_FIELD(reservoir, active_literals);
252 break;
253 case ConstraintProto::ConstraintCase::kTable:
254 break;
255 case ConstraintProto::ConstraintCase::kAutomaton:
256 break;
257 case ConstraintProto::ConstraintCase::kInterval:
258 break;
259 case ConstraintProto::ConstraintCase::kNoOverlap:
260 break;
261 case ConstraintProto::ConstraintCase::kNoOverlap2D:
262 break;
263 case ConstraintProto::ConstraintCase::kCumulative:
264 break;
265 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
266 break;
267 }
268}
269
270void ApplyToAllVariableIndices(const std::function<void(int*)>& f,
271 ConstraintProto* ct) {
272 switch (ct->constraint_case()) {
273 case ConstraintProto::ConstraintCase::kBoolOr:
274 break;
275 case ConstraintProto::ConstraintCase::kBoolAnd:
276 break;
277 case ConstraintProto::ConstraintCase::kAtMostOne:
278 break;
279 case ConstraintProto::ConstraintCase::kExactlyOne:
280 break;
281 case ConstraintProto::ConstraintCase::kBoolXor:
282 break;
283 case ConstraintProto::ConstraintCase::kIntDiv:
284 APPLY_TO_REPEATED_FIELD(int_div, target()->mutable_vars);
285 for (int i = 0; i < ct->int_div().exprs_size(); ++i) {
286 APPLY_TO_REPEATED_FIELD(int_div, exprs(i)->mutable_vars);
287 }
288 break;
289 case ConstraintProto::ConstraintCase::kIntMod:
290 APPLY_TO_REPEATED_FIELD(int_mod, target()->mutable_vars);
291 for (int i = 0; i < ct->int_mod().exprs_size(); ++i) {
292 APPLY_TO_REPEATED_FIELD(int_mod, exprs(i)->mutable_vars);
293 }
294 break;
295 case ConstraintProto::ConstraintCase::kLinMax:
296 APPLY_TO_REPEATED_FIELD(lin_max, target()->mutable_vars);
297 for (int i = 0; i < ct->lin_max().exprs_size(); ++i) {
298 APPLY_TO_REPEATED_FIELD(lin_max, exprs(i)->mutable_vars);
299 }
300 break;
301 case ConstraintProto::ConstraintCase::kIntProd:
302 APPLY_TO_REPEATED_FIELD(int_prod, target()->mutable_vars);
303 for (int i = 0; i < ct->int_prod().exprs_size(); ++i) {
304 APPLY_TO_REPEATED_FIELD(int_prod, exprs(i)->mutable_vars);
305 }
306 break;
307 case ConstraintProto::ConstraintCase::kLinear:
308 APPLY_TO_REPEATED_FIELD(linear, vars);
309 break;
310 case ConstraintProto::ConstraintCase::kAllDiff:
311 for (int i = 0; i < ct->all_diff().exprs_size(); ++i) {
312 APPLY_TO_REPEATED_FIELD(all_diff, exprs(i)->mutable_vars);
313 }
314 break;
315 case ConstraintProto::ConstraintCase::kDummyConstraint:
316 APPLY_TO_REPEATED_FIELD(dummy_constraint, vars);
317 break;
318 case ConstraintProto::ConstraintCase::kElement:
319 APPLY_TO_SINGULAR_FIELD(element, index);
320 APPLY_TO_SINGULAR_FIELD(element, target);
321 APPLY_TO_REPEATED_FIELD(element, vars);
322 break;
323 case ConstraintProto::ConstraintCase::kCircuit:
324 break;
325 case ConstraintProto::ConstraintCase::kRoutes:
326 break;
327 case ConstraintProto::ConstraintCase::kInverse:
328 APPLY_TO_REPEATED_FIELD(inverse, f_direct);
329 APPLY_TO_REPEATED_FIELD(inverse, f_inverse);
330 break;
331 case ConstraintProto::ConstraintCase::kReservoir:
332 for (int i = 0; i < ct->reservoir().time_exprs_size(); ++i) {
333 APPLY_TO_REPEATED_FIELD(reservoir, time_exprs(i)->mutable_vars);
334 }
335 for (int i = 0; i < ct->reservoir().level_changes_size(); ++i) {
336 APPLY_TO_REPEATED_FIELD(reservoir, level_changes(i)->mutable_vars);
337 }
338 break;
339 case ConstraintProto::ConstraintCase::kTable:
340 APPLY_TO_REPEATED_FIELD(table, vars);
341 break;
342 case ConstraintProto::ConstraintCase::kAutomaton:
343 APPLY_TO_REPEATED_FIELD(automaton, vars);
344 break;
345 case ConstraintProto::ConstraintCase::kInterval:
346 APPLY_TO_REPEATED_FIELD(interval, start()->mutable_vars);
347 APPLY_TO_REPEATED_FIELD(interval, size()->mutable_vars);
348 APPLY_TO_REPEATED_FIELD(interval, end()->mutable_vars);
349 break;
350 case ConstraintProto::ConstraintCase::kNoOverlap:
351 break;
352 case ConstraintProto::ConstraintCase::kNoOverlap2D:
353 break;
354 case ConstraintProto::ConstraintCase::kCumulative:
355 APPLY_TO_REPEATED_FIELD(cumulative, capacity()->mutable_vars);
356 for (int i = 0; i < ct->cumulative().demands_size(); ++i) {
357 for (int& r :
358 *ct->mutable_cumulative()->mutable_demands(i)->mutable_vars()) {
359 f(&r);
360 }
361 }
362 break;
363 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
364 break;
365 }
366}
367
368void ApplyToAllIntervalIndices(const std::function<void(int*)>& f,
369 ConstraintProto* ct) {
370 switch (ct->constraint_case()) {
371 case ConstraintProto::ConstraintCase::kBoolOr:
372 break;
373 case ConstraintProto::ConstraintCase::kBoolAnd:
374 break;
375 case ConstraintProto::ConstraintCase::kAtMostOne:
376 break;
377 case ConstraintProto::ConstraintCase::kExactlyOne:
378 break;
379 case ConstraintProto::ConstraintCase::kBoolXor:
380 break;
381 case ConstraintProto::ConstraintCase::kIntDiv:
382 break;
383 case ConstraintProto::ConstraintCase::kIntMod:
384 break;
385 case ConstraintProto::ConstraintCase::kLinMax:
386 break;
387 case ConstraintProto::ConstraintCase::kIntProd:
388 break;
389 case ConstraintProto::ConstraintCase::kLinear:
390 break;
391 case ConstraintProto::ConstraintCase::kAllDiff:
392 break;
393 case ConstraintProto::ConstraintCase::kDummyConstraint:
394 break;
395 case ConstraintProto::ConstraintCase::kElement:
396 break;
397 case ConstraintProto::ConstraintCase::kCircuit:
398 break;
399 case ConstraintProto::ConstraintCase::kRoutes:
400 break;
401 case ConstraintProto::ConstraintCase::kInverse:
402 break;
403 case ConstraintProto::ConstraintCase::kReservoir:
404 break;
405 case ConstraintProto::ConstraintCase::kTable:
406 break;
407 case ConstraintProto::ConstraintCase::kAutomaton:
408 break;
409 case ConstraintProto::ConstraintCase::kInterval:
410 break;
411 case ConstraintProto::ConstraintCase::kNoOverlap:
412 APPLY_TO_REPEATED_FIELD(no_overlap, intervals);
413 break;
414 case ConstraintProto::ConstraintCase::kNoOverlap2D:
415 APPLY_TO_REPEATED_FIELD(no_overlap_2d, x_intervals);
416 APPLY_TO_REPEATED_FIELD(no_overlap_2d, y_intervals);
417 break;
418 case ConstraintProto::ConstraintCase::kCumulative:
419 APPLY_TO_REPEATED_FIELD(cumulative, intervals);
420 break;
421 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
422 break;
423 }
424}
425
426#undef APPLY_TO_SINGULAR_FIELD
427#undef APPLY_TO_REPEATED_FIELD
428
429absl::string_view ConstraintCaseName(
430 ConstraintProto::ConstraintCase constraint_case) {
431 switch (constraint_case) {
432 case ConstraintProto::ConstraintCase::kBoolOr:
433 return "kBoolOr";
434 case ConstraintProto::ConstraintCase::kBoolAnd:
435 return "kBoolAnd";
436 case ConstraintProto::ConstraintCase::kAtMostOne:
437 return "kAtMostOne";
438 case ConstraintProto::ConstraintCase::kExactlyOne:
439 return "kExactlyOne";
440 case ConstraintProto::ConstraintCase::kBoolXor:
441 return "kBoolXor";
442 case ConstraintProto::ConstraintCase::kIntDiv:
443 return "kIntDiv";
444 case ConstraintProto::ConstraintCase::kIntMod:
445 return "kIntMod";
446 case ConstraintProto::ConstraintCase::kLinMax:
447 return "kLinMax";
448 case ConstraintProto::ConstraintCase::kIntProd:
449 return "kIntProd";
450 case ConstraintProto::ConstraintCase::kLinear:
451 return "kLinear";
452 case ConstraintProto::ConstraintCase::kAllDiff:
453 return "kAllDiff";
454 case ConstraintProto::ConstraintCase::kDummyConstraint:
455 return "kDummyConstraint";
456 case ConstraintProto::ConstraintCase::kElement:
457 return "kElement";
458 case ConstraintProto::ConstraintCase::kCircuit:
459 return "kCircuit";
460 case ConstraintProto::ConstraintCase::kRoutes:
461 return "kRoutes";
462 case ConstraintProto::ConstraintCase::kInverse:
463 return "kInverse";
464 case ConstraintProto::ConstraintCase::kReservoir:
465 return "kReservoir";
466 case ConstraintProto::ConstraintCase::kTable:
467 return "kTable";
468 case ConstraintProto::ConstraintCase::kAutomaton:
469 return "kAutomaton";
470 case ConstraintProto::ConstraintCase::kInterval:
471 return "kInterval";
472 case ConstraintProto::ConstraintCase::kNoOverlap:
473 return "kNoOverlap";
474 case ConstraintProto::ConstraintCase::kNoOverlap2D:
475 return "kNoOverlap2D";
476 case ConstraintProto::ConstraintCase::kCumulative:
477 return "kCumulative";
478 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
479 return "kEmpty";
480 }
481}
482
483std::vector<int> UsedVariables(const ConstraintProto& ct) {
484 std::vector<int> result;
485 GetReferencesUsedByConstraint(ct, &result, &result);
486 for (int& ref : result) {
487 ref = PositiveRef(ref);
488 }
489 for (const int lit : ct.enforcement_literal()) {
490 result.push_back(PositiveRef(lit));
491 }
492 gtl::STLSortAndRemoveDuplicates(&result);
493 return result;
494}
495
496std::vector<int> UsedIntervals(const ConstraintProto& ct) {
497 std::vector<int> used_intervals;
498 switch (ct.constraint_case()) {
499 case ConstraintProto::ConstraintCase::kBoolOr:
500 break;
501 case ConstraintProto::ConstraintCase::kBoolAnd:
502 break;
503 case ConstraintProto::ConstraintCase::kAtMostOne:
504 break;
505 case ConstraintProto::ConstraintCase::kExactlyOne:
506 break;
507 case ConstraintProto::ConstraintCase::kBoolXor:
508 break;
509 case ConstraintProto::ConstraintCase::kIntDiv:
510 break;
511 case ConstraintProto::ConstraintCase::kIntMod:
512 break;
513 case ConstraintProto::ConstraintCase::kLinMax:
514 break;
515 case ConstraintProto::ConstraintCase::kIntProd:
516 break;
517 case ConstraintProto::ConstraintCase::kLinear:
518 break;
519 case ConstraintProto::ConstraintCase::kAllDiff:
520 break;
521 case ConstraintProto::ConstraintCase::kDummyConstraint:
522 break;
523 case ConstraintProto::ConstraintCase::kElement:
524 break;
525 case ConstraintProto::ConstraintCase::kCircuit:
526 break;
527 case ConstraintProto::ConstraintCase::kRoutes:
528 break;
529 case ConstraintProto::ConstraintCase::kInverse:
530 break;
531 case ConstraintProto::ConstraintCase::kReservoir:
532 break;
533 case ConstraintProto::ConstraintCase::kTable:
534 break;
535 case ConstraintProto::ConstraintCase::kAutomaton:
536 break;
537 case ConstraintProto::ConstraintCase::kInterval:
538 break;
539 case ConstraintProto::ConstraintCase::kNoOverlap:
540 AddIndices(ct.no_overlap().intervals(), &used_intervals);
541 break;
542 case ConstraintProto::ConstraintCase::kNoOverlap2D:
543 AddIndices(ct.no_overlap_2d().x_intervals(), &used_intervals);
544 AddIndices(ct.no_overlap_2d().y_intervals(), &used_intervals);
545 break;
546 case ConstraintProto::ConstraintCase::kCumulative:
547 AddIndices(ct.cumulative().intervals(), &used_intervals);
548 break;
549 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
550 break;
551 }
552 gtl::STLSortAndRemoveDuplicates(&used_intervals);
553 return used_intervals;
554}
555
556int64_t ComputeInnerObjective(const CpObjectiveProto& objective,
557 absl::Span<const int64_t> solution) {
558 int64_t objective_value = 0;
559 for (int i = 0; i < objective.vars_size(); ++i) {
560 int64_t coeff = objective.coeffs(i);
561 const int ref = objective.vars(i);
562 const int var = PositiveRef(ref);
563 if (!RefIsPositive(ref)) coeff = -coeff;
564 objective_value += coeff * solution[var];
565 }
566 return objective_value;
567}
568
569bool ExpressionContainsSingleRef(const LinearExpressionProto& expr) {
570 return expr.offset() == 0 && expr.vars_size() == 1 &&
571 std::abs(expr.coeffs(0)) == 1;
572}
573
574bool ExpressionIsAffine(const LinearExpressionProto& expr) {
575 return expr.vars_size() <= 1;
576}
577
578// Returns the reference the expression can be reduced to. It will DCHECK that
579// ExpressionContainsSingleRef(expr) is true.
580int GetSingleRefFromExpression(const LinearExpressionProto& expr) {
581 DCHECK(ExpressionContainsSingleRef(expr));
582 return expr.coeffs(0) == 1 ? expr.vars(0) : NegatedRef(expr.vars(0));
583}
584
585void AddLinearExpressionToLinearConstraint(const LinearExpressionProto& expr,
586 int64_t coefficient,
587 LinearConstraintProto* linear) {
588 for (int i = 0; i < expr.vars_size(); ++i) {
589 linear->add_vars(expr.vars(i));
590 linear->add_coeffs(expr.coeffs(i) * coefficient);
591 }
592 DCHECK(!linear->domain().empty());
593 const int64_t shift = coefficient * expr.offset();
594 if (shift != 0) {
595 FillDomainInProto(ReadDomainFromProto(*linear).AdditionWith(Domain(-shift)),
596 linear);
597 }
598}
599
600bool SafeAddLinearExpressionToLinearConstraint(
601 const LinearExpressionProto& expr, int64_t coefficient,
602 LinearConstraintProto* linear) {
603 for (int i = 0; i < expr.vars_size(); ++i) {
604 linear->add_vars(expr.vars(i));
605 const int64_t prod = CapProd(expr.coeffs(i), coefficient);
606 if (AtMinOrMaxInt64(prod)) return false;
607 linear->add_coeffs(prod);
608 }
609 DCHECK(!linear->domain().empty());
610
611 const int64_t shift = CapProd(coefficient, expr.offset());
612 if (AtMinOrMaxInt64(shift)) return false;
613 Domain d = ReadDomainFromProto(*linear).AdditionWith(Domain(-shift));
614 if (AtMinOrMaxInt64(d.Min()) || AtMinOrMaxInt64(d.Max())) return false;
615 FillDomainInProto(d, linear);
616 return true;
617}
618
619bool LinearExpressionProtosAreEqual(const LinearExpressionProto& a,
620 const LinearExpressionProto& b,
621 int64_t b_scaling) {
622 if (a.vars_size() != b.vars_size()) return false;
623 if (a.offset() != b.offset() * b_scaling) return false;
624 absl::flat_hash_map<int, int64_t> coeffs;
625 for (int i = 0; i < a.vars_size(); ++i) {
626 coeffs[a.vars(i)] += a.coeffs(i);
627 coeffs[b.vars(i)] += -b.coeffs(i) * b_scaling;
628 }
629
630 for (const auto [var, coeff] : coeffs) {
631 if (coeff != 0) return false;
632 }
633 return true;
634}
635
636uint64_t FingerprintExpression(const LinearExpressionProto& lin,
637 uint64_t seed) {
638 uint64_t fp = seed;
639 if (!lin.vars().empty()) {
640 fp = FingerprintRepeatedField(lin.vars(), fp);
641 fp = FingerprintRepeatedField(lin.coeffs(), fp);
642 }
643 fp = FingerprintSingleField(lin.offset(), fp);
644 return fp;
645}
646
647uint64_t FingerprintModel(const CpModelProto& model, uint64_t seed) {
648 uint64_t fp = seed;
649 for (const IntegerVariableProto& var_proto : model.variables()) {
650 fp = FingerprintRepeatedField(var_proto.domain(), fp);
651 }
652 for (const ConstraintProto& ct : model.constraints()) {
653 if (!ct.enforcement_literal().empty()) {
654 fp = FingerprintRepeatedField(ct.enforcement_literal(), fp);
655 }
656 switch (ct.constraint_case()) {
657 case ConstraintProto::ConstraintCase::kBoolOr:
658 fp = FingerprintRepeatedField(ct.bool_or().literals(), fp);
659 break;
660 case ConstraintProto::ConstraintCase::kBoolAnd:
661 fp = FingerprintRepeatedField(ct.bool_and().literals(), fp);
662 break;
663 case ConstraintProto::ConstraintCase::kAtMostOne:
664 fp = FingerprintRepeatedField(ct.at_most_one().literals(), fp);
665 break;
666 case ConstraintProto::ConstraintCase::kExactlyOne:
667 fp = FingerprintRepeatedField(ct.exactly_one().literals(), fp);
668 break;
669 case ConstraintProto::ConstraintCase::kBoolXor:
670 fp = FingerprintRepeatedField(ct.bool_xor().literals(), fp);
671 break;
672 case ConstraintProto::ConstraintCase::kIntDiv:
673 fp = FingerprintExpression(ct.int_div().target(), fp);
674 for (const LinearExpressionProto& expr : ct.int_div().exprs()) {
675 fp = FingerprintExpression(expr, fp);
676 }
677 break;
678 case ConstraintProto::ConstraintCase::kIntMod:
679 fp = FingerprintExpression(ct.int_mod().target(), fp);
680 for (const LinearExpressionProto& expr : ct.int_mod().exprs()) {
681 fp = FingerprintExpression(expr, fp);
682 }
683 break;
684 case ConstraintProto::ConstraintCase::kLinMax: {
685 fp = FingerprintExpression(ct.lin_max().target(), fp);
686 for (const LinearExpressionProto& expr : ct.lin_max().exprs()) {
687 fp = FingerprintExpression(expr, fp);
688 }
689 break;
690 }
691 case ConstraintProto::ConstraintCase::kIntProd:
692 fp = FingerprintExpression(ct.int_prod().target(), fp);
693 for (const LinearExpressionProto& expr : ct.int_prod().exprs()) {
694 fp = FingerprintExpression(expr, fp);
695 }
696 break;
697 case ConstraintProto::ConstraintCase::kLinear:
698 fp = FingerprintRepeatedField(ct.linear().vars(), fp);
699 fp = FingerprintRepeatedField(ct.linear().coeffs(), fp);
700 fp = FingerprintRepeatedField(ct.linear().domain(), fp);
701 break;
702 case ConstraintProto::ConstraintCase::kAllDiff:
703 for (const LinearExpressionProto& expr : ct.all_diff().exprs()) {
704 fp = FingerprintExpression(expr, fp);
705 }
706 break;
707 case ConstraintProto::ConstraintCase::kDummyConstraint:
708 break;
709 case ConstraintProto::ConstraintCase::kElement:
710 fp = FingerprintSingleField(ct.element().index(), fp);
711 fp = FingerprintSingleField(ct.element().target(), fp);
712 fp = FingerprintRepeatedField(ct.element().vars(), fp);
713 break;
714 case ConstraintProto::ConstraintCase::kCircuit:
715 fp = FingerprintRepeatedField(ct.circuit().heads(), fp);
716 fp = FingerprintRepeatedField(ct.circuit().tails(), fp);
717 fp = FingerprintRepeatedField(ct.circuit().literals(), fp);
718 break;
719 case ConstraintProto::ConstraintCase::kRoutes:
720 fp = FingerprintRepeatedField(ct.routes().heads(), fp);
721 fp = FingerprintRepeatedField(ct.routes().tails(), fp);
722 fp = FingerprintRepeatedField(ct.routes().literals(), fp);
723 break;
724 case ConstraintProto::ConstraintCase::kInverse:
725 fp = FingerprintRepeatedField(ct.inverse().f_direct(), fp);
726 fp = FingerprintRepeatedField(ct.inverse().f_inverse(), fp);
727 break;
728 case ConstraintProto::ConstraintCase::kReservoir:
729 fp = FingerprintSingleField(ct.reservoir().min_level(), fp);
730 fp = FingerprintSingleField(ct.reservoir().max_level(), fp);
731 for (const LinearExpressionProto& expr : ct.reservoir().time_exprs()) {
732 fp = FingerprintExpression(expr, fp);
733 }
734 for (const LinearExpressionProto& expr :
735 ct.reservoir().level_changes()) {
736 fp = FingerprintExpression(expr, fp);
737 }
738 break;
739 case ConstraintProto::ConstraintCase::kTable:
740 fp = FingerprintRepeatedField(ct.table().vars(), fp);
741 fp = FingerprintRepeatedField(ct.table().values(), fp);
742 fp = FingerprintSingleField(ct.table().negated(), fp);
743 break;
744 case ConstraintProto::ConstraintCase::kAutomaton:
745 fp = FingerprintSingleField(ct.automaton().starting_state(), fp);
746 fp = FingerprintRepeatedField(ct.automaton().final_states(), fp);
747 fp = FingerprintRepeatedField(ct.automaton().transition_tail(), fp);
748 fp = FingerprintRepeatedField(ct.automaton().transition_head(), fp);
749 fp = FingerprintRepeatedField(ct.automaton().transition_label(), fp);
750 fp = FingerprintRepeatedField(ct.automaton().vars(), fp);
751 break;
752 case ConstraintProto::ConstraintCase::kInterval:
753 fp = FingerprintExpression(ct.interval().start(), fp);
754 fp = FingerprintExpression(ct.interval().size(), fp);
755 fp = FingerprintExpression(ct.interval().end(), fp);
756 break;
757 case ConstraintProto::ConstraintCase::kNoOverlap:
758 fp = FingerprintRepeatedField(ct.no_overlap().intervals(), fp);
759 break;
760 case ConstraintProto::ConstraintCase::kNoOverlap2D:
761 fp = FingerprintRepeatedField(ct.no_overlap_2d().x_intervals(), fp);
762 fp = FingerprintRepeatedField(ct.no_overlap_2d().y_intervals(), fp);
763 break;
764 case ConstraintProto::ConstraintCase::kCumulative:
765 fp = FingerprintRepeatedField(ct.cumulative().intervals(), fp);
766 fp = FingerprintExpression(ct.cumulative().capacity(), fp);
767 for (const LinearExpressionProto& demand : ct.cumulative().demands()) {
768 fp = FingerprintExpression(demand, fp);
769 }
770 break;
771 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
772 break;
773 }
774 }
775
776 // Fingerprint the objective.
777 if (model.has_objective()) {
778 fp = FingerprintRepeatedField(model.objective().vars(), fp);
779 fp = FingerprintRepeatedField(model.objective().coeffs(), fp);
780 fp = FingerprintSingleField(model.objective().offset(), fp);
781 fp = FingerprintSingleField(model.objective().scaling_factor(), fp);
782 fp = FingerprintRepeatedField(model.objective().domain(), fp);
783 } else if (model.has_floating_point_objective()) {
784 fp = FingerprintRepeatedField(model.floating_point_objective().vars(), fp);
785 fp =
786 FingerprintRepeatedField(model.floating_point_objective().coeffs(), fp);
787 fp = FingerprintSingleField(model.floating_point_objective().offset(), fp);
788 fp =
789 FingerprintSingleField(model.floating_point_objective().maximize(), fp);
790 }
791
792 if (model.has_solution_hint()) {
793 fp = FingerprintRepeatedField(model.solution_hint().vars(), fp);
794 fp = FingerprintRepeatedField(model.solution_hint().values(), fp);
795 }
796
797 // TODO(user): Should we fingerprint decision strategies?
798
799 return fp;
800}
801
802#if !defined(__PORTABLE_PLATFORM__)
803namespace {
804
805// We need to print " { " instead of " {\n" to inline our variables like:
806//
807// variables { domain: [0, 1] }
808//
809// instead of
810//
811// variables {
812// domain: [0, 1] }
813class InlineFieldPrinter
814 : public google::protobuf::TextFormat::FastFieldValuePrinter {
815 void PrintMessageStart(const google::protobuf::Message& /*message*/,
816 int /*field_index*/, int /*field_count*/,
817 bool /*single_line_mode*/,
818 google::protobuf::TextFormat::BaseTextGenerator*
819 generator) const override {
820 generator->PrintLiteral(" { ");
821 }
822};
823
824class InlineMessagePrinter
825 : public google::protobuf::TextFormat::MessagePrinter {
826 public:
827 InlineMessagePrinter() {
828 printer_.SetSingleLineMode(true);
829 printer_.SetUseShortRepeatedPrimitives(true);
830 }
831
832 void Print(const google::protobuf::Message& message,
833 bool /*single_line_mode*/,
834 google::protobuf::TextFormat::BaseTextGenerator* generator)
835 const override {
836 buffer_.clear();
837 printer_.PrintToString(message, &buffer_);
838 generator->Print(buffer_.data(), buffer_.size());
839 }
840
841 private:
842 google::protobuf::TextFormat::Printer printer_;
843 mutable std::string buffer_;
844};
845
846// Register a InlineFieldPrinter() for all the fields containing the message we
847// want to print in one line.
848void RegisterFieldPrinters(
849 const google::protobuf::Descriptor* descriptor,
850 absl::flat_hash_set<const google::protobuf::Descriptor*>* descriptors,
851 google::protobuf::TextFormat::Printer* printer) {
852 // Recursion stopper.
853 if (!descriptors->insert(descriptor).second) return;
854
855 for (int i = 0; i < descriptor->field_count(); ++i) {
856 const google::protobuf::FieldDescriptor* field = descriptor->field(i);
857 if (field->type() == google::protobuf::FieldDescriptor::TYPE_MESSAGE) {
858 if (field->message_type() == IntegerVariableProto::descriptor() ||
859 field->message_type() == LinearExpressionProto::descriptor()) {
860 printer->RegisterFieldValuePrinter(field, new InlineFieldPrinter());
861 } else {
862 RegisterFieldPrinters(field->message_type(), descriptors, printer);
863 }
864 }
865 }
866}
867
868} // namespace
869
870void SetupTextFormatPrinter(google::protobuf::TextFormat::Printer* printer) {
871 printer->SetUseShortRepeatedPrimitives(true);
872 absl::flat_hash_set<const google::protobuf::Descriptor*> descriptors;
873 RegisterFieldPrinters(CpModelProto::descriptor(), &descriptors, printer);
874 printer->RegisterMessagePrinter(IntegerVariableProto::descriptor(),
875 new InlineMessagePrinter());
876 printer->RegisterMessagePrinter(LinearExpressionProto::descriptor(),
877 new InlineMessagePrinter());
878}
879#endif // !defined(__PORTABLE_PLATFORM__)
880
881bool ConvertCpModelProtoToCnf(const CpModelProto& cp_model, std::string* out) {
882 out->clear();
883
884 // We should have no objective, only unassigned Boolean, and only bool_or and
885 // bool_and.
886 if (cp_model.has_objective()) return false;
887 const int num_vars = cp_model.variables().size();
888 for (int v = 0; v < num_vars; ++v) {
889 if (cp_model.variables(v).domain().size() != 2) return false;
890 if (cp_model.variables(v).domain(0) != 0) return false;
891 if (cp_model.variables(v).domain(1) != 1) return false;
892 }
893 int num_clauses = 0;
894 for (const ConstraintProto& ct : cp_model.constraints()) {
895 if (ct.constraint_case() == ConstraintProto::kBoolOr) {
896 ++num_clauses;
897 } else if (ct.constraint_case() == ConstraintProto::kBoolAnd) {
898 num_clauses += ct.bool_and().literals().size();
899 } else {
900 return false;
901 }
902 }
903
904 // We can convert.
905 std::string start;
906 absl::StrAppend(out, "p cnf ", num_vars, " ", num_clauses, "\n");
907 for (const ConstraintProto& ct : cp_model.constraints()) {
908 if (ct.constraint_case() == ConstraintProto::kBoolOr) {
909 CHECK(ct.enforcement_literal().empty());
910 for (const int lit : ct.bool_or().literals()) {
911 const int value =
912 Literal(BooleanVariable(PositiveRef(lit)), RefIsPositive(lit))
913 .SignedValue();
914 absl::StrAppend(out, value, " ");
915 }
916 absl::StrAppend(out, "0\n");
917 } else if (ct.constraint_case() == ConstraintProto::kBoolAnd) {
918 CHECK(!ct.enforcement_literal().empty());
919 start.clear();
920 for (const int lit : ct.enforcement_literal()) {
921 const int value =
922 Literal(BooleanVariable(PositiveRef(lit)), RefIsPositive(lit))
923 .SignedValue();
924 absl::StrAppend(&start, -value, " ");
925 }
926 for (const int lit : ct.bool_and().literals()) {
927 const int value =
928 Literal(BooleanVariable(PositiveRef(lit)), RefIsPositive(lit))
929 .SignedValue();
930 absl::StrAppend(out, start, value, " 0\n");
931 }
932 }
933 }
934
935 return true;
936}
937
938int CombineSeed(int base_seed, int64_t delta) {
939 CHECK_GE(delta, 0);
940 const uint64_t fp = FingerprintSingleField(delta, kDefaultFingerprintSeed);
941 return static_cast<int>(FingerprintSingleField(base_seed, fp) & (0x7FFFFFFF));
942}
943
944} // namespace sat
945} // namespace operations_research
size
IntegerValue size
Definition 2d_rectangle_presolve.cc:235
operations_research::Domain
Definition sorted_interval_list.h:87
operations_research::Domain::Max
int64_t Max() const
Definition sorted_interval_list.cc:224
operations_research::Domain::Min
int64_t Min() const
Definition sorted_interval_list.cc:219
operations_research::Domain::AdditionWith
Domain AdditionWith(const Domain &domain) const
Definition sorted_interval_list.cc:428
operations_research::sat::Literal
Definition sat_base.h:66
operations_research::sat::Literal::SignedValue
int SignedValue() const
Definition sat_base.h:94
a
int64_t a
Definition table.cc:44
APPLY_TO_SINGULAR_FIELD
#define APPLY_TO_SINGULAR_FIELD(ct_name, field_name)
Definition cp_model_utils.cc:195
APPLY_TO_REPEATED_FIELD
#define APPLY_TO_REPEATED_FIELD(ct_name, field_name)
Definition cp_model_utils.cc:202
cp_model_utils.h
ct
const Constraint * ct
Definition demon_profiler.cc:45
value
int64_t value
Definition demon_profiler.cc:46
var
IntVar * var
Definition expr_array.cc:1876
model
GRBmodel * model
Definition gurobi_interface.cc:300
lit
int lit
Definition linear_model.cc:55
index
int index
Definition local_search.cc:2838
solution
double solution
Definition multi_objective_tests.cc:167
gtl::STLSortAndRemoveDuplicates
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition stl_util.h:58
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:245
operations_research::sat::FingerprintRepeatedField
uint64_t FingerprintRepeatedField(const google::protobuf::RepeatedField< T > &sequence, uint64_t seed)
Definition cp_model_utils.h:248
operations_research::sat::RefIsPositive
bool RefIsPositive(int ref)
Definition cp_model_utils.h:45
operations_research::sat::ComputeInnerObjective
int64_t ComputeInnerObjective(const CpObjectiveProto &objective, absl::Span< const int64_t > solution)
Definition cp_model_utils.cc:556
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:938
operations_research::sat::ApplyToAllIntervalIndices
void ApplyToAllIntervalIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
Definition cp_model_utils.cc:368
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:600
operations_research::sat::FingerprintSingleField
uint64_t FingerprintSingleField(const T &field, uint64_t seed)
Definition cp_model_utils.h:256
operations_research::sat::ConvertCpModelProtoToCnf
bool ConvertCpModelProtoToCnf(const CpModelProto &cp_model, std::string *out)
Definition cp_model_utils.cc:881
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:636
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:647
operations_research::sat::ExpressionIsAffine
bool ExpressionIsAffine(const LinearExpressionProto &expr)
Checks if the expression is affine or constant.
Definition cp_model_utils.cc:574
operations_research::sat::UsedVariables
std::vector< int > UsedVariables(const ConstraintProto &ct)
Definition cp_model_utils.cc:483
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:496
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:122
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:133
operations_research::sat::SetupTextFormatPrinter
void SetupTextFormatPrinter(google::protobuf::TextFormat::Printer *printer)
Definition cp_model_utils.cc:870
operations_research::sat::ConstraintCaseName
absl::string_view ConstraintCaseName(ConstraintProto::ConstraintCase constraint_case)
Definition cp_model_utils.cc:429
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:569
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:207
operations_research::sat::PositiveRef
int PositiveRef(int ref)
Definition cp_model_utils.h:44
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:585
operations_research::sat::GetSingleRefFromExpression
int GetSingleRefFromExpression(const LinearExpressionProto &expr)
Definition cp_model_utils.cc:580
operations_research::sat::NegatedRef
int NegatedRef(int ref)
Small utility functions to deal with negative variable/literal references.
Definition cp_model_utils.h:43
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:619
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:270
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::CapProd
int64_t CapProd(int64_t x, int64_t y)
Definition saturated_arithmetic.h:314
demand
int64_t demand
Definition resource.cc:126
time
int64_t time
Definition resource.cc:1708
delta
int64_t delta
Definition resource.cc:1709
interval
IntervalVar * interval
Definition resource.cc:101
coefficient
int64_t coefficient
Definition routing_filters.cc:969
sat_base.h
saturated_arithmetic.h
sorted_interval_list.h
end
std::optional< int64_t > end
Definition sparse_submatrix.cc:37
start
int64_t start
Definition sparse_submatrix.cc:36
stl_util.h
operations_research::sat::IndexReferences
Definition cp_model_utils.h:71
operations_research::sat::IndexReferences::variables
std::vector< int > variables
Definition cp_model_utils.h:72
operations_research::sat::IndexReferences::literals
std::vector< int > literals
Definition cp_model_utils.h:73
message
std::string message
Definition trace.cc:397
objective_value
double objective_value
The value objective_vector^T * (solution - center_point).
Definition trust_region.cc:168