OR-Tools  8.2
checker.cc
Go to the documentation of this file.
1// Copyright 2010-2018 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
15
16#include <algorithm>
17
18#include "absl/container/flat_hash_map.h"
19#include "absl/container/flat_hash_set.h"
23
24namespace operations_research {
25namespace fz {
26namespace {
27
28// Helpers
29
30int64 Eval(const Argument& arg,
31 const std::function<int64(IntegerVariable*)>& evaluator) {
32 switch (arg.type) {
34 return arg.Value();
35 }
37 return evaluator(arg.Var());
38 }
39 default: {
40 LOG(FATAL) << "Cannot evaluate " << arg.DebugString();
41 return 0;
42 }
43 }
44}
45
46int Size(const Argument& arg) {
47 return std::max(arg.values.size(), arg.variables.size());
48}
49
50int64 EvalAt(const Argument& arg, int pos,
51 const std::function<int64(IntegerVariable*)>& evaluator) {
52 switch (arg.type) {
53 case Argument::INT_LIST: {
54 return arg.ValueAt(pos);
55 }
57 return evaluator(arg.VarAt(pos));
58 }
59 default: {
60 LOG(FATAL) << "Cannot evaluate " << arg.DebugString();
61 return 0;
62 }
63 }
64}
65
66// Checkers
67
68bool CheckAllDifferentInt(
69 const Constraint& ct,
70 const std::function<int64(IntegerVariable*)>& evaluator) {
71 absl::flat_hash_set<int64> visited;
72 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
73 const int64 value = EvalAt(ct.arguments[0], i, evaluator);
74 if (gtl::ContainsKey(visited, value)) {
75 return false;
76 }
77 visited.insert(value);
78 }
79
80 return true;
81}
82
83bool CheckAlldifferentExcept0(
84 const Constraint& ct,
85 const std::function<int64(IntegerVariable*)>& evaluator) {
86 absl::flat_hash_set<int64> visited;
87 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
88 const int64 value = EvalAt(ct.arguments[0], i, evaluator);
89 if (value != 0 && gtl::ContainsKey(visited, value)) {
90 return false;
91 }
92 visited.insert(value);
93 }
94
95 return true;
96}
97
98bool CheckAmong(const Constraint& ct,
99 const std::function<int64(IntegerVariable*)>& evaluator) {
100 const int64 expected = Eval(ct.arguments[0], evaluator);
101 int64 count = 0;
102 for (int i = 0; i < Size(ct.arguments[1]); ++i) {
103 const int64 value = EvalAt(ct.arguments[0], i, evaluator);
104 count += ct.arguments[2].Contains(value);
105 }
106
107 return count == expected;
108}
109
110bool CheckArrayBoolAnd(
111 const Constraint& ct,
112 const std::function<int64(IntegerVariable*)>& evaluator) {
113 int64 result = 1;
114
115 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
116 const int64 value = EvalAt(ct.arguments[0], i, evaluator);
117 result = std::min(result, value);
118 }
119
120 return result == Eval(ct.arguments[1], evaluator);
121}
122
123bool CheckArrayBoolOr(const Constraint& ct,
124 const std::function<int64(IntegerVariable*)>& evaluator) {
125 int64 result = 0;
126
127 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
128 const int64 value = EvalAt(ct.arguments[0], i, evaluator);
129 result = std::max(result, value);
130 }
131
132 return result == Eval(ct.arguments[1], evaluator);
133}
134
135bool CheckArrayBoolXor(
136 const Constraint& ct,
137 const std::function<int64(IntegerVariable*)>& evaluator) {
138 int64 result = 0;
139
140 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
141 result += EvalAt(ct.arguments[0], i, evaluator);
142 }
143
144 return result % 2 == 1;
145}
146
147bool CheckArrayIntElement(
148 const Constraint& ct,
149 const std::function<int64(IntegerVariable*)>& evaluator) {
150 if (ct.arguments[0].variables.size() == 2) {
151 // TODO(user): Check 2D element.
152 return true;
153 }
154 // Flatzinc arrays are 1 based.
155 const int64 shifted_index = Eval(ct.arguments[0], evaluator) - 1;
156 const int64 element = EvalAt(ct.arguments[1], shifted_index, evaluator);
157 const int64 target = Eval(ct.arguments[2], evaluator);
158 return element == target;
159}
160
161bool CheckArrayIntElementNonShifted(
162 const Constraint& ct,
163 const std::function<int64(IntegerVariable*)>& evaluator) {
164 CHECK_EQ(ct.arguments[0].variables.size(), 1);
165 const int64 index = Eval(ct.arguments[0], evaluator);
166 const int64 element = EvalAt(ct.arguments[1], index, evaluator);
167 const int64 target = Eval(ct.arguments[2], evaluator);
168 return element == target;
169}
170
171bool CheckArrayVarIntElement(
172 const Constraint& ct,
173 const std::function<int64(IntegerVariable*)>& evaluator) {
174 if (ct.arguments[0].variables.size() == 2) {
175 // TODO(user): Check 2D element.
176 return true;
177 }
178 // Flatzinc arrays are 1 based.
179 const int64 shifted_index = Eval(ct.arguments[0], evaluator) - 1;
180 const int64 element = EvalAt(ct.arguments[1], shifted_index, evaluator);
181 const int64 target = Eval(ct.arguments[2], evaluator);
182 return element == target;
183}
184
185bool CheckAtMostInt(const Constraint& ct,
186 const std::function<int64(IntegerVariable*)>& evaluator) {
187 const int64 expected = Eval(ct.arguments[0], evaluator);
188 const int64 value = Eval(ct.arguments[2], evaluator);
189
190 int64 count = 0;
191 for (int i = 0; i < Size(ct.arguments[1]); ++i) {
192 count += EvalAt(ct.arguments[1], i, evaluator) == value;
193 }
194 return count <= expected;
195}
196
197bool CheckBoolAnd(const Constraint& ct,
198 const std::function<int64(IntegerVariable*)>& evaluator) {
199 const int64 left = Eval(ct.arguments[0], evaluator);
200 const int64 right = Eval(ct.arguments[1], evaluator);
201 const int64 status = Eval(ct.arguments[2], evaluator);
202 return status == std::min(left, right);
203}
204
205bool CheckBoolClause(const Constraint& ct,
206 const std::function<int64(IntegerVariable*)>& evaluator) {
207 int64 result = 0;
208
209 // Positive variables.
210 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
211 const int64 value = EvalAt(ct.arguments[0], i, evaluator);
212 result = std::max(result, value);
213 }
214 // Negative variables.
215 for (int i = 0; i < Size(ct.arguments[1]); ++i) {
216 const int64 value = EvalAt(ct.arguments[1], i, evaluator);
217 result = std::max(result, 1 - value);
218 }
219
220 return result;
221}
222
223bool CheckBoolNot(const Constraint& ct,
224 const std::function<int64(IntegerVariable*)>& evaluator) {
225 const int64 left = Eval(ct.arguments[0], evaluator);
226 const int64 right = Eval(ct.arguments[1], evaluator);
227 return left == 1 - right;
228}
229
230bool CheckBoolOr(const Constraint& ct,
231 const std::function<int64(IntegerVariable*)>& evaluator) {
232 const int64 left = Eval(ct.arguments[0], evaluator);
233 const int64 right = Eval(ct.arguments[1], evaluator);
234 const int64 status = Eval(ct.arguments[2], evaluator);
235 return status == std::max(left, right);
236}
237
238bool CheckBoolXor(const Constraint& ct,
239 const std::function<int64(IntegerVariable*)>& evaluator) {
240 const int64 left = Eval(ct.arguments[0], evaluator);
241 const int64 right = Eval(ct.arguments[1], evaluator);
242 const int64 target = Eval(ct.arguments[2], evaluator);
243 return target == (left + right == 1);
244}
245
246bool CheckCircuit(const Constraint& ct,
247 const std::function<int64(IntegerVariable*)>& evaluator) {
248 // There are two versions of the constraint. 0 based and 1 based.
249 // Let's try to detect which one we have.
250 const int size = Size(ct.arguments[0]);
251 int shift = 0;
252 for (int i = 0; i < size; ++i) {
253 const int64 next = EvalAt(ct.arguments[0], i, evaluator);
254 if (next == 0) { // 0 based.
255 shift = 0;
256 break;
257 } else if (next == size) { // 1 based.
258 shift = -1;
259 break;
260 }
261 }
262
263 absl::flat_hash_set<int64> visited;
264 int64 current = 0;
265 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
266 const int64 next = EvalAt(ct.arguments[0], current, evaluator) + shift;
267 visited.insert(next);
268 current = next;
269 }
270 return visited.size() == Size(ct.arguments[0]);
271}
272
273int64 ComputeCount(const Constraint& ct,
274 const std::function<int64(IntegerVariable*)>& evaluator) {
275 int64 result = 0;
276 const int64 value = Eval(ct.arguments[1], evaluator);
277 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
278 result += EvalAt(ct.arguments[0], i, evaluator) == value;
279 }
280 return result;
281}
282
283bool CheckCountEq(const Constraint& ct,
284 const std::function<int64(IntegerVariable*)>& evaluator) {
285 const int64 count = ComputeCount(ct, evaluator);
286 const int64 expected = Eval(ct.arguments[2], evaluator);
287 return count == expected;
288}
289
290bool CheckCountGeq(const Constraint& ct,
291 const std::function<int64(IntegerVariable*)>& evaluator) {
292 const int64 count = ComputeCount(ct, evaluator);
293 const int64 expected = Eval(ct.arguments[2], evaluator);
294 return count >= expected;
295}
296
297bool CheckCountGt(const Constraint& ct,
298 const std::function<int64(IntegerVariable*)>& evaluator) {
299 const int64 count = ComputeCount(ct, evaluator);
300 const int64 expected = Eval(ct.arguments[2], evaluator);
301 return count > expected;
302}
303
304bool CheckCountLeq(const Constraint& ct,
305 const std::function<int64(IntegerVariable*)>& evaluator) {
306 const int64 count = ComputeCount(ct, evaluator);
307 const int64 expected = Eval(ct.arguments[2], evaluator);
308 return count <= expected;
309}
310
311bool CheckCountLt(const Constraint& ct,
312 const std::function<int64(IntegerVariable*)>& evaluator) {
313 const int64 count = ComputeCount(ct, evaluator);
314 const int64 expected = Eval(ct.arguments[2], evaluator);
315 return count < expected;
316}
317
318bool CheckCountNeq(const Constraint& ct,
319 const std::function<int64(IntegerVariable*)>& evaluator) {
320 const int64 count = ComputeCount(ct, evaluator);
321 const int64 expected = Eval(ct.arguments[2], evaluator);
322 return count != expected;
323}
324
325bool CheckCountReif(const Constraint& ct,
326 const std::function<int64(IntegerVariable*)>& evaluator) {
327 const int64 count = ComputeCount(ct, evaluator);
328 const int64 expected = Eval(ct.arguments[2], evaluator);
329 const int64 status = Eval(ct.arguments[3], evaluator);
330 return status == (expected == count);
331}
332
333bool CheckCumulative(const Constraint& ct,
334 const std::function<int64(IntegerVariable*)>& evaluator) {
335 // TODO(user): Improve complexity for large durations.
336 const int64 capacity = Eval(ct.arguments[3], evaluator);
337 const int size = Size(ct.arguments[0]);
338 CHECK_EQ(size, Size(ct.arguments[1]));
339 CHECK_EQ(size, Size(ct.arguments[2]));
340 absl::flat_hash_map<int64, int64> usage;
341 for (int i = 0; i < size; ++i) {
342 const int64 start = EvalAt(ct.arguments[0], i, evaluator);
343 const int64 duration = EvalAt(ct.arguments[1], i, evaluator);
344 const int64 requirement = EvalAt(ct.arguments[2], i, evaluator);
345 for (int64 t = start; t < start + duration; ++t) {
346 usage[t] += requirement;
347 if (usage[t] > capacity) {
348 return false;
349 }
350 }
351 }
352 return true;
353}
354
355bool CheckDiffn(const Constraint& ct,
356 const std::function<int64(IntegerVariable*)>& evaluator) {
357 return true;
358}
359
360bool CheckDiffnK(const Constraint& ct,
361 const std::function<int64(IntegerVariable*)>& evaluator) {
362 return true;
363}
364
365bool CheckDiffnNonStrict(
366 const Constraint& ct,
367 const std::function<int64(IntegerVariable*)>& evaluator) {
368 return true;
369}
370
371bool CheckDiffnNonStrictK(
372 const Constraint& ct,
373 const std::function<int64(IntegerVariable*)>& evaluator) {
374 return true;
375}
376
377bool CheckDisjunctive(const Constraint& ct,
378 const std::function<int64(IntegerVariable*)>& evaluator) {
379 return true;
380}
381
382bool CheckDisjunctiveStrict(
383 const Constraint& ct,
384 const std::function<int64(IntegerVariable*)>& evaluator) {
385 return true;
386}
387
388bool CheckFalseConstraint(
389 const Constraint& ct,
390 const std::function<int64(IntegerVariable*)>& evaluator) {
391 return false;
392}
393
394std::vector<int64> ComputeGlobalCardinalityCards(
395 const Constraint& ct,
396 const std::function<int64(IntegerVariable*)>& evaluator) {
397 std::vector<int64> cards(Size(ct.arguments[1]), 0);
398 absl::flat_hash_map<int64, int> positions;
399 for (int i = 0; i < ct.arguments[1].values.size(); ++i) {
400 const int64 value = ct.arguments[1].values[i];
401 CHECK(!gtl::ContainsKey(positions, value));
402 positions[value] = i;
403 }
404 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
405 const int value = EvalAt(ct.arguments[0], i, evaluator);
406 if (gtl::ContainsKey(positions, value)) {
407 cards[positions[value]]++;
408 }
409 }
410 return cards;
411}
412
413bool CheckGlobalCardinality(
414 const Constraint& ct,
415 const std::function<int64(IntegerVariable*)>& evaluator) {
416 const std::vector<int64> cards = ComputeGlobalCardinalityCards(ct, evaluator);
417 CHECK_EQ(cards.size(), Size(ct.arguments[2]));
418 for (int i = 0; i < Size(ct.arguments[2]); ++i) {
419 const int64 card = EvalAt(ct.arguments[2], i, evaluator);
420 if (card != cards[i]) {
421 return false;
422 }
423 }
424 return true;
425}
426
427bool CheckGlobalCardinalityClosed(
428 const Constraint& ct,
429 const std::function<int64(IntegerVariable*)>& evaluator) {
430 const std::vector<int64> cards = ComputeGlobalCardinalityCards(ct, evaluator);
431 CHECK_EQ(cards.size(), Size(ct.arguments[2]));
432 for (int i = 0; i < Size(ct.arguments[2]); ++i) {
433 const int64 card = EvalAt(ct.arguments[2], i, evaluator);
434 if (card != cards[i]) {
435 return false;
436 }
437 }
438 int64 sum_of_cards = 0;
439 for (int64 card : cards) {
440 sum_of_cards += card;
441 }
442 return sum_of_cards == Size(ct.arguments[0]);
443}
444
445bool CheckGlobalCardinalityLowUp(
446 const Constraint& ct,
447 const std::function<int64(IntegerVariable*)>& evaluator) {
448 const std::vector<int64> cards = ComputeGlobalCardinalityCards(ct, evaluator);
449 CHECK_EQ(cards.size(), ct.arguments[2].values.size());
450 CHECK_EQ(cards.size(), ct.arguments[3].values.size());
451 for (int i = 0; i < cards.size(); ++i) {
452 const int64 card = cards[i];
453 if (card < ct.arguments[2].values[i] || card > ct.arguments[3].values[i]) {
454 return false;
455 }
456 }
457 return true;
458}
459
460bool CheckGlobalCardinalityLowUpClosed(
461 const Constraint& ct,
462 const std::function<int64(IntegerVariable*)>& evaluator) {
463 const std::vector<int64> cards = ComputeGlobalCardinalityCards(ct, evaluator);
464 CHECK_EQ(cards.size(), ct.arguments[2].values.size());
465 CHECK_EQ(cards.size(), ct.arguments[3].values.size());
466 for (int i = 0; i < cards.size(); ++i) {
467 const int64 card = cards[i];
468 if (card < ct.arguments[2].values[i] || card > ct.arguments[3].values[i]) {
469 return false;
470 }
471 }
472 int64 sum_of_cards = 0;
473 for (int64 card : cards) {
474 sum_of_cards += card;
475 }
476 return sum_of_cards == Size(ct.arguments[0]);
477}
478
479bool CheckGlobalCardinalityOld(
480 const Constraint& ct,
481 const std::function<int64(IntegerVariable*)>& evaluator) {
482 const int size = Size(ct.arguments[1]);
483 std::vector<int64> cards(size, 0);
484 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
485 const int64 value = EvalAt(ct.arguments[0], i, evaluator);
486 if (value >= 0 && value < size) {
487 cards[value]++;
488 }
489 }
490 for (int i = 0; i < size; ++i) {
491 const int64 card = EvalAt(ct.arguments[1], i, evaluator);
492 if (card != cards[i]) {
493 return false;
494 }
495 }
496 return true;
497}
498
499bool CheckIntAbs(const Constraint& ct,
500 const std::function<int64(IntegerVariable*)>& evaluator) {
501 const int64 left = Eval(ct.arguments[0], evaluator);
502 const int64 right = Eval(ct.arguments[1], evaluator);
503 return std::abs(left) == right;
504}
505
506bool CheckIntDiv(const Constraint& ct,
507 const std::function<int64(IntegerVariable*)>& evaluator) {
508 const int64 left = Eval(ct.arguments[0], evaluator);
509 const int64 right = Eval(ct.arguments[1], evaluator);
510 const int64 target = Eval(ct.arguments[2], evaluator);
511 return target == left / right;
512}
513
514bool CheckIntEq(const Constraint& ct,
515 const std::function<int64(IntegerVariable*)>& evaluator) {
516 const int64 left = Eval(ct.arguments[0], evaluator);
517 const int64 right = Eval(ct.arguments[1], evaluator);
518 return left == right;
519}
520
521bool CheckIntEqImp(const Constraint& ct,
522 const std::function<int64(IntegerVariable*)>& evaluator) {
523 const int64 left = Eval(ct.arguments[0], evaluator);
524 const int64 right = Eval(ct.arguments[1], evaluator);
525 const bool status = Eval(ct.arguments[2], evaluator) != 0;
526 return (status && (left == right)) || !status;
527}
528
529bool CheckIntEqReif(const Constraint& ct,
530 const std::function<int64(IntegerVariable*)>& evaluator) {
531 const int64 left = Eval(ct.arguments[0], evaluator);
532 const int64 right = Eval(ct.arguments[1], evaluator);
533 const bool status = Eval(ct.arguments[2], evaluator) != 0;
534 return status == (left == right);
535}
536
537bool CheckIntGe(const Constraint& ct,
538 const std::function<int64(IntegerVariable*)>& evaluator) {
539 const int64 left = Eval(ct.arguments[0], evaluator);
540 const int64 right = Eval(ct.arguments[1], evaluator);
541 return left >= right;
542}
543
544bool CheckIntGeImp(const Constraint& ct,
545 const std::function<int64(IntegerVariable*)>& evaluator) {
546 const int64 left = Eval(ct.arguments[0], evaluator);
547 const int64 right = Eval(ct.arguments[1], evaluator);
548 const bool status = Eval(ct.arguments[2], evaluator) != 0;
549 return (status && (left >= right)) || !status;
550}
551
552bool CheckIntGeReif(const Constraint& ct,
553 const std::function<int64(IntegerVariable*)>& evaluator) {
554 const int64 left = Eval(ct.arguments[0], evaluator);
555 const int64 right = Eval(ct.arguments[1], evaluator);
556 const bool status = Eval(ct.arguments[2], evaluator) != 0;
557 return status == (left >= right);
558}
559
560bool CheckIntGt(const Constraint& ct,
561 const std::function<int64(IntegerVariable*)>& evaluator) {
562 const int64 left = Eval(ct.arguments[0], evaluator);
563 const int64 right = Eval(ct.arguments[1], evaluator);
564 return left > right;
565}
566
567bool CheckIntGtImp(const Constraint& ct,
568 const std::function<int64(IntegerVariable*)>& evaluator) {
569 const int64 left = Eval(ct.arguments[0], evaluator);
570 const int64 right = Eval(ct.arguments[1], evaluator);
571 const bool status = Eval(ct.arguments[2], evaluator) != 0;
572 return (status && (left > right)) || !status;
573}
574
575bool CheckIntGtReif(const Constraint& ct,
576 const std::function<int64(IntegerVariable*)>& evaluator) {
577 const int64 left = Eval(ct.arguments[0], evaluator);
578 const int64 right = Eval(ct.arguments[1], evaluator);
579 const bool status = Eval(ct.arguments[2], evaluator) != 0;
580 return status == (left > right);
581}
582
583bool CheckIntLe(const Constraint& ct,
584 const std::function<int64(IntegerVariable*)>& evaluator) {
585 const int64 left = Eval(ct.arguments[0], evaluator);
586 const int64 right = Eval(ct.arguments[1], evaluator);
587 return left <= right;
588}
589
590bool CheckIntLeImp(const Constraint& ct,
591 const std::function<int64(IntegerVariable*)>& evaluator) {
592 const int64 left = Eval(ct.arguments[0], evaluator);
593 const int64 right = Eval(ct.arguments[1], evaluator);
594 const bool status = Eval(ct.arguments[2], evaluator) != 0;
595 return (status && (left <= right)) || !status;
596}
597
598bool CheckIntLeReif(const Constraint& ct,
599 const std::function<int64(IntegerVariable*)>& evaluator) {
600 const int64 left = Eval(ct.arguments[0], evaluator);
601 const int64 right = Eval(ct.arguments[1], evaluator);
602 const bool status = Eval(ct.arguments[2], evaluator) != 0;
603 return status == (left <= right);
604}
605
606bool CheckIntLt(const Constraint& ct,
607 const std::function<int64(IntegerVariable*)>& evaluator) {
608 const int64 left = Eval(ct.arguments[0], evaluator);
609 const int64 right = Eval(ct.arguments[1], evaluator);
610 return left < right;
611}
612
613bool CheckIntLtImp(const Constraint& ct,
614 const std::function<int64(IntegerVariable*)>& evaluator) {
615 const int64 left = Eval(ct.arguments[0], evaluator);
616 const int64 right = Eval(ct.arguments[1], evaluator);
617 const bool status = Eval(ct.arguments[2], evaluator) != 0;
618 return (status && (left < right)) || !status;
619}
620
621bool CheckIntLtReif(const Constraint& ct,
622 const std::function<int64(IntegerVariable*)>& evaluator) {
623 const int64 left = Eval(ct.arguments[0], evaluator);
624 const int64 right = Eval(ct.arguments[1], evaluator);
625 const bool status = Eval(ct.arguments[2], evaluator) != 0;
626 return status == (left < right);
627}
628
629int64 ComputeIntLin(const Constraint& ct,
630 const std::function<int64(IntegerVariable*)>& evaluator) {
631 int64 result = 0;
632 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
633 result += EvalAt(ct.arguments[0], i, evaluator) *
634 EvalAt(ct.arguments[1], i, evaluator);
635 }
636 return result;
637}
638
639bool CheckIntLinEq(const Constraint& ct,
640 const std::function<int64(IntegerVariable*)>& evaluator) {
641 const int64 left = ComputeIntLin(ct, evaluator);
642 const int64 right = Eval(ct.arguments[2], evaluator);
643 return left == right;
644}
645
646bool CheckIntLinEqImp(const Constraint& ct,
647 const std::function<int64(IntegerVariable*)>& evaluator) {
648 const int64 left = ComputeIntLin(ct, evaluator);
649 const int64 right = Eval(ct.arguments[2], evaluator);
650 const bool status = Eval(ct.arguments[3], evaluator) != 0;
651 return (status && (left == right)) || !status;
652}
653
654bool CheckIntLinEqReif(
655 const Constraint& ct,
656 const std::function<int64(IntegerVariable*)>& evaluator) {
657 const int64 left = ComputeIntLin(ct, evaluator);
658 const int64 right = Eval(ct.arguments[2], evaluator);
659 const bool status = Eval(ct.arguments[3], evaluator) != 0;
660 return status == (left == right);
661}
662
663bool CheckIntLinGe(const Constraint& ct,
664 const std::function<int64(IntegerVariable*)>& evaluator) {
665 const int64 left = ComputeIntLin(ct, evaluator);
666 const int64 right = Eval(ct.arguments[2], evaluator);
667 return left >= right;
668}
669
670bool CheckIntLinGeImp(const Constraint& ct,
671 const std::function<int64(IntegerVariable*)>& evaluator) {
672 const int64 left = ComputeIntLin(ct, evaluator);
673 const int64 right = Eval(ct.arguments[2], evaluator);
674 const bool status = Eval(ct.arguments[3], evaluator) != 0;
675 return (status && (left >= right)) || !status;
676}
677
678bool CheckIntLinGeReif(
679 const Constraint& ct,
680 const std::function<int64(IntegerVariable*)>& evaluator) {
681 const int64 left = ComputeIntLin(ct, evaluator);
682 const int64 right = Eval(ct.arguments[2], evaluator);
683 const bool status = Eval(ct.arguments[3], evaluator) != 0;
684 return status == (left >= right);
685}
686
687bool CheckIntLinLe(const Constraint& ct,
688 const std::function<int64(IntegerVariable*)>& evaluator) {
689 const int64 left = ComputeIntLin(ct, evaluator);
690 const int64 right = Eval(ct.arguments[2], evaluator);
691 return left <= right;
692}
693
694bool CheckIntLinLeImp(const Constraint& ct,
695 const std::function<int64(IntegerVariable*)>& evaluator) {
696 const int64 left = ComputeIntLin(ct, evaluator);
697 const int64 right = Eval(ct.arguments[2], evaluator);
698 const bool status = Eval(ct.arguments[3], evaluator) != 0;
699 return (status && (left <= right)) || !status;
700}
701
702bool CheckIntLinLeReif(
703 const Constraint& ct,
704 const std::function<int64(IntegerVariable*)>& evaluator) {
705 const int64 left = ComputeIntLin(ct, evaluator);
706 const int64 right = Eval(ct.arguments[2], evaluator);
707 const bool status = Eval(ct.arguments[3], evaluator) != 0;
708 return status == (left <= right);
709}
710
711bool CheckIntLinNe(const Constraint& ct,
712 const std::function<int64(IntegerVariable*)>& evaluator) {
713 const int64 left = ComputeIntLin(ct, evaluator);
714 const int64 right = Eval(ct.arguments[2], evaluator);
715 return left != right;
716}
717
718bool CheckIntLinNeImp(const Constraint& ct,
719 const std::function<int64(IntegerVariable*)>& evaluator) {
720 const int64 left = ComputeIntLin(ct, evaluator);
721 const int64 right = Eval(ct.arguments[2], evaluator);
722 const bool status = Eval(ct.arguments[3], evaluator) != 0;
723 return (status && (left != right)) || !status;
724}
725
726bool CheckIntLinNeReif(
727 const Constraint& ct,
728 const std::function<int64(IntegerVariable*)>& evaluator) {
729 const int64 left = ComputeIntLin(ct, evaluator);
730 const int64 right = Eval(ct.arguments[2], evaluator);
731 const bool status = Eval(ct.arguments[3], evaluator) != 0;
732 return status == (left != right);
733}
734
735bool CheckIntMax(const Constraint& ct,
736 const std::function<int64(IntegerVariable*)>& evaluator) {
737 const int64 left = Eval(ct.arguments[0], evaluator);
738 const int64 right = Eval(ct.arguments[1], evaluator);
739 const int64 status = Eval(ct.arguments[2], evaluator);
740 return status == std::max(left, right);
741}
742
743bool CheckIntMin(const Constraint& ct,
744 const std::function<int64(IntegerVariable*)>& evaluator) {
745 const int64 left = Eval(ct.arguments[0], evaluator);
746 const int64 right = Eval(ct.arguments[1], evaluator);
747 const int64 status = Eval(ct.arguments[2], evaluator);
748 return status == std::min(left, right);
749}
750
751bool CheckIntMinus(const Constraint& ct,
752 const std::function<int64(IntegerVariable*)>& evaluator) {
753 const int64 left = Eval(ct.arguments[0], evaluator);
754 const int64 right = Eval(ct.arguments[1], evaluator);
755 const int64 target = Eval(ct.arguments[2], evaluator);
756 return target == left - right;
757}
758
759bool CheckIntMod(const Constraint& ct,
760 const std::function<int64(IntegerVariable*)>& evaluator) {
761 const int64 left = Eval(ct.arguments[0], evaluator);
762 const int64 right = Eval(ct.arguments[1], evaluator);
763 const int64 target = Eval(ct.arguments[2], evaluator);
764 return target == left % right;
765}
766
767bool CheckIntNe(const Constraint& ct,
768 const std::function<int64(IntegerVariable*)>& evaluator) {
769 const int64 left = Eval(ct.arguments[0], evaluator);
770 const int64 right = Eval(ct.arguments[1], evaluator);
771 return left != right;
772}
773
774bool CheckIntNeImp(const Constraint& ct,
775 const std::function<int64(IntegerVariable*)>& evaluator) {
776 const int64 left = Eval(ct.arguments[0], evaluator);
777 const int64 right = Eval(ct.arguments[1], evaluator);
778 const bool status = Eval(ct.arguments[2], evaluator) != 0;
779 return (status && (left != right)) || !status;
780}
781
782bool CheckIntNeReif(const Constraint& ct,
783 const std::function<int64(IntegerVariable*)>& evaluator) {
784 const int64 left = Eval(ct.arguments[0], evaluator);
785 const int64 right = Eval(ct.arguments[1], evaluator);
786 const bool status = Eval(ct.arguments[2], evaluator) != 0;
787 return status == (left != right);
788}
789
790bool CheckIntNegate(const Constraint& ct,
791 const std::function<int64(IntegerVariable*)>& evaluator) {
792 const int64 left = Eval(ct.arguments[0], evaluator);
793 const int64 right = Eval(ct.arguments[1], evaluator);
794 return left == -right;
795}
796
797bool CheckIntPlus(const Constraint& ct,
798 const std::function<int64(IntegerVariable*)>& evaluator) {
799 const int64 left = Eval(ct.arguments[0], evaluator);
800 const int64 right = Eval(ct.arguments[1], evaluator);
801 const int64 target = Eval(ct.arguments[2], evaluator);
802 return target == left + right;
803}
804
805bool CheckIntTimes(const Constraint& ct,
806 const std::function<int64(IntegerVariable*)>& evaluator) {
807 const int64 left = Eval(ct.arguments[0], evaluator);
808 const int64 right = Eval(ct.arguments[1], evaluator);
809 const int64 target = Eval(ct.arguments[2], evaluator);
810 return target == left * right;
811}
812
813bool CheckInverse(const Constraint& ct,
814 const std::function<int64(IntegerVariable*)>& evaluator) {
815 CHECK_EQ(Size(ct.arguments[0]), Size(ct.arguments[1]));
816 const int size = Size(ct.arguments[0]);
817 // Check all bounds.
818 for (int i = 0; i < size; ++i) {
819 const int64 x = EvalAt(ct.arguments[0], i, evaluator) - 1;
820 const int64 y = EvalAt(ct.arguments[1], i, evaluator) - 1;
821 if (x < 0 || x >= size || y < 0 || y >= size) {
822 return false;
823 }
824 }
825 // Check f-1(f(i)) = i.
826 for (int i = 0; i < size; ++i) {
827 const int64 fi = EvalAt(ct.arguments[0], i, evaluator) - 1;
828 const int64 invf_fi = EvalAt(ct.arguments[1], fi, evaluator) - 1;
829 if (invf_fi != i) {
830 return false;
831 }
832 }
833
834 return true;
835}
836
837bool CheckLexLessInt(const Constraint& ct,
838 const std::function<int64(IntegerVariable*)>& evaluator) {
839 CHECK_EQ(Size(ct.arguments[0]), Size(ct.arguments[1]));
840 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
841 const int64 x = EvalAt(ct.arguments[0], i, evaluator);
842 const int64 y = EvalAt(ct.arguments[1], i, evaluator);
843 if (x < y) {
844 return true;
845 }
846 if (x > y) {
847 return false;
848 }
849 }
850 // We are at the end of the list. The two chains are equals.
851 return false;
852}
853
854bool CheckLexLesseqInt(
855 const Constraint& ct,
856 const std::function<int64(IntegerVariable*)>& evaluator) {
857 CHECK_EQ(Size(ct.arguments[0]), Size(ct.arguments[1]));
858 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
859 const int64 x = EvalAt(ct.arguments[0], i, evaluator);
860 const int64 y = EvalAt(ct.arguments[1], i, evaluator);
861 if (x < y) {
862 return true;
863 }
864 if (x > y) {
865 return false;
866 }
867 }
868 // We are at the end of the list. The two chains are equals.
869 return true;
870}
871
872bool CheckMaximumArgInt(
873 const Constraint& ct,
874 const std::function<int64(IntegerVariable*)>& evaluator) {
875 const int64 max_index = Eval(ct.arguments[1], evaluator) - 1;
876 const int64 max_value = EvalAt(ct.arguments[0], max_index, evaluator);
877 // Checks that all value before max_index are < max_value.
878 for (int i = 0; i < max_index; ++i) {
879 if (EvalAt(ct.arguments[0], i, evaluator) >= max_value) {
880 return false;
881 }
882 }
883 // Checks that all value after max_index are <= max_value.
884 for (int i = max_index + 1; i < Size(ct.arguments[0]); i++) {
885 if (EvalAt(ct.arguments[0], i, evaluator) > max_value) {
886 return false;
887 }
888 }
889
890 return true;
891}
892
893bool CheckMaximumInt(const Constraint& ct,
894 const std::function<int64(IntegerVariable*)>& evaluator) {
895 int64 max_value = kint64min;
896 for (int i = 0; i < Size(ct.arguments[1]); ++i) {
897 max_value = std::max(max_value, EvalAt(ct.arguments[1], i, evaluator));
898 }
899 return max_value == Eval(ct.arguments[0], evaluator);
900}
901
902bool CheckMinimumArgInt(
903 const Constraint& ct,
904 const std::function<int64(IntegerVariable*)>& evaluator) {
905 const int64 min_index = Eval(ct.arguments[1], evaluator) - 1;
906 const int64 min_value = EvalAt(ct.arguments[0], min_index, evaluator);
907 // Checks that all value before min_index are > min_value.
908 for (int i = 0; i < min_index; ++i) {
909 if (EvalAt(ct.arguments[0], i, evaluator) <= min_value) {
910 return false;
911 }
912 }
913 // Checks that all value after min_index are >= min_value.
914 for (int i = min_index + 1; i < Size(ct.arguments[0]); i++) {
915 if (EvalAt(ct.arguments[0], i, evaluator) < min_value) {
916 return false;
917 }
918 }
919
920 return true;
921}
922
923bool CheckMinimumInt(const Constraint& ct,
924 const std::function<int64(IntegerVariable*)>& evaluator) {
925 int64 min_value = kint64max;
926 for (int i = 0; i < Size(ct.arguments[1]); ++i) {
927 min_value = std::min(min_value, EvalAt(ct.arguments[1], i, evaluator));
928 }
929 return min_value == Eval(ct.arguments[0], evaluator);
930}
931
932bool CheckNetworkFlowConservation(
933 const Argument& arcs, const Argument& balance_input,
934 const Argument& flow_vars,
935 const std::function<int64(IntegerVariable*)>& evaluator) {
936 std::vector<int64> balance(balance_input.values);
937
938 const int num_arcs = Size(arcs) / 2;
939 for (int arc = 0; arc < num_arcs; arc++) {
940 const int tail = arcs.values[arc * 2] - 1;
941 const int head = arcs.values[arc * 2 + 1] - 1;
942 const int64 flow = EvalAt(flow_vars, arc, evaluator);
943 balance[tail] -= flow;
944 balance[head] += flow;
945 }
946
947 for (const int64 value : balance) {
948 if (value != 0) return false;
949 }
950
951 return true;
952}
953
954bool CheckNetworkFlow(const Constraint& ct,
955 const std::function<int64(IntegerVariable*)>& evaluator) {
956 return CheckNetworkFlowConservation(ct.arguments[0], ct.arguments[1],
957 ct.arguments[2], evaluator);
958}
959
960bool CheckNetworkFlowCost(
961 const Constraint& ct,
962 const std::function<int64(IntegerVariable*)>& evaluator) {
963 if (!CheckNetworkFlowConservation(ct.arguments[0], ct.arguments[1],
964 ct.arguments[3], evaluator)) {
965 return false;
966 }
967
968 int64 total_cost = 0;
969 const int num_arcs = Size(ct.arguments[3]);
970 for (int arc = 0; arc < num_arcs; arc++) {
971 const int64 flow = EvalAt(ct.arguments[3], arc, evaluator);
972 const int64 cost = EvalAt(ct.arguments[2], arc, evaluator);
973 total_cost += flow * cost;
974 }
975
976 return total_cost == Eval(ct.arguments[4], evaluator);
977}
978
979bool CheckNvalue(const Constraint& ct,
980 const std::function<int64(IntegerVariable*)>& evaluator) {
981 const int64 count = Eval(ct.arguments[0], evaluator);
982 absl::flat_hash_set<int64> all_values;
983 for (int i = 0; i < Size(ct.arguments[1]); ++i) {
984 all_values.insert(EvalAt(ct.arguments[1], i, evaluator));
985 }
986
987 return count == all_values.size();
988}
989
990bool CheckRegular(const Constraint& ct,
991 const std::function<int64(IntegerVariable*)>& evaluator) {
992 return true;
993}
994
995bool CheckRegularNfa(const Constraint& ct,
996 const std::function<int64(IntegerVariable*)>& evaluator) {
997 return true;
998}
999
1000bool CheckSetIn(const Constraint& ct,
1001 const std::function<int64(IntegerVariable*)>& evaluator) {
1002 const int64 value = Eval(ct.arguments[0], evaluator);
1003 return ct.arguments[1].Contains(value);
1004}
1005
1006bool CheckSetNotIn(const Constraint& ct,
1007 const std::function<int64(IntegerVariable*)>& evaluator) {
1008 const int64 value = Eval(ct.arguments[0], evaluator);
1009 return !ct.arguments[1].Contains(value);
1010}
1011
1012bool CheckSetInReif(const Constraint& ct,
1013 const std::function<int64(IntegerVariable*)>& evaluator) {
1014 const int64 value = Eval(ct.arguments[0], evaluator);
1015 const int64 status = Eval(ct.arguments[2], evaluator);
1016 return status == ct.arguments[1].Contains(value);
1017}
1018
1019bool CheckSlidingSum(const Constraint& ct,
1020 const std::function<int64(IntegerVariable*)>& evaluator) {
1021 const int64 low = Eval(ct.arguments[0], evaluator);
1022 const int64 up = Eval(ct.arguments[1], evaluator);
1023 const int64 length = Eval(ct.arguments[2], evaluator);
1024 // Compute initial sum.
1025 int64 sliding_sum = 0;
1026 for (int i = 0; i < std::min<int64>(length, Size(ct.arguments[3])); ++i) {
1027 sliding_sum += EvalAt(ct.arguments[3], i, evaluator);
1028 }
1029 if (sliding_sum < low || sliding_sum > up) {
1030 return false;
1031 }
1032 for (int i = length; i < Size(ct.arguments[3]); ++i) {
1033 sliding_sum += EvalAt(ct.arguments[3], i, evaluator) -
1034 EvalAt(ct.arguments[3], i - length, evaluator);
1035 if (sliding_sum < low || sliding_sum > up) {
1036 return false;
1037 }
1038 }
1039 return true;
1040}
1041
1042bool CheckSort(const Constraint& ct,
1043 const std::function<int64(IntegerVariable*)>& evaluator) {
1044 CHECK_EQ(Size(ct.arguments[0]), Size(ct.arguments[1]));
1045 absl::flat_hash_map<int64, int> init_count;
1046 absl::flat_hash_map<int64, int> sorted_count;
1047 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
1048 init_count[EvalAt(ct.arguments[0], i, evaluator)]++;
1049 sorted_count[EvalAt(ct.arguments[1], i, evaluator)]++;
1050 }
1051 if (init_count != sorted_count) {
1052 return false;
1053 }
1054 for (int i = 0; i < Size(ct.arguments[1]) - 1; ++i) {
1055 if (EvalAt(ct.arguments[1], i, evaluator) >
1056 EvalAt(ct.arguments[1], i, evaluator)) {
1057 return false;
1058 }
1059 }
1060 return true;
1061}
1062
1063bool CheckSubCircuit(const Constraint& ct,
1064 const std::function<int64(IntegerVariable*)>& evaluator) {
1065 absl::flat_hash_set<int64> visited;
1066 // Find inactive nodes (pointing to themselves).
1067 int64 current = -1;
1068 for (int i = 0; i < Size(ct.arguments[0]); ++i) {
1069 const int64 next = EvalAt(ct.arguments[0], i, evaluator) - 1;
1070 if (next != i && current == -1) {
1071 current = next;
1072 } else if (next == i) {
1073 visited.insert(next);
1074 }
1075 }
1076
1077 // Try to find a path of length 'residual_size'.
1078 const int residual_size = Size(ct.arguments[0]) - visited.size();
1079 for (int i = 0; i < residual_size; ++i) {
1080 const int64 next = EvalAt(ct.arguments[0], current, evaluator) - 1;
1081 visited.insert(next);
1082 if (next == current) {
1083 return false;
1084 }
1085 current = next;
1086 }
1087
1088 // Have we visited all nodes?
1089 return visited.size() == Size(ct.arguments[0]);
1090}
1091
1092bool CheckTableInt(const Constraint& ct,
1093 const std::function<int64(IntegerVariable*)>& evaluator) {
1094 return true;
1095}
1096
1097bool CheckSymmetricAllDifferent(
1098 const Constraint& ct,
1099 const std::function<int64(IntegerVariable*)>& evaluator) {
1100 const int size = Size(ct.arguments[0]);
1101 for (int i = 0; i < size; ++i) {
1102 const int64 value = EvalAt(ct.arguments[0], i, evaluator) - 1;
1103 if (value < 0 || value >= size) {
1104 return false;
1105 }
1106 const int64 reverse_value = EvalAt(ct.arguments[0], value, evaluator) - 1;
1107 if (reverse_value != i) {
1108 return false;
1109 }
1110 }
1111 return true;
1112}
1113
1114using CallMap = absl::flat_hash_map<
1115 std::string, std::function<bool(const Constraint& ct,
1116 std::function<int64(IntegerVariable*)>)>>;
1117
1118// Creates a map between flatzinc predicates and CP-SAT builders.
1119//
1120// Predicates starting with fzn_ are predicates with the same name in flatzinc
1121// and in minizinc. The fzn_ prefix is added to differentiate them.
1122//
1123// Predicates starting with ortools_ are predicates defined only in or-tools.
1124// They are created at compilation time when using the or-tools mzn library.
1125CallMap CreateCallMap() {
1126 CallMap m;
1127 m["fzn_all_different_int"] = CheckAllDifferentInt;
1128 m["alldifferent_except_0"] = CheckAlldifferentExcept0;
1129 m["among"] = CheckAmong;
1130 m["array_bool_and"] = CheckArrayBoolAnd;
1131 m["array_bool_element"] = CheckArrayIntElement;
1132 m["array_bool_or"] = CheckArrayBoolOr;
1133 m["array_bool_xor"] = CheckArrayBoolXor;
1134 m["array_int_element"] = CheckArrayIntElement;
1135 m["array_int_element_nonshifted"] = CheckArrayIntElementNonShifted;
1136 m["array_var_bool_element"] = CheckArrayVarIntElement;
1137 m["array_var_int_element"] = CheckArrayVarIntElement;
1138 m["at_most_int"] = CheckAtMostInt;
1139 m["bool_and"] = CheckBoolAnd;
1140 m["bool_clause"] = CheckBoolClause;
1141 m["bool_eq"] = CheckIntEq;
1142 m["bool2int"] = CheckIntEq;
1143 m["bool_eq_imp"] = CheckIntEqImp;
1144 m["bool_eq_reif"] = CheckIntEqReif;
1145 m["bool_ge"] = CheckIntGe;
1146 m["bool_ge_imp"] = CheckIntGeImp;
1147 m["bool_ge_reif"] = CheckIntGeReif;
1148 m["bool_gt"] = CheckIntGt;
1149 m["bool_gt_imp"] = CheckIntGtImp;
1150 m["bool_gt_reif"] = CheckIntGtReif;
1151 m["bool_le"] = CheckIntLe;
1152 m["bool_le_imp"] = CheckIntLeImp;
1153 m["bool_le_reif"] = CheckIntLeReif;
1154 m["bool_left_imp"] = CheckIntLe;
1155 m["bool_lin_eq"] = CheckIntLinEq;
1156 m["bool_lin_le"] = CheckIntLinLe;
1157 m["bool_lt"] = CheckIntLt;
1158 m["bool_lt_imp"] = CheckIntLtImp;
1159 m["bool_lt_reif"] = CheckIntLtReif;
1160 m["bool_ne"] = CheckIntNe;
1161 m["bool_ne_imp"] = CheckIntNeImp;
1162 m["bool_ne_reif"] = CheckIntNeReif;
1163 m["bool_not"] = CheckBoolNot;
1164 m["bool_or"] = CheckBoolOr;
1165 m["bool_right_imp"] = CheckIntGe;
1166 m["bool_xor"] = CheckBoolXor;
1167 m["fzn_circuit"] = CheckCircuit;
1168 m["count_eq"] = CheckCountEq;
1169 m["count"] = CheckCountEq;
1170 m["count_geq"] = CheckCountGeq;
1171 m["count_gt"] = CheckCountGt;
1172 m["count_leq"] = CheckCountLeq;
1173 m["count_lt"] = CheckCountLt;
1174 m["count_neq"] = CheckCountNeq;
1175 m["count_reif"] = CheckCountReif;
1176 m["fzn_cumulative"] = CheckCumulative;
1177 m["var_cumulative"] = CheckCumulative;
1178 m["variable_cumulative"] = CheckCumulative;
1179 m["fixed_cumulative"] = CheckCumulative;
1180 m["fzn_diffn"] = CheckDiffn;
1181 m["diffn_k_with_sizes"] = CheckDiffnK;
1182 m["fzn_diffn_nonstrict"] = CheckDiffnNonStrict;
1183 m["diffn_nonstrict_k_with_sizes"] = CheckDiffnNonStrictK;
1184 m["disjunctive"] = CheckDisjunctive;
1185 m["disjunctive_strict"] = CheckDisjunctiveStrict;
1186 m["false_constraint"] = CheckFalseConstraint;
1187 m["global_cardinality"] = CheckGlobalCardinality;
1188 m["global_cardinality_closed"] = CheckGlobalCardinalityClosed;
1189 m["global_cardinality_low_up"] = CheckGlobalCardinalityLowUp;
1190 m["global_cardinality_low_up_closed"] = CheckGlobalCardinalityLowUpClosed;
1191 m["global_cardinality_old"] = CheckGlobalCardinalityOld;
1192 m["int_abs"] = CheckIntAbs;
1193 m["int_div"] = CheckIntDiv;
1194 m["int_eq"] = CheckIntEq;
1195 m["int_eq_imp"] = CheckIntEqImp;
1196 m["int_eq_reif"] = CheckIntEqReif;
1197 m["int_ge"] = CheckIntGe;
1198 m["int_ge_imp"] = CheckIntGeImp;
1199 m["int_ge_reif"] = CheckIntGeReif;
1200 m["int_gt"] = CheckIntGt;
1201 m["int_gt_imp"] = CheckIntGtImp;
1202 m["int_gt_reif"] = CheckIntGtReif;
1203 m["int_le"] = CheckIntLe;
1204 m["int_le_imp"] = CheckIntLeImp;
1205 m["int_le_reif"] = CheckIntLeReif;
1206 m["int_lin_eq"] = CheckIntLinEq;
1207 m["int_lin_eq_imp"] = CheckIntLinEqImp;
1208 m["int_lin_eq_reif"] = CheckIntLinEqReif;
1209 m["int_lin_ge"] = CheckIntLinGe;
1210 m["int_lin_ge_imp"] = CheckIntLinGeImp;
1211 m["int_lin_ge_reif"] = CheckIntLinGeReif;
1212 m["int_lin_le"] = CheckIntLinLe;
1213 m["int_lin_le_imp"] = CheckIntLinLeImp;
1214 m["int_lin_le_reif"] = CheckIntLinLeReif;
1215 m["int_lin_ne"] = CheckIntLinNe;
1216 m["int_lin_ne_imp"] = CheckIntLinNeImp;
1217 m["int_lin_ne_reif"] = CheckIntLinNeReif;
1218 m["int_lt"] = CheckIntLt;
1219 m["int_lt_imp"] = CheckIntLtImp;
1220 m["int_lt_reif"] = CheckIntLtReif;
1221 m["int_max"] = CheckIntMax;
1222 m["int_min"] = CheckIntMin;
1223 m["int_minus"] = CheckIntMinus;
1224 m["int_mod"] = CheckIntMod;
1225 m["int_ne"] = CheckIntNe;
1226 m["int_ne_imp"] = CheckIntNeImp;
1227 m["int_ne_reif"] = CheckIntNeReif;
1228 m["int_negate"] = CheckIntNegate;
1229 m["int_plus"] = CheckIntPlus;
1230 m["int_times"] = CheckIntTimes;
1231 m["fzn_inverse"] = CheckInverse;
1232 m["lex_less_bool"] = CheckLexLessInt;
1233 m["lex_less_int"] = CheckLexLessInt;
1234 m["lex_lesseq_bool"] = CheckLexLesseqInt;
1235 m["lex_lesseq_int"] = CheckLexLesseqInt;
1236 m["maximum_arg_int"] = CheckMaximumArgInt;
1237 m["maximum_int"] = CheckMaximumInt;
1238 m["array_int_maximum"] = CheckMaximumInt;
1239 m["minimum_arg_int"] = CheckMinimumArgInt;
1240 m["minimum_int"] = CheckMinimumInt;
1241 m["array_int_minimum"] = CheckMinimumInt;
1242 m["ortools_network_flow"] = CheckNetworkFlow;
1243 m["ortools_network_flow_cost"] = CheckNetworkFlowCost;
1244 m["nvalue"] = CheckNvalue;
1245 m["ortools_regular"] = CheckRegular;
1246 m["regular_nfa"] = CheckRegularNfa;
1247 m["set_in"] = CheckSetIn;
1248 m["int_in"] = CheckSetIn;
1249 m["set_not_in"] = CheckSetNotIn;
1250 m["int_not_in"] = CheckSetNotIn;
1251 m["set_in_reif"] = CheckSetInReif;
1252 m["sliding_sum"] = CheckSlidingSum;
1253 m["sort"] = CheckSort;
1254 m["fzn_subcircuit"] = CheckSubCircuit;
1255 m["symmetric_all_different"] = CheckSymmetricAllDifferent;
1256 m["ortools_table_bool"] = CheckTableInt;
1257 m["ortools_table_int"] = CheckTableInt;
1258 return m;
1259}
1260
1261} // namespace
1262
1264 const std::function<int64(IntegerVariable*)>& evaluator) {
1265 bool ok = true;
1266 const CallMap call_map = CreateCallMap();
1267 for (Constraint* ct : model.constraints()) {
1268 if (!ct->active) continue;
1269 const auto& checker = gtl::FindOrDie(call_map, ct->type);
1270 if (!checker(*ct, evaluator)) {
1271 FZLOG << "Failing constraint " << ct->DebugString() << FZENDL;
1272 ok = false;
1273 }
1274 }
1275 return ok;
1276}
1277
1278} // namespace fz
1279} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define LOG(severity)
Definition: base/logging.h:420
Block * next
const Constraint * ct
int64 value
#define FZLOG
#define FZENDL
GRBmodel * model
static const int64 kint64max
int64_t int64
static const int64 kint64min
const int FATAL
Definition: log_severity.h:32
const Collection::value_type::second_type & FindOrDie(const Collection &collection, const typename Collection::value_type::first_type &key)
Definition: map_util.h:176
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
bool CheckSolution(const Model &model, const std::function< int64(IntegerVariable *)> &evaluator)
Definition: checker.cc:1263
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int index
Definition: pack.cc:508
int64 tail
int64 cost
int64 head
int64 capacity
int64 ValueAt(int pos) const
Definition: model.cc:549
IntegerVariable * Var() const
Definition: model.cc:574
std::vector< IntegerVariable * > variables
IntegerVariable * VarAt(int pos) const
Definition: model.cc:578
std::string DebugString() const
Definition: model.cc:447
std::string DebugString() const
Definition: model.cc:614
std::vector< Argument > arguments