OR-Tools  8.2
expr_cst.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 
14 //
15 // Expression constraints
16 
17 #include <cstddef>
18 #include <set>
19 #include <string>
20 #include <vector>
21 
22 #include "absl/strings/str_format.h"
23 #include "absl/strings/str_join.h"
26 #include "ortools/base/logging.h"
27 #include "ortools/base/stl_util.h"
32 
33 ABSL_FLAG(int, cache_initial_size, 1024,
34  "Initial size of the array of the hash "
35  "table of caches for objects of type Var(x == 3)");
36 
37 namespace operations_research {
38 
39 //-----------------------------------------------------------------------------
40 // Equality
41 
42 namespace {
43 class EqualityExprCst : public Constraint {
44  public:
45  EqualityExprCst(Solver* const s, IntExpr* const e, int64 v);
46  ~EqualityExprCst() override {}
47  void Post() override;
48  void InitialPropagate() override;
49  IntVar* Var() override {
50  return solver()->MakeIsEqualCstVar(expr_->Var(), value_);
51  }
52  std::string DebugString() const override;
53 
54  void Accept(ModelVisitor* const visitor) const override {
55  visitor->BeginVisitConstraint(ModelVisitor::kEquality, this);
56  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
57  expr_);
58  visitor->VisitIntegerArgument(ModelVisitor::kValueArgument, value_);
59  visitor->EndVisitConstraint(ModelVisitor::kEquality, this);
60  }
61 
62  private:
63  IntExpr* const expr_;
64  int64 value_;
65 };
66 
67 EqualityExprCst::EqualityExprCst(Solver* const s, IntExpr* const e, int64 v)
68  : Constraint(s), expr_(e), value_(v) {}
69 
70 void EqualityExprCst::Post() {
71  if (!expr_->IsVar()) {
72  Demon* d = solver()->MakeConstraintInitialPropagateCallback(this);
73  expr_->WhenRange(d);
74  }
75 }
76 
77 void EqualityExprCst::InitialPropagate() { expr_->SetValue(value_); }
78 
79 std::string EqualityExprCst::DebugString() const {
80  return absl::StrFormat("(%s == %d)", expr_->DebugString(), value_);
81 }
82 } // namespace
83 
84 Constraint* Solver::MakeEquality(IntExpr* const e, int64 v) {
85  CHECK_EQ(this, e->solver());
86  IntExpr* left = nullptr;
87  IntExpr* right = nullptr;
88  if (IsADifference(e, &left, &right)) {
89  return MakeEquality(left, MakeSum(right, v));
90  } else if (e->IsVar() && !e->Var()->Contains(v)) {
91  return MakeFalseConstraint();
92  } else if (e->Min() == e->Max() && e->Min() == v) {
93  return MakeTrueConstraint();
94  } else {
95  return RevAlloc(new EqualityExprCst(this, e, v));
96  }
97 }
98 
99 Constraint* Solver::MakeEquality(IntExpr* const e, int v) {
100  CHECK_EQ(this, e->solver());
101  IntExpr* left = nullptr;
102  IntExpr* right = nullptr;
103  if (IsADifference(e, &left, &right)) {
104  return MakeEquality(left, MakeSum(right, v));
105  } else if (e->IsVar() && !e->Var()->Contains(v)) {
106  return MakeFalseConstraint();
107  } else if (e->Min() == e->Max() && e->Min() == v) {
108  return MakeTrueConstraint();
109  } else {
110  return RevAlloc(new EqualityExprCst(this, e, v));
111  }
112 }
113 
114 //-----------------------------------------------------------------------------
115 // Greater or equal constraint
116 
117 namespace {
118 class GreaterEqExprCst : public Constraint {
119  public:
120  GreaterEqExprCst(Solver* const s, IntExpr* const e, int64 v);
121  ~GreaterEqExprCst() override {}
122  void Post() override;
123  void InitialPropagate() override;
124  std::string DebugString() const override;
125  IntVar* Var() override {
126  return solver()->MakeIsGreaterOrEqualCstVar(expr_->Var(), value_);
127  }
128 
129  void Accept(ModelVisitor* const visitor) const override {
130  visitor->BeginVisitConstraint(ModelVisitor::kGreaterOrEqual, this);
131  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
132  expr_);
133  visitor->VisitIntegerArgument(ModelVisitor::kValueArgument, value_);
134  visitor->EndVisitConstraint(ModelVisitor::kGreaterOrEqual, this);
135  }
136 
137  private:
138  IntExpr* const expr_;
139  int64 value_;
140  Demon* demon_;
141 };
142 
143 GreaterEqExprCst::GreaterEqExprCst(Solver* const s, IntExpr* const e, int64 v)
144  : Constraint(s), expr_(e), value_(v), demon_(nullptr) {}
145 
146 void GreaterEqExprCst::Post() {
147  if (!expr_->IsVar() && expr_->Min() < value_) {
148  demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
149  expr_->WhenRange(demon_);
150  } else {
151  // Let's clean the demon in case the constraint is posted during search.
152  demon_ = nullptr;
153  }
154 }
155 
156 void GreaterEqExprCst::InitialPropagate() {
157  expr_->SetMin(value_);
158  if (demon_ != nullptr && expr_->Min() >= value_) {
159  demon_->inhibit(solver());
160  }
161 }
162 
163 std::string GreaterEqExprCst::DebugString() const {
164  return absl::StrFormat("(%s >= %d)", expr_->DebugString(), value_);
165 }
166 } // namespace
167 
169  CHECK_EQ(this, e->solver());
170  if (e->Min() >= v) {
171  return MakeTrueConstraint();
172  } else if (e->Max() < v) {
173  return MakeFalseConstraint();
174  } else {
175  return RevAlloc(new GreaterEqExprCst(this, e, v));
176  }
177 }
178 
180  CHECK_EQ(this, e->solver());
181  if (e->Min() >= v) {
182  return MakeTrueConstraint();
183  } else if (e->Max() < v) {
184  return MakeFalseConstraint();
185  } else {
186  return RevAlloc(new GreaterEqExprCst(this, e, v));
187  }
188 }
189 
191  CHECK_EQ(this, e->solver());
192  if (e->Min() > v) {
193  return MakeTrueConstraint();
194  } else if (e->Max() <= v) {
195  return MakeFalseConstraint();
196  } else {
197  return RevAlloc(new GreaterEqExprCst(this, e, v + 1));
198  }
199 }
200 
202  CHECK_EQ(this, e->solver());
203  if (e->Min() > v) {
204  return MakeTrueConstraint();
205  } else if (e->Max() <= v) {
206  return MakeFalseConstraint();
207  } else {
208  return RevAlloc(new GreaterEqExprCst(this, e, v + 1));
209  }
210 }
211 
212 //-----------------------------------------------------------------------------
213 // Less or equal constraint
214 
215 namespace {
216 class LessEqExprCst : public Constraint {
217  public:
218  LessEqExprCst(Solver* const s, IntExpr* const e, int64 v);
219  ~LessEqExprCst() override {}
220  void Post() override;
221  void InitialPropagate() override;
222  std::string DebugString() const override;
223  IntVar* Var() override {
224  return solver()->MakeIsLessOrEqualCstVar(expr_->Var(), value_);
225  }
226  void Accept(ModelVisitor* const visitor) const override {
227  visitor->BeginVisitConstraint(ModelVisitor::kLessOrEqual, this);
228  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
229  expr_);
230  visitor->VisitIntegerArgument(ModelVisitor::kValueArgument, value_);
231  visitor->EndVisitConstraint(ModelVisitor::kLessOrEqual, this);
232  }
233 
234  private:
235  IntExpr* const expr_;
236  int64 value_;
237  Demon* demon_;
238 };
239 
240 LessEqExprCst::LessEqExprCst(Solver* const s, IntExpr* const e, int64 v)
241  : Constraint(s), expr_(e), value_(v), demon_(nullptr) {}
242 
243 void LessEqExprCst::Post() {
244  if (!expr_->IsVar() && expr_->Max() > value_) {
245  demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
246  expr_->WhenRange(demon_);
247  } else {
248  // Let's clean the demon in case the constraint is posted during search.
249  demon_ = nullptr;
250  }
251 }
252 
253 void LessEqExprCst::InitialPropagate() {
254  expr_->SetMax(value_);
255  if (demon_ != nullptr && expr_->Max() <= value_) {
256  demon_->inhibit(solver());
257  }
258 }
259 
260 std::string LessEqExprCst::DebugString() const {
261  return absl::StrFormat("(%s <= %d)", expr_->DebugString(), value_);
262 }
263 } // namespace
264 
266  CHECK_EQ(this, e->solver());
267  if (e->Max() <= v) {
268  return MakeTrueConstraint();
269  } else if (e->Min() > v) {
270  return MakeFalseConstraint();
271  } else {
272  return RevAlloc(new LessEqExprCst(this, e, v));
273  }
274 }
275 
277  CHECK_EQ(this, e->solver());
278  if (e->Max() <= v) {
279  return MakeTrueConstraint();
280  } else if (e->Min() > v) {
281  return MakeFalseConstraint();
282  } else {
283  return RevAlloc(new LessEqExprCst(this, e, v));
284  }
285 }
286 
288  CHECK_EQ(this, e->solver());
289  if (e->Max() < v) {
290  return MakeTrueConstraint();
291  } else if (e->Min() >= v) {
292  return MakeFalseConstraint();
293  } else {
294  return RevAlloc(new LessEqExprCst(this, e, v - 1));
295  }
296 }
297 
299  CHECK_EQ(this, e->solver());
300  if (e->Max() < v) {
301  return MakeTrueConstraint();
302  } else if (e->Min() >= v) {
303  return MakeFalseConstraint();
304  } else {
305  return RevAlloc(new LessEqExprCst(this, e, v - 1));
306  }
307 }
308 
309 //-----------------------------------------------------------------------------
310 // Different constraints
311 
312 namespace {
313 class DiffCst : public Constraint {
314  public:
315  DiffCst(Solver* const s, IntVar* const var, int64 value);
316  ~DiffCst() override {}
317  void Post() override {}
318  void InitialPropagate() override;
319  void BoundPropagate();
320  std::string DebugString() const override;
321  IntVar* Var() override {
322  return solver()->MakeIsDifferentCstVar(var_, value_);
323  }
324  void Accept(ModelVisitor* const visitor) const override {
325  visitor->BeginVisitConstraint(ModelVisitor::kNonEqual, this);
326  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
327  var_);
328  visitor->VisitIntegerArgument(ModelVisitor::kValueArgument, value_);
329  visitor->EndVisitConstraint(ModelVisitor::kNonEqual, this);
330  }
331 
332  private:
333  bool HasLargeDomain(IntVar* var);
334 
335  IntVar* const var_;
336  int64 value_;
337  Demon* demon_;
338 };
339 
340 DiffCst::DiffCst(Solver* const s, IntVar* const var, int64 value)
341  : Constraint(s), var_(var), value_(value), demon_(nullptr) {}
342 
343 void DiffCst::InitialPropagate() {
344  if (HasLargeDomain(var_)) {
345  demon_ = MakeConstraintDemon0(solver(), this, &DiffCst::BoundPropagate,
346  "BoundPropagate");
347  var_->WhenRange(demon_);
348  } else {
349  var_->RemoveValue(value_);
350  }
351 }
352 
353 void DiffCst::BoundPropagate() {
354  const int64 var_min = var_->Min();
355  const int64 var_max = var_->Max();
356  if (var_min > value_ || var_max < value_) {
357  demon_->inhibit(solver());
358  } else if (var_min == value_) {
359  var_->SetMin(value_ + 1);
360  } else if (var_max == value_) {
361  var_->SetMax(value_ - 1);
362  } else if (!HasLargeDomain(var_)) {
363  demon_->inhibit(solver());
364  var_->RemoveValue(value_);
365  }
366 }
367 
368 std::string DiffCst::DebugString() const {
369  return absl::StrFormat("(%s != %d)", var_->DebugString(), value_);
370 }
371 
372 bool DiffCst::HasLargeDomain(IntVar* var) {
373  return CapSub(var->Max(), var->Min()) > 0xFFFFFF;
374 }
375 } // namespace
376 
378  CHECK_EQ(this, e->solver());
379  IntExpr* left = nullptr;
380  IntExpr* right = nullptr;
381  if (IsADifference(e, &left, &right)) {
382  return MakeNonEquality(left, MakeSum(right, v));
383  } else if (e->IsVar() && !e->Var()->Contains(v)) {
384  return MakeTrueConstraint();
385  } else if (e->Bound() && e->Min() == v) {
386  return MakeFalseConstraint();
387  } else {
388  return RevAlloc(new DiffCst(this, e->Var(), v));
389  }
390 }
391 
393  CHECK_EQ(this, e->solver());
394  IntExpr* left = nullptr;
395  IntExpr* right = nullptr;
396  if (IsADifference(e, &left, &right)) {
397  return MakeNonEquality(left, MakeSum(right, v));
398  } else if (e->IsVar() && !e->Var()->Contains(v)) {
399  return MakeTrueConstraint();
400  } else if (e->Bound() && e->Min() == v) {
401  return MakeFalseConstraint();
402  } else {
403  return RevAlloc(new DiffCst(this, e->Var(), v));
404  }
405 }
406 // ----- is_equal_cst Constraint -----
407 
408 namespace {
409 class IsEqualCstCt : public CastConstraint {
410  public:
411  IsEqualCstCt(Solver* const s, IntVar* const v, int64 c, IntVar* const b)
412  : CastConstraint(s, b), var_(v), cst_(c), demon_(nullptr) {}
413  void Post() override {
414  demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
415  var_->WhenDomain(demon_);
416  target_var_->WhenBound(demon_);
417  }
418  void InitialPropagate() override {
419  bool inhibit = var_->Bound();
420  int64 u = var_->Contains(cst_);
421  int64 l = inhibit ? u : 0;
422  target_var_->SetRange(l, u);
423  if (target_var_->Bound()) {
424  if (target_var_->Min() == 0) {
425  if (var_->Size() <= 0xFFFFFF) {
426  var_->RemoveValue(cst_);
427  inhibit = true;
428  }
429  } else {
430  var_->SetValue(cst_);
431  inhibit = true;
432  }
433  }
434  if (inhibit) {
435  demon_->inhibit(solver());
436  }
437  }
438  std::string DebugString() const override {
439  return absl::StrFormat("IsEqualCstCt(%s, %d, %s)", var_->DebugString(),
440  cst_, target_var_->DebugString());
441  }
442 
443  void Accept(ModelVisitor* const visitor) const override {
444  visitor->BeginVisitConstraint(ModelVisitor::kIsEqual, this);
445  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
446  var_);
447  visitor->VisitIntegerArgument(ModelVisitor::kValueArgument, cst_);
448  visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,
449  target_var_);
450  visitor->EndVisitConstraint(ModelVisitor::kIsEqual, this);
451  }
452 
453  private:
454  IntVar* const var_;
455  int64 cst_;
456  Demon* demon_;
457 };
458 } // namespace
459 
461  IntExpr* left = nullptr;
462  IntExpr* right = nullptr;
463  if (IsADifference(var, &left, &right)) {
464  return MakeIsEqualVar(left, MakeSum(right, value));
465  }
466  if (CapSub(var->Max(), var->Min()) == 1) {
467  if (value == var->Min()) {
468  return MakeDifference(value + 1, var)->Var();
469  } else if (value == var->Max()) {
470  return MakeSum(var, -value + 1)->Var();
471  } else {
472  return MakeIntConst(0);
473  }
474  }
475  if (var->IsVar()) {
476  return var->Var()->IsEqual(value);
477  } else {
478  IntVar* const boolvar =
479  MakeBoolVar(absl::StrFormat("Is(%s == %d)", var->DebugString(), value));
481  return boolvar;
482  }
483 }
484 
486  IntVar* const boolvar) {
487  CHECK_EQ(this, var->solver());
488  CHECK_EQ(this, boolvar->solver());
489  if (value == var->Min()) {
490  if (CapSub(var->Max(), var->Min()) == 1) {
491  return MakeEquality(MakeDifference(value + 1, var), boolvar);
492  }
493  return MakeIsLessOrEqualCstCt(var, value, boolvar);
494  }
495  if (value == var->Max()) {
496  if (CapSub(var->Max(), var->Min()) == 1) {
497  return MakeEquality(MakeSum(var, -value + 1), boolvar);
498  }
499  return MakeIsGreaterOrEqualCstCt(var, value, boolvar);
500  }
501  if (boolvar->Bound()) {
502  if (boolvar->Min() == 0) {
503  return MakeNonEquality(var, value);
504  } else {
505  return MakeEquality(var, value);
506  }
507  }
508  // TODO(user) : what happens if the constraint is not posted?
509  // The cache becomes tainted.
510  model_cache_->InsertExprConstantExpression(
512  IntExpr* left = nullptr;
513  IntExpr* right = nullptr;
514  if (IsADifference(var, &left, &right)) {
515  return MakeIsEqualCt(left, MakeSum(right, value), boolvar);
516  } else {
517  return RevAlloc(new IsEqualCstCt(this, var->Var(), value, boolvar));
518  }
519 }
520 
521 // ----- is_diff_cst Constraint -----
522 
523 namespace {
524 class IsDiffCstCt : public CastConstraint {
525  public:
526  IsDiffCstCt(Solver* const s, IntVar* const v, int64 c, IntVar* const b)
527  : CastConstraint(s, b), var_(v), cst_(c), demon_(nullptr) {}
528 
529  void Post() override {
530  demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
531  var_->WhenDomain(demon_);
532  target_var_->WhenBound(demon_);
533  }
534 
535  void InitialPropagate() override {
536  bool inhibit = var_->Bound();
537  int64 l = 1 - var_->Contains(cst_);
538  int64 u = inhibit ? l : 1;
539  target_var_->SetRange(l, u);
540  if (target_var_->Bound()) {
541  if (target_var_->Min() == 1) {
542  if (var_->Size() <= 0xFFFFFF) {
543  var_->RemoveValue(cst_);
544  inhibit = true;
545  }
546  } else {
547  var_->SetValue(cst_);
548  inhibit = true;
549  }
550  }
551  if (inhibit) {
552  demon_->inhibit(solver());
553  }
554  }
555 
556  std::string DebugString() const override {
557  return absl::StrFormat("IsDiffCstCt(%s, %d, %s)", var_->DebugString(), cst_,
558  target_var_->DebugString());
559  }
560 
561  void Accept(ModelVisitor* const visitor) const override {
562  visitor->BeginVisitConstraint(ModelVisitor::kIsDifferent, this);
563  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
564  var_);
565  visitor->VisitIntegerArgument(ModelVisitor::kValueArgument, cst_);
566  visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,
567  target_var_);
568  visitor->EndVisitConstraint(ModelVisitor::kIsDifferent, this);
569  }
570 
571  private:
572  IntVar* const var_;
573  int64 cst_;
574  Demon* demon_;
575 };
576 } // namespace
577 
579  IntExpr* left = nullptr;
580  IntExpr* right = nullptr;
581  if (IsADifference(var, &left, &right)) {
582  return MakeIsDifferentVar(left, MakeSum(right, value));
583  }
584  return var->Var()->IsDifferent(value);
585 }
586 
588  IntVar* const boolvar) {
589  CHECK_EQ(this, var->solver());
590  CHECK_EQ(this, boolvar->solver());
591  if (value == var->Min()) {
592  return MakeIsGreaterOrEqualCstCt(var, value + 1, boolvar);
593  }
594  if (value == var->Max()) {
595  return MakeIsLessOrEqualCstCt(var, value - 1, boolvar);
596  }
597  if (var->IsVar() && !var->Var()->Contains(value)) {
598  return MakeEquality(boolvar, int64{1});
599  }
600  if (var->Bound() && var->Min() == value) {
601  return MakeEquality(boolvar, Zero());
602  }
603  if (boolvar->Bound()) {
604  if (boolvar->Min() == 0) {
605  return MakeEquality(var, value);
606  } else {
607  return MakeNonEquality(var, value);
608  }
609  }
610  model_cache_->InsertExprConstantExpression(
612  IntExpr* left = nullptr;
613  IntExpr* right = nullptr;
614  if (IsADifference(var, &left, &right)) {
615  return MakeIsDifferentCt(left, MakeSum(right, value), boolvar);
616  } else {
617  return RevAlloc(new IsDiffCstCt(this, var->Var(), value, boolvar));
618  }
619 }
620 
621 // ----- is_greater_equal_cst Constraint -----
622 
623 namespace {
624 class IsGreaterEqualCstCt : public CastConstraint {
625  public:
626  IsGreaterEqualCstCt(Solver* const s, IntExpr* const v, int64 c,
627  IntVar* const b)
628  : CastConstraint(s, b), expr_(v), cst_(c), demon_(nullptr) {}
629  void Post() override {
630  demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
631  expr_->WhenRange(demon_);
632  target_var_->WhenBound(demon_);
633  }
634  void InitialPropagate() override {
635  bool inhibit = false;
636  int64 u = expr_->Max() >= cst_;
637  int64 l = expr_->Min() >= cst_;
638  target_var_->SetRange(l, u);
639  if (target_var_->Bound()) {
640  inhibit = true;
641  if (target_var_->Min() == 0) {
642  expr_->SetMax(cst_ - 1);
643  } else {
644  expr_->SetMin(cst_);
645  }
646  }
647  if (inhibit && ((target_var_->Max() == 0 && expr_->Max() < cst_) ||
648  (target_var_->Min() == 1 && expr_->Min() >= cst_))) {
649  // Can we safely inhibit? Sometimes an expression is not
650  // persistent, just monotonic.
651  demon_->inhibit(solver());
652  }
653  }
654  std::string DebugString() const override {
655  return absl::StrFormat("IsGreaterEqualCstCt(%s, %d, %s)",
656  expr_->DebugString(), cst_,
657  target_var_->DebugString());
658  }
659 
660  void Accept(ModelVisitor* const visitor) const override {
661  visitor->BeginVisitConstraint(ModelVisitor::kIsGreaterOrEqual, this);
662  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
663  expr_);
664  visitor->VisitIntegerArgument(ModelVisitor::kValueArgument, cst_);
665  visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,
666  target_var_);
667  visitor->EndVisitConstraint(ModelVisitor::kIsGreaterOrEqual, this);
668  }
669 
670  private:
671  IntExpr* const expr_;
672  int64 cst_;
673  Demon* demon_;
674 };
675 } // namespace
676 
678  if (var->Min() >= value) {
679  return MakeIntConst(int64{1});
680  }
681  if (var->Max() < value) {
682  return MakeIntConst(int64{0});
683  }
684  if (var->IsVar()) {
685  return var->Var()->IsGreaterOrEqual(value);
686  } else {
687  IntVar* const boolvar =
688  MakeBoolVar(absl::StrFormat("Is(%s >= %d)", var->DebugString(), value));
690  return boolvar;
691  }
692 }
693 
695  return MakeIsGreaterOrEqualCstVar(var, value + 1);
696 }
697 
699  IntVar* const boolvar) {
700  if (boolvar->Bound()) {
701  if (boolvar->Min() == 0) {
702  return MakeLess(var, value);
703  } else {
704  return MakeGreaterOrEqual(var, value);
705  }
706  }
707  CHECK_EQ(this, var->solver());
708  CHECK_EQ(this, boolvar->solver());
709  model_cache_->InsertExprConstantExpression(
711  return RevAlloc(new IsGreaterEqualCstCt(this, var, value, boolvar));
712 }
713 
715  IntVar* const b) {
716  return MakeIsGreaterOrEqualCstCt(v, c + 1, b);
717 }
718 
719 // ----- is_lesser_equal_cst Constraint -----
720 
721 namespace {
722 class IsLessEqualCstCt : public CastConstraint {
723  public:
724  IsLessEqualCstCt(Solver* const s, IntExpr* const v, int64 c, IntVar* const b)
725  : CastConstraint(s, b), expr_(v), cst_(c), demon_(nullptr) {}
726 
727  void Post() override {
728  demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
729  expr_->WhenRange(demon_);
730  target_var_->WhenBound(demon_);
731  }
732 
733  void InitialPropagate() override {
734  bool inhibit = false;
735  int64 u = expr_->Min() <= cst_;
736  int64 l = expr_->Max() <= cst_;
737  target_var_->SetRange(l, u);
738  if (target_var_->Bound()) {
739  inhibit = true;
740  if (target_var_->Min() == 0) {
741  expr_->SetMin(cst_ + 1);
742  } else {
743  expr_->SetMax(cst_);
744  }
745  }
746  if (inhibit && ((target_var_->Max() == 0 && expr_->Min() > cst_) ||
747  (target_var_->Min() == 1 && expr_->Max() <= cst_))) {
748  // Can we safely inhibit? Sometimes an expression is not
749  // persistent, just monotonic.
750  demon_->inhibit(solver());
751  }
752  }
753 
754  std::string DebugString() const override {
755  return absl::StrFormat("IsLessEqualCstCt(%s, %d, %s)", expr_->DebugString(),
756  cst_, target_var_->DebugString());
757  }
758 
759  void Accept(ModelVisitor* const visitor) const override {
760  visitor->BeginVisitConstraint(ModelVisitor::kIsLessOrEqual, this);
761  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
762  expr_);
763  visitor->VisitIntegerArgument(ModelVisitor::kValueArgument, cst_);
764  visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,
765  target_var_);
766  visitor->EndVisitConstraint(ModelVisitor::kIsLessOrEqual, this);
767  }
768 
769  private:
770  IntExpr* const expr_;
771  int64 cst_;
772  Demon* demon_;
773 };
774 } // namespace
775 
777  if (var->Max() <= value) {
778  return MakeIntConst(int64{1});
779  }
780  if (var->Min() > value) {
781  return MakeIntConst(int64{0});
782  }
783  if (var->IsVar()) {
784  return var->Var()->IsLessOrEqual(value);
785  } else {
786  IntVar* const boolvar =
787  MakeBoolVar(absl::StrFormat("Is(%s <= %d)", var->DebugString(), value));
789  return boolvar;
790  }
791 }
792 
794  return MakeIsLessOrEqualCstVar(var, value - 1);
795 }
796 
798  IntVar* const boolvar) {
799  if (boolvar->Bound()) {
800  if (boolvar->Min() == 0) {
801  return MakeGreater(var, value);
802  } else {
803  return MakeLessOrEqual(var, value);
804  }
805  }
806  CHECK_EQ(this, var->solver());
807  CHECK_EQ(this, boolvar->solver());
808  model_cache_->InsertExprConstantExpression(
810  return RevAlloc(new IsLessEqualCstCt(this, var, value, boolvar));
811 }
812 
814  IntVar* const b) {
815  return MakeIsLessOrEqualCstCt(v, c - 1, b);
816 }
817 
818 // ----- BetweenCt -----
819 
820 namespace {
821 class BetweenCt : public Constraint {
822  public:
823  BetweenCt(Solver* const s, IntExpr* const v, int64 l, int64 u)
824  : Constraint(s), expr_(v), min_(l), max_(u), demon_(nullptr) {}
825 
826  void Post() override {
827  if (!expr_->IsVar()) {
828  demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
829  expr_->WhenRange(demon_);
830  }
831  }
832 
833  void InitialPropagate() override {
834  expr_->SetRange(min_, max_);
835  int64 emin = 0;
836  int64 emax = 0;
837  expr_->Range(&emin, &emax);
838  if (demon_ != nullptr && emin >= min_ && emax <= max_) {
839  demon_->inhibit(solver());
840  }
841  }
842 
843  std::string DebugString() const override {
844  return absl::StrFormat("BetweenCt(%s, %d, %d)", expr_->DebugString(), min_,
845  max_);
846  }
847 
848  void Accept(ModelVisitor* const visitor) const override {
849  visitor->BeginVisitConstraint(ModelVisitor::kBetween, this);
850  visitor->VisitIntegerArgument(ModelVisitor::kMinArgument, min_);
851  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
852  expr_);
853  visitor->VisitIntegerArgument(ModelVisitor::kMaxArgument, max_);
854  visitor->EndVisitConstraint(ModelVisitor::kBetween, this);
855  }
856 
857  private:
858  IntExpr* const expr_;
859  int64 min_;
860  int64 max_;
861  Demon* demon_;
862 };
863 
864 // ----- NonMember constraint -----
865 
866 class NotBetweenCt : public Constraint {
867  public:
868  NotBetweenCt(Solver* const s, IntExpr* const v, int64 l, int64 u)
869  : Constraint(s), expr_(v), min_(l), max_(u), demon_(nullptr) {}
870 
871  void Post() override {
872  demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
873  expr_->WhenRange(demon_);
874  }
875 
876  void InitialPropagate() override {
877  int64 emin = 0;
878  int64 emax = 0;
879  expr_->Range(&emin, &emax);
880  if (emin >= min_) {
881  expr_->SetMin(max_ + 1);
882  } else if (emax <= max_) {
883  expr_->SetMax(min_ - 1);
884  }
885 
886  if (!expr_->IsVar() && (emax < min_ || emin > max_)) {
887  demon_->inhibit(solver());
888  }
889  }
890 
891  std::string DebugString() const override {
892  return absl::StrFormat("NotBetweenCt(%s, %d, %d)", expr_->DebugString(),
893  min_, max_);
894  }
895 
896  void Accept(ModelVisitor* const visitor) const override {
897  visitor->BeginVisitConstraint(ModelVisitor::kNotBetween, this);
898  visitor->VisitIntegerArgument(ModelVisitor::kMinArgument, min_);
899  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
900  expr_);
901  visitor->VisitIntegerArgument(ModelVisitor::kMaxArgument, max_);
902  visitor->EndVisitConstraint(ModelVisitor::kBetween, this);
903  }
904 
905  private:
906  IntExpr* const expr_;
907  int64 min_;
908  int64 max_;
909  Demon* demon_;
910 };
911 
912 int64 ExtractExprProductCoeff(IntExpr** expr) {
913  int64 prod = 1;
914  int64 coeff = 1;
915  while ((*expr)->solver()->IsProduct(*expr, expr, &coeff)) prod *= coeff;
916  return prod;
917 }
918 } // namespace
919 
921  DCHECK_EQ(this, expr->solver());
922  // Catch empty and singleton intervals.
923  if (l >= u) {
924  if (l > u) return MakeFalseConstraint();
925  return MakeEquality(expr, l);
926  }
927  int64 emin = 0;
928  int64 emax = 0;
929  expr->Range(&emin, &emax);
930  // Catch the trivial cases first.
931  if (emax < l || emin > u) return MakeFalseConstraint();
932  if (emin >= l && emax <= u) return MakeTrueConstraint();
933  // Catch one-sided constraints.
934  if (emax <= u) return MakeGreaterOrEqual(expr, l);
935  if (emin >= l) return MakeLessOrEqual(expr, u);
936  // Simplify the common factor, if any.
937  int64 coeff = ExtractExprProductCoeff(&expr);
938  if (coeff != 1) {
939  CHECK_NE(coeff, 0); // Would have been caught by the trivial cases already.
940  if (coeff < 0) {
941  std::swap(u, l);
942  u = -u;
943  l = -l;
944  coeff = -coeff;
945  }
946  return MakeBetweenCt(expr, PosIntDivUp(l, coeff), PosIntDivDown(u, coeff));
947  } else {
948  // No further reduction is possible.
949  return RevAlloc(new BetweenCt(this, expr, l, u));
950  }
951 }
952 
954  DCHECK_EQ(this, expr->solver());
955  // Catch empty interval.
956  if (l > u) {
957  return MakeTrueConstraint();
958  }
959 
960  int64 emin = 0;
961  int64 emax = 0;
962  expr->Range(&emin, &emax);
963  // Catch the trivial cases first.
964  if (emax < l || emin > u) return MakeTrueConstraint();
965  if (emin >= l && emax <= u) return MakeFalseConstraint();
966  // Catch one-sided constraints.
967  if (emin >= l) return MakeGreater(expr, u);
968  if (emax <= u) return MakeLess(expr, l);
969  // TODO(user): Add back simplification code if expr is constant *
970  // other_expr.
971  return RevAlloc(new NotBetweenCt(this, expr, l, u));
972 }
973 
974 // ----- is_between_cst Constraint -----
975 
976 namespace {
977 class IsBetweenCt : public Constraint {
978  public:
979  IsBetweenCt(Solver* const s, IntExpr* const e, int64 l, int64 u,
980  IntVar* const b)
981  : Constraint(s),
982  expr_(e),
983  min_(l),
984  max_(u),
985  boolvar_(b),
986  demon_(nullptr) {}
987 
988  void Post() override {
989  demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
990  expr_->WhenRange(demon_);
991  boolvar_->WhenBound(demon_);
992  }
993 
994  void InitialPropagate() override {
995  bool inhibit = false;
996  int64 emin = 0;
997  int64 emax = 0;
998  expr_->Range(&emin, &emax);
999  int64 u = 1 - (emin > max_ || emax < min_);
1000  int64 l = emax <= max_ && emin >= min_;
1001  boolvar_->SetRange(l, u);
1002  if (boolvar_->Bound()) {
1003  inhibit = true;
1004  if (boolvar_->Min() == 0) {
1005  if (expr_->IsVar()) {
1006  expr_->Var()->RemoveInterval(min_, max_);
1007  inhibit = true;
1008  } else if (emin > min_) {
1009  expr_->SetMin(max_ + 1);
1010  } else if (emax < max_) {
1011  expr_->SetMax(min_ - 1);
1012  }
1013  } else {
1014  expr_->SetRange(min_, max_);
1015  inhibit = true;
1016  }
1017  if (inhibit && expr_->IsVar()) {
1018  demon_->inhibit(solver());
1019  }
1020  }
1021  }
1022 
1023  std::string DebugString() const override {
1024  return absl::StrFormat("IsBetweenCt(%s, %d, %d, %s)", expr_->DebugString(),
1025  min_, max_, boolvar_->DebugString());
1026  }
1027 
1028  void Accept(ModelVisitor* const visitor) const override {
1029  visitor->BeginVisitConstraint(ModelVisitor::kIsBetween, this);
1030  visitor->VisitIntegerArgument(ModelVisitor::kMinArgument, min_);
1031  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
1032  expr_);
1033  visitor->VisitIntegerArgument(ModelVisitor::kMaxArgument, max_);
1034  visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,
1035  boolvar_);
1036  visitor->EndVisitConstraint(ModelVisitor::kIsBetween, this);
1037  }
1038 
1039  private:
1040  IntExpr* const expr_;
1041  int64 min_;
1042  int64 max_;
1043  IntVar* const boolvar_;
1044  Demon* demon_;
1045 };
1046 } // namespace
1047 
1049  IntVar* const b) {
1050  CHECK_EQ(this, expr->solver());
1051  CHECK_EQ(this, b->solver());
1052  // Catch empty and singleton intervals.
1053  if (l >= u) {
1054  if (l > u) return MakeEquality(b, Zero());
1055  return MakeIsEqualCstCt(expr, l, b);
1056  }
1057  int64 emin = 0;
1058  int64 emax = 0;
1059  expr->Range(&emin, &emax);
1060  // Catch the trivial cases first.
1061  if (emax < l || emin > u) return MakeEquality(b, Zero());
1062  if (emin >= l && emax <= u) return MakeEquality(b, 1);
1063  // Catch one-sided constraints.
1064  if (emax <= u) return MakeIsGreaterOrEqualCstCt(expr, l, b);
1065  if (emin >= l) return MakeIsLessOrEqualCstCt(expr, u, b);
1066  // Simplify the common factor, if any.
1067  int64 coeff = ExtractExprProductCoeff(&expr);
1068  if (coeff != 1) {
1069  CHECK_NE(coeff, 0); // Would have been caught by the trivial cases already.
1070  if (coeff < 0) {
1071  std::swap(u, l);
1072  u = -u;
1073  l = -l;
1074  coeff = -coeff;
1075  }
1076  return MakeIsBetweenCt(expr, PosIntDivUp(l, coeff), PosIntDivDown(u, coeff),
1077  b);
1078  } else {
1079  // No further reduction is possible.
1080  return RevAlloc(new IsBetweenCt(this, expr, l, u, b));
1081  }
1082 }
1083 
1085  CHECK_EQ(this, v->solver());
1086  IntVar* const b = MakeBoolVar();
1087  AddConstraint(MakeIsBetweenCt(v, l, u, b));
1088  return b;
1089 }
1090 
1091 // ---------- Member ----------
1092 
1093 // ----- Member(IntVar, IntSet) -----
1094 
1095 namespace {
1096 // TODO(user): Do not create holes on expressions.
1097 class MemberCt : public Constraint {
1098  public:
1099  MemberCt(Solver* const s, IntVar* const v,
1100  const std::vector<int64>& sorted_values)
1101  : Constraint(s), var_(v), values_(sorted_values) {
1102  DCHECK(v != nullptr);
1103  DCHECK(s != nullptr);
1104  }
1105 
1106  void Post() override {}
1107 
1108  void InitialPropagate() override { var_->SetValues(values_); }
1109 
1110  std::string DebugString() const override {
1111  return absl::StrFormat("Member(%s, %s)", var_->DebugString(),
1112  absl::StrJoin(values_, ", "));
1113  }
1114 
1115  void Accept(ModelVisitor* const visitor) const override {
1116  visitor->BeginVisitConstraint(ModelVisitor::kMember, this);
1117  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
1118  var_);
1119  visitor->VisitIntegerArrayArgument(ModelVisitor::kValuesArgument, values_);
1120  visitor->EndVisitConstraint(ModelVisitor::kMember, this);
1121  }
1122 
1123  private:
1124  IntVar* const var_;
1125  const std::vector<int64> values_;
1126 };
1127 
1128 class NotMemberCt : public Constraint {
1129  public:
1130  NotMemberCt(Solver* const s, IntVar* const v,
1131  const std::vector<int64>& sorted_values)
1132  : Constraint(s), var_(v), values_(sorted_values) {
1133  DCHECK(v != nullptr);
1134  DCHECK(s != nullptr);
1135  }
1136 
1137  void Post() override {}
1138 
1139  void InitialPropagate() override { var_->RemoveValues(values_); }
1140 
1141  std::string DebugString() const override {
1142  return absl::StrFormat("NotMember(%s, %s)", var_->DebugString(),
1143  absl::StrJoin(values_, ", "));
1144  }
1145 
1146  void Accept(ModelVisitor* const visitor) const override {
1147  visitor->BeginVisitConstraint(ModelVisitor::kMember, this);
1148  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
1149  var_);
1150  visitor->VisitIntegerArrayArgument(ModelVisitor::kValuesArgument, values_);
1151  visitor->EndVisitConstraint(ModelVisitor::kMember, this);
1152  }
1153 
1154  private:
1155  IntVar* const var_;
1156  const std::vector<int64> values_;
1157 };
1158 } // namespace
1159 
1161  const std::vector<int64>& values) {
1162  const int64 coeff = ExtractExprProductCoeff(&expr);
1163  if (coeff == 0) {
1164  return std::find(values.begin(), values.end(), 0) == values.end()
1166  : MakeTrueConstraint();
1167  }
1168  std::vector<int64> copied_values = values;
1169  // If the expression is a non-trivial product, we filter out the values that
1170  // aren't multiples of "coeff", and divide them.
1171  if (coeff != 1) {
1172  int num_kept = 0;
1173  for (const int64 v : copied_values) {
1174  if (v % coeff == 0) copied_values[num_kept++] = v / coeff;
1175  }
1176  copied_values.resize(num_kept);
1177  }
1178  // Filter out the values that are outside the [Min, Max] interval.
1179  int num_kept = 0;
1180  int64 emin;
1181  int64 emax;
1182  expr->Range(&emin, &emax);
1183  for (const int64 v : copied_values) {
1184  if (v >= emin && v <= emax) copied_values[num_kept++] = v;
1185  }
1186  copied_values.resize(num_kept);
1187  // Catch empty set.
1188  if (copied_values.empty()) return MakeFalseConstraint();
1189  // Sort and remove duplicates.
1190  gtl::STLSortAndRemoveDuplicates(&copied_values);
1191  // Special case for singleton.
1192  if (copied_values.size() == 1) return MakeEquality(expr, copied_values[0]);
1193  // Catch contiguous intervals.
1194  if (copied_values.size() ==
1195  copied_values.back() - copied_values.front() + 1) {
1196  // Note: MakeBetweenCt() has a fast-track for trivially true constraints.
1197  return MakeBetweenCt(expr, copied_values.front(), copied_values.back());
1198  }
1199  // If the set of values in [expr.Min(), expr.Max()] that are *not* in
1200  // "values" is smaller than "values", then it's more efficient to use
1201  // NotMemberCt. Catch that case here.
1202  if (emax - emin < 2 * copied_values.size()) {
1203  // Convert "copied_values" to list the values *not* allowed.
1204  std::vector<bool> is_among_input_values(emax - emin + 1, false);
1205  for (const int64 v : copied_values) is_among_input_values[v - emin] = true;
1206  // We use the zero valued indices of is_among_input_values to build the
1207  // complement of copied_values.
1208  copied_values.clear();
1209  for (int64 v_off = 0; v_off < is_among_input_values.size(); ++v_off) {
1210  if (!is_among_input_values[v_off]) copied_values.push_back(v_off + emin);
1211  }
1212  // The empty' case (all values in range [expr.Min(), expr.Max()] are in the
1213  // "values" input) was caught earlier, by the "contiguous interval" case.
1214  DCHECK_GE(copied_values.size(), 1);
1215  if (copied_values.size() == 1) {
1216  return MakeNonEquality(expr, copied_values[0]);
1217  }
1218  return RevAlloc(new NotMemberCt(this, expr->Var(), copied_values));
1219  }
1220  // Otherwise, just use MemberCt. No further reduction is possible.
1221  return RevAlloc(new MemberCt(this, expr->Var(), copied_values));
1222 }
1223 
1225  const std::vector<int>& values) {
1226  return MakeMemberCt(expr, ToInt64Vector(values));
1227 }
1228 
1230  const std::vector<int64>& values) {
1231  const int64 coeff = ExtractExprProductCoeff(&expr);
1232  if (coeff == 0) {
1233  return std::find(values.begin(), values.end(), 0) == values.end()
1234  ? MakeTrueConstraint()
1235  : MakeFalseConstraint();
1236  }
1237  std::vector<int64> copied_values = values;
1238  // If the expression is a non-trivial product, we filter out the values that
1239  // aren't multiples of "coeff", and divide them.
1240  if (coeff != 1) {
1241  int num_kept = 0;
1242  for (const int64 v : copied_values) {
1243  if (v % coeff == 0) copied_values[num_kept++] = v / coeff;
1244  }
1245  copied_values.resize(num_kept);
1246  }
1247  // Filter out the values that are outside the [Min, Max] interval.
1248  int num_kept = 0;
1249  int64 emin;
1250  int64 emax;
1251  expr->Range(&emin, &emax);
1252  for (const int64 v : copied_values) {
1253  if (v >= emin && v <= emax) copied_values[num_kept++] = v;
1254  }
1255  copied_values.resize(num_kept);
1256  // Catch empty set.
1257  if (copied_values.empty()) return MakeTrueConstraint();
1258  // Sort and remove duplicates.
1259  gtl::STLSortAndRemoveDuplicates(&copied_values);
1260  // Special case for singleton.
1261  if (copied_values.size() == 1) return MakeNonEquality(expr, copied_values[0]);
1262  // Catch contiguous intervals.
1263  if (copied_values.size() ==
1264  copied_values.back() - copied_values.front() + 1) {
1265  return MakeNotBetweenCt(expr, copied_values.front(), copied_values.back());
1266  }
1267  // If the set of values in [expr.Min(), expr.Max()] that are *not* in
1268  // "values" is smaller than "values", then it's more efficient to use
1269  // MemberCt. Catch that case here.
1270  if (emax - emin < 2 * copied_values.size()) {
1271  // Convert "copied_values" to a dense boolean vector.
1272  std::vector<bool> is_among_input_values(emax - emin + 1, false);
1273  for (const int64 v : copied_values) is_among_input_values[v - emin] = true;
1274  // Use zero valued indices for is_among_input_values to build the
1275  // complement of copied_values.
1276  copied_values.clear();
1277  for (int64 v_off = 0; v_off < is_among_input_values.size(); ++v_off) {
1278  if (!is_among_input_values[v_off]) copied_values.push_back(v_off + emin);
1279  }
1280  // The empty' case (all values in range [expr.Min(), expr.Max()] are in the
1281  // "values" input) was caught earlier, by the "contiguous interval" case.
1282  DCHECK_GE(copied_values.size(), 1);
1283  if (copied_values.size() == 1) {
1284  return MakeEquality(expr, copied_values[0]);
1285  }
1286  return RevAlloc(new MemberCt(this, expr->Var(), copied_values));
1287  }
1288  // Otherwise, just use NotMemberCt. No further reduction is possible.
1289  return RevAlloc(new NotMemberCt(this, expr->Var(), copied_values));
1290 }
1291 
1293  const std::vector<int>& values) {
1294  return MakeNotMemberCt(expr, ToInt64Vector(values));
1295 }
1296 
1297 // ----- IsMemberCt -----
1298 
1299 namespace {
1300 class IsMemberCt : public Constraint {
1301  public:
1302  IsMemberCt(Solver* const s, IntVar* const v,
1303  const std::vector<int64>& sorted_values, IntVar* const b)
1304  : Constraint(s),
1305  var_(v),
1306  values_as_set_(sorted_values.begin(), sorted_values.end()),
1307  values_(sorted_values),
1308  boolvar_(b),
1309  support_(0),
1310  demon_(nullptr),
1311  domain_(var_->MakeDomainIterator(true)),
1312  neg_support_(kint64min) {
1313  DCHECK(v != nullptr);
1314  DCHECK(s != nullptr);
1315  DCHECK(b != nullptr);
1316  while (gtl::ContainsKey(values_as_set_, neg_support_)) {
1317  neg_support_++;
1318  }
1319  }
1320 
1321  void Post() override {
1322  demon_ = MakeConstraintDemon0(solver(), this, &IsMemberCt::VarDomain,
1323  "VarDomain");
1324  if (!var_->Bound()) {
1325  var_->WhenDomain(demon_);
1326  }
1327  if (!boolvar_->Bound()) {
1328  Demon* const bdemon = MakeConstraintDemon0(
1329  solver(), this, &IsMemberCt::TargetBound, "TargetBound");
1330  boolvar_->WhenBound(bdemon);
1331  }
1332  }
1333 
1334  void InitialPropagate() override {
1335  boolvar_->SetRange(0, 1);
1336  if (boolvar_->Bound()) {
1337  TargetBound();
1338  } else {
1339  VarDomain();
1340  }
1341  }
1342 
1343  std::string DebugString() const override {
1344  return absl::StrFormat("IsMemberCt(%s, %s, %s)", var_->DebugString(),
1345  absl::StrJoin(values_, ", "),
1346  boolvar_->DebugString());
1347  }
1348 
1349  void Accept(ModelVisitor* const visitor) const override {
1350  visitor->BeginVisitConstraint(ModelVisitor::kIsMember, this);
1351  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
1352  var_);
1353  visitor->VisitIntegerArrayArgument(ModelVisitor::kValuesArgument, values_);
1354  visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,
1355  boolvar_);
1356  visitor->EndVisitConstraint(ModelVisitor::kIsMember, this);
1357  }
1358 
1359  private:
1360  void VarDomain() {
1361  if (boolvar_->Bound()) {
1362  TargetBound();
1363  } else {
1364  for (int offset = 0; offset < values_.size(); ++offset) {
1365  const int candidate = (support_ + offset) % values_.size();
1366  if (var_->Contains(values_[candidate])) {
1367  support_ = candidate;
1368  if (var_->Bound()) {
1369  demon_->inhibit(solver());
1370  boolvar_->SetValue(1);
1371  return;
1372  }
1373  // We have found a positive support. Let's check the
1374  // negative support.
1375  if (var_->Contains(neg_support_)) {
1376  return;
1377  } else {
1378  // Look for a new negative support.
1379  for (const int64 value : InitAndGetValues(domain_)) {
1380  if (!gtl::ContainsKey(values_as_set_, value)) {
1381  neg_support_ = value;
1382  return;
1383  }
1384  }
1385  }
1386  // No negative support, setting boolvar to true.
1387  demon_->inhibit(solver());
1388  boolvar_->SetValue(1);
1389  return;
1390  }
1391  }
1392  // No positive support, setting boolvar to false.
1393  demon_->inhibit(solver());
1394  boolvar_->SetValue(0);
1395  }
1396  }
1397 
1398  void TargetBound() {
1399  DCHECK(boolvar_->Bound());
1400  if (boolvar_->Min() == 1LL) {
1401  demon_->inhibit(solver());
1402  var_->SetValues(values_);
1403  } else {
1404  demon_->inhibit(solver());
1405  var_->RemoveValues(values_);
1406  }
1407  }
1408 
1409  IntVar* const var_;
1410  absl::flat_hash_set<int64> values_as_set_;
1411  std::vector<int64> values_;
1412  IntVar* const boolvar_;
1413  int support_;
1414  Demon* demon_;
1415  IntVarIterator* const domain_;
1416  int64 neg_support_;
1417 };
1418 
1419 template <class T>
1420 Constraint* BuildIsMemberCt(Solver* const solver, IntExpr* const expr,
1421  const std::vector<T>& values,
1422  IntVar* const boolvar) {
1423  // TODO(user): optimize this by copying the code from MakeMemberCt.
1424  // Simplify and filter if expr is a product.
1425  IntExpr* sub = nullptr;
1426  int64 coef = 1;
1427  if (solver->IsProduct(expr, &sub, &coef) && coef != 0 && coef != 1) {
1428  std::vector<int64> new_values;
1429  new_values.reserve(values.size());
1430  for (const int64 value : values) {
1431  if (value % coef == 0) {
1432  new_values.push_back(value / coef);
1433  }
1434  }
1435  return BuildIsMemberCt(solver, sub, new_values, boolvar);
1436  }
1437 
1438  std::set<T> set_of_values(values.begin(), values.end());
1439  std::vector<int64> filtered_values;
1440  bool all_values = false;
1441  if (expr->IsVar()) {
1442  IntVar* const var = expr->Var();
1443  for (const T value : set_of_values) {
1444  if (var->Contains(value)) {
1445  filtered_values.push_back(value);
1446  }
1447  }
1448  all_values = (filtered_values.size() == var->Size());
1449  } else {
1450  int64 emin = 0;
1451  int64 emax = 0;
1452  expr->Range(&emin, &emax);
1453  for (const T value : set_of_values) {
1454  if (value >= emin && value <= emax) {
1455  filtered_values.push_back(value);
1456  }
1457  }
1458  all_values = (filtered_values.size() == emax - emin + 1);
1459  }
1460  if (filtered_values.empty()) {
1461  return solver->MakeEquality(boolvar, Zero());
1462  } else if (all_values) {
1463  return solver->MakeEquality(boolvar, 1);
1464  } else if (filtered_values.size() == 1) {
1465  return solver->MakeIsEqualCstCt(expr, filtered_values.back(), boolvar);
1466  } else if (filtered_values.back() ==
1467  filtered_values.front() + filtered_values.size() - 1) {
1468  // Contiguous
1469  return solver->MakeIsBetweenCt(expr, filtered_values.front(),
1470  filtered_values.back(), boolvar);
1471  } else {
1472  return solver->RevAlloc(
1473  new IsMemberCt(solver, expr->Var(), filtered_values, boolvar));
1474  }
1475 }
1476 } // namespace
1477 
1479  const std::vector<int64>& values,
1480  IntVar* const boolvar) {
1481  return BuildIsMemberCt(this, expr, values, boolvar);
1482 }
1483 
1485  const std::vector<int>& values,
1486  IntVar* const boolvar) {
1487  return BuildIsMemberCt(this, expr, values, boolvar);
1488 }
1489 
1491  const std::vector<int64>& values) {
1492  IntVar* const b = MakeBoolVar();
1493  AddConstraint(MakeIsMemberCt(expr, values, b));
1494  return b;
1495 }
1496 
1498  const std::vector<int>& values) {
1499  IntVar* const b = MakeBoolVar();
1500  AddConstraint(MakeIsMemberCt(expr, values, b));
1501  return b;
1502 }
1503 
1504 namespace {
1505 class SortedDisjointForbiddenIntervalsConstraint : public Constraint {
1506  public:
1507  SortedDisjointForbiddenIntervalsConstraint(
1508  Solver* const solver, IntVar* const var,
1509  SortedDisjointIntervalList intervals)
1510  : Constraint(solver), var_(var), intervals_(std::move(intervals)) {}
1511 
1512  ~SortedDisjointForbiddenIntervalsConstraint() override {}
1513 
1514  void Post() override {
1515  Demon* const demon = solver()->MakeConstraintInitialPropagateCallback(this);
1516  var_->WhenRange(demon);
1517  }
1518 
1519  void InitialPropagate() override {
1520  const int64 vmin = var_->Min();
1521  const int64 vmax = var_->Max();
1522  const auto first_interval_it = intervals_.FirstIntervalGreaterOrEqual(vmin);
1523  if (first_interval_it == intervals_.end()) {
1524  // No interval intersects the variable's range. Nothing to do.
1525  return;
1526  }
1527  const auto last_interval_it = intervals_.LastIntervalLessOrEqual(vmax);
1528  if (last_interval_it == intervals_.end()) {
1529  // No interval intersects the variable's range. Nothing to do.
1530  return;
1531  }
1532  // TODO(user): Quick fail if first_interval_it == last_interval_it, which
1533  // would imply that the interval contains the entire range of the variable?
1534  if (vmin >= first_interval_it->start) {
1535  // The variable's minimum is inside a forbidden interval. Move it to the
1536  // interval's end.
1537  var_->SetMin(CapAdd(first_interval_it->end, 1));
1538  }
1539  if (vmax <= last_interval_it->end) {
1540  // Ditto, on the other side.
1541  var_->SetMax(CapSub(last_interval_it->start, 1));
1542  }
1543  }
1544 
1545  std::string DebugString() const override {
1546  return absl::StrFormat("ForbiddenIntervalCt(%s, %s)", var_->DebugString(),
1547  intervals_.DebugString());
1548  }
1549 
1550  void Accept(ModelVisitor* const visitor) const override {
1551  visitor->BeginVisitConstraint(ModelVisitor::kNotMember, this);
1552  visitor->VisitIntegerExpressionArgument(ModelVisitor::kExpressionArgument,
1553  var_);
1554  std::vector<int64> starts;
1555  std::vector<int64> ends;
1556  for (auto& interval : intervals_) {
1557  starts.push_back(interval.start);
1558  ends.push_back(interval.end);
1559  }
1560  visitor->VisitIntegerArrayArgument(ModelVisitor::kStartsArgument, starts);
1561  visitor->VisitIntegerArrayArgument(ModelVisitor::kEndsArgument, ends);
1562  visitor->EndVisitConstraint(ModelVisitor::kNotMember, this);
1563  }
1564 
1565  private:
1566  IntVar* const var_;
1567  const SortedDisjointIntervalList intervals_;
1568 };
1569 } // namespace
1570 
1572  std::vector<int64> starts,
1573  std::vector<int64> ends) {
1574  return RevAlloc(new SortedDisjointForbiddenIntervalsConstraint(
1575  this, expr->Var(), {starts, ends}));
1576 }
1577 
1579  std::vector<int> starts,
1580  std::vector<int> ends) {
1581  return RevAlloc(new SortedDisjointForbiddenIntervalsConstraint(
1582  this, expr->Var(), {starts, ends}));
1583 }
1584 
1586  SortedDisjointIntervalList intervals) {
1587  return RevAlloc(new SortedDisjointForbiddenIntervalsConstraint(
1588  this, expr->Var(), std::move(intervals)));
1589 }
1590 } // namespace operations_research
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define DCHECK(condition)
Definition: base/logging.h:884
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
Cast constraints are special channeling constraints designed to keep a variable in sync with an expre...
A constraint is the main modeling object.
virtual void InitialPropagate()=0
This method performs the initial propagation of the constraint.
virtual void Accept(ModelVisitor *const visitor) const
Accepts the given visitor.
virtual IntVar * Var()
Creates a Boolean variable representing the status of the constraint (false = constraint is violated,...
std::string DebugString() const override
virtual void Post()=0
This method is called when the constraint is processed by the solver.
void inhibit(Solver *const s)
This method inhibits the demon in the search tree below the current position.
The class IntExpr is the base of all integer expressions in constraint programming.
virtual void SetMax(int64 m)=0
virtual IntVar * Var()=0
Creates a variable from the expression.
virtual bool Bound() const
Returns true if the min and the max of the expression are equal.
virtual void SetMin(int64 m)=0
virtual bool IsVar() const
Returns true if the expression is indeed a variable.
virtual void Range(int64 *l, int64 *u)
By default calls Min() and Max(), but can be redefined when Min and Max code can be factorized.
virtual int64 Max() const =0
virtual int64 Min() const =0
virtual void WhenRange(Demon *d)=0
Attach a demon that will watch the min or the max of the expression.
The class IntVar is a subset of IntExpr.
IntVar * Var() override
Creates a variable from the expression.
virtual void RemoveValue(int64 v)=0
This method removes the value 'v' from the domain of the variable.
virtual bool Contains(int64 v) const =0
This method returns whether the value 'v' is in the domain of the variable.
virtual uint64 Size() const =0
This method returns the number of values in the domain of the variable.
bool IsVar() const override
Returns true if the expression is indeed a variable.
Constraint * MakeMemberCt(IntExpr *const expr, const std::vector< int64 > &values)
expr in set.
Definition: expr_cst.cc:1160
IntVar * MakeIsGreaterOrEqualCstVar(IntExpr *const var, int64 value)
status var of (var >= value)
Definition: expr_cst.cc:677
Constraint * MakeLess(IntExpr *const left, IntExpr *const right)
left < right
Definition: range_cst.cc:546
Constraint * MakeFalseConstraint()
This constraint always fails.
Definition: constraints.cc:520
Constraint * MakeEquality(IntExpr *const left, IntExpr *const right)
left == right
Definition: range_cst.cc:512
Constraint * MakeIsDifferentCt(IntExpr *const v1, IntExpr *const v2, IntVar *const b)
b == (v1 != v2)
Definition: range_cst.cc:686
Constraint * MakeLessOrEqual(IntExpr *const left, IntExpr *const right)
left <= right
Definition: range_cst.cc:526
Constraint * MakeIsLessCstCt(IntExpr *const v, int64 c, IntVar *const b)
b == (v < c)
Definition: expr_cst.cc:813
IntVar * MakeIsDifferentVar(IntExpr *const v1, IntExpr *const v2)
status var of (v1 != v2)
Definition: range_cst.cc:641
IntVar * MakeIsEqualVar(IntExpr *const v1, IntExpr *v2)
status var of (v1 == v2)
Definition: range_cst.cc:577
Constraint * MakeNotBetweenCt(IntExpr *const expr, int64 l, int64 u)
(expr < l || expr > u) This constraint is lazy as it will not make holes in the domain of variables.
Definition: expr_cst.cc:953
Constraint * MakeGreater(IntExpr *const left, IntExpr *const right)
left > right
Definition: range_cst.cc:560
Constraint * MakeBetweenCt(IntExpr *const expr, int64 l, int64 u)
(l <= expr <= u)
Definition: expr_cst.cc:920
Constraint * MakeIsEqualCstCt(IntExpr *const var, int64 value, IntVar *const boolvar)
boolvar == (var == value)
Definition: expr_cst.cc:485
IntVar * MakeIsDifferentCstVar(IntExpr *const var, int64 value)
status var of (var != value)
Definition: expr_cst.cc:578
Constraint * MakeIsGreaterCstCt(IntExpr *const v, int64 c, IntVar *const b)
b == (v > c)
Definition: expr_cst.cc:714
void AddConstraint(Constraint *const c)
Adds the constraint 'c' to the model.
IntVar * MakeIsMemberVar(IntExpr *const expr, const std::vector< int64 > &values)
Definition: expr_cst.cc:1490
IntVar * MakeIsEqualCstVar(IntExpr *const var, int64 value)
status var of (var == value)
Definition: expr_cst.cc:460
Constraint * MakeNotMemberCt(IntExpr *const expr, const std::vector< int64 > &values)
expr not in set.
Definition: expr_cst.cc:1229
Constraint * MakeIsEqualCt(IntExpr *const v1, IntExpr *v2, IntVar *const b)
b == (v1 == v2)
Definition: range_cst.cc:622
Constraint * MakeTrueConstraint()
This constraint always succeeds.
Definition: constraints.cc:515
Constraint * MakeIsBetweenCt(IntExpr *const expr, int64 l, int64 u, IntVar *const b)
b == (l <= expr <= u)
Definition: expr_cst.cc:1048
IntExpr * MakeDifference(IntExpr *const left, IntExpr *const right)
left - right
IntVar * MakeBoolVar()
MakeBoolVar will create a variable with a {0, 1} domain.
Constraint * MakeNonEquality(IntExpr *const left, IntExpr *const right)
left != right
Definition: range_cst.cc:564
IntVar * MakeIsBetweenVar(IntExpr *const v, int64 l, int64 u)
Definition: expr_cst.cc:1084
Constraint * MakeIsMemberCt(IntExpr *const expr, const std::vector< int64 > &values, IntVar *const boolvar)
boolvar == (expr in set)
Definition: expr_cst.cc:1478
T * RevAlloc(T *object)
Registers the given object as being reversible.
IntExpr * MakeSum(IntExpr *const left, IntExpr *const right)
left + right.
Constraint * MakeIsDifferentCstCt(IntExpr *const var, int64 value, IntVar *const boolvar)
boolvar == (var != value)
Definition: expr_cst.cc:587
IntVar * MakeIsLessCstVar(IntExpr *const var, int64 value)
status var of (var < value)
Definition: expr_cst.cc:793
IntVar * MakeIsGreaterCstVar(IntExpr *const var, int64 value)
status var of (var > value)
Definition: expr_cst.cc:694
IntVar * MakeIsLessOrEqualCstVar(IntExpr *const var, int64 value)
status var of (var <= value)
Definition: expr_cst.cc:776
Constraint * MakeIsLessOrEqualCstCt(IntExpr *const var, int64 value, IntVar *const boolvar)
boolvar == (var <= value)
Definition: expr_cst.cc:797
Constraint * MakeGreaterOrEqual(IntExpr *const left, IntExpr *const right)
left >= right
Definition: range_cst.cc:542
Constraint * MakeIsGreaterOrEqualCstCt(IntExpr *const var, int64 value, IntVar *const boolvar)
boolvar == (var >= value)
Definition: expr_cst.cc:698
IntVar * MakeIntConst(int64 val, const std::string &name)
IntConst will create a constant expression.
This class represents a sorted list of disjoint, closed intervals.
int64 value
IntVar *const expr_
Definition: element.cc:85
IntVar * var
Definition: expr_array.cc:1858
int64 coef
Definition: expr_array.cc:1859
ABSL_FLAG(int, cache_initial_size, 1024, "Initial size of the array of the hash " "table of caches for objects of type Var(x == 3)")
const int64 cst_
int64_t int64
static const int64 kint64min
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 CapSub(int64 x, int64 y)
Demon * MakeConstraintDemon0(Solver *const s, T *const ct, void(T::*method)(), const std::string &name)
int64 PosIntDivUp(int64 e, int64 v)
int64 PosIntDivDown(int64 e, int64 v)
int64 CapAdd(int64 x, int64 y)
std::vector< int64 > ToInt64Vector(const std::vector< int > &input)
Definition: utilities.cc:822
IntervalVar * interval
Definition: resource.cc:98
IntervalVar *const target_var_