1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16#include <algorithm>

17#include <cmath>

18#include <cstdint>

19#include <cstdlib>

20#include <limits>

21#include <string>

22#include <vector>

23

24#include "absl/strings/str_format.h"

25#include "absl/strings/str_join.h"

26#include "absl/strings/string_view.h"

27#include "absl/types/span.h"

35

37namespace {

38

39

41 public:

42 TreeArrayConstraint(Solver* const solver, const std::vector<IntVar*>& vars,

43 IntVar* const sum_var)

44 : CastConstraint(solver, sum_var),

45 vars_(vars),

46 block_size_(solver->parameters().array_split_size()) {

47 std::vector<int> lengths;

48 lengths.push_back(vars_.size());

49 while (lengths.back() > 1) {

50 const int current = lengths.back();

51 lengths.push_back((current + block_size_ - 1) / block_size_);

52 }

53 tree_.resize(lengths.size());

54 for (int i = 0; i < lengths.size(); ++i) {

55 tree_[i].resize(lengths[lengths.size() - i - 1]);

56 }

57 DCHECK_GE(tree_.size(), 1);

58 DCHECK_EQ(1, tree_[0].size());

59 root_node_ = &tree_[0][0];

60 }

61

62 std::string DebugStringInternal(absl::string_view name) const {

63 return absl::StrFormat("%s(%s) == %s", name,

65 target_var_->DebugString());

66 }

67

68 void AcceptInternal(const std::string& name,

69 ModelVisitor* const visitor) const {

70 visitor->BeginVisitConstraint(name, this);

72 vars_);

74 target_var_);

75 visitor->EndVisitConstraint(name, this);

76 }

77

78

79 void ReduceRange(int depth, int position, int64_t delta_min,

80 int64_t delta_max) {

81 NodeInfo* const info = &tree_[depth][position];

82 if (delta_min > 0) {

83 info->node_min.SetValue(solver(),

84 CapAdd(info->node_min.Value(), delta_min));

85 }

86 if (delta_max > 0) {

87 info->node_max.SetValue(solver(),

88 CapSub(info->node_max.Value(), delta_max));

89 }

90 }

91

92

93 void SetRange(int depth, int position, int64_t new_min, int64_t new_max) {

94 NodeInfo* const info = &tree_[depth][position];

95 if (new_min > info->node_min.Value()) {

96 info->node_min.SetValue(solver(), new_min);

97 }

98 if (new_max < info->node_max.Value()) {

99 info->node_max.SetValue(solver(), new_max);

100 }

101 }

102

103 void InitLeaf(int position, int64_t var_min, int64_t var_max) {

104 InitNode(MaxDepth(), position, var_min, var_max);

105 }

106

107 void InitNode(int depth, int position, int64_t node_min, int64_t node_max) {

108 tree_[depth][position].node_min.SetValue(solver(), node_min);

109 tree_[depth][position].node_max.SetValue(solver(), node_max);

110 }

111

112 int64_t Min(int depth, int position) const {

113 return tree_[depth][position].node_min.Value();

114 }

115

116 int64_t Max(int depth, int position) const {

117 return tree_[depth][position].node_max.Value();

118 }

119

120 int64_t RootMin() const { return root_node_->node_min.Value(); }

121

122 int64_t RootMax() const { return root_node_->node_max.Value(); }

123

124 int Parent(int position) const { return position / block_size_; }

125

126 int ChildStart(int position) const { return position * block_size_; }

127

128 int ChildEnd(int depth, int position) const {

129 DCHECK_LT(depth + 1, tree_.size());

130 return std::min((position + 1) * block_size_ - 1, Width(depth + 1) - 1);

131 }

132

133 bool IsLeaf(int depth) const { return depth == MaxDepth(); }

134

135 int MaxDepth() const { return tree_.size() - 1; }

136

137 int Width(int depth) const { return tree_[depth].size(); }

138

139 protected:

140 const std::vector<IntVar*> vars_;

141

142 private:

143 struct NodeInfo {

144 NodeInfo() : node_min(0), node_max(0) {}

145 Rev<int64_t> node_min;

146 Rev<int64_t> node_max;

147 };

148

149 std::vector<std::vector<NodeInfo> > tree_;

150 const int block_size_;

151 NodeInfo* root_node_;

152};

153

154

155

156

157

158

159

160

161

162

163

164

165

166class SumConstraint : public TreeArrayConstraint {

167 public:

168 SumConstraint(Solver* const solver, const std::vector<IntVar*>& vars,

169 IntVar* const sum_var)

170 : TreeArrayConstraint(solver, vars, sum_var), sum_demon_(nullptr) {}

171

172 ~SumConstraint() override {}

173

174 void Post() override {

175 for (int i = 0; i < vars_.size(); ++i) {

177 solver(), this, &SumConstraint::LeafChanged, "LeafChanged", i);

178 vars_[i]->WhenRange(demon);

179 }

181 solver(), this, &SumConstraint::SumChanged, "SumChanged"));

182 target_var_->WhenRange(sum_demon_);

183 }

184

185 void InitialPropagate() override {

186

187 for (int i = 0; i < vars_.size(); ++i) {

188 InitLeaf(i, vars_[i]->Min(), vars_[i]->Max());

189 }

190

191 for (int i = MaxDepth() - 1; i >= 0; --i) {

192 for (int j = 0; j < Width(i); ++j) {

193 int64_t sum_min = 0;

194 int64_t sum_max = 0;

195 const int block_start = ChildStart(j);

196 const int block_end = ChildEnd(i, j);

197 for (int k = block_start; k <= block_end; ++k) {

198 sum_min = CapAdd(sum_min, Min(i + 1, k));

199 sum_max = CapAdd(sum_max, Max(i + 1, k));

200 }

201 InitNode(i, j, sum_min, sum_max);

202 }

203 }

204

205 target_var_->SetRange(RootMin(), RootMax());

206

207

208 SumChanged();

209 }

210

211 void SumChanged() {

212 if (target_var_->Max() == RootMin() &&

213 target_var_->Max() != std::numeric_limits<int64_t>::max()) {

214

215 for (int i = 0; i < vars_.size(); ++i) {

216 vars_[i]->SetValue(vars_[i]->Min());

217 }

218 } else if (target_var_->Min() == RootMax() &&

219 target_var_->Min() != std::numeric_limits<int64_t>::min()) {

220

221 for (int i = 0; i < vars_.size(); ++i) {

222 vars_[i]->SetValue(vars_[i]->Max());

223 }

224 } else {

225 PushDown(0, 0, target_var_->Min(), target_var_->Max());

226 }

227 }

228

229 void PushDown(int depth, int position, int64_t new_min, int64_t new_max) {

230

231 if (new_min <= Min(depth, position) && new_max >= Max(depth, position)) {

232 return;

233 }

234

235

236 if (IsLeaf(depth)) {

237 vars_[position]->SetRange(new_min, new_max);

238 return;

239 }

240

241

242

243

244

245 const int64_t sum_min = Min(depth, position);

246 const int64_t sum_max = Max(depth, position);

247

248

249 new_max = std::min(sum_max, new_max);

250 new_min = std::max(sum_min, new_min);

251

252

253 if (new_max < sum_min || new_min > sum_max) {

254 solver()->Fail();

255 }

256

257

258 const int block_start = ChildStart(position);

259 const int block_end = ChildEnd(depth, position);

260 for (int i = block_start; i <= block_end; ++i) {

261 const int64_t target_var_min = Min(depth + 1, i);

262 const int64_t target_var_max = Max(depth + 1, i);

263 const int64_t residual_min = CapSub(sum_min, target_var_min);

264 const int64_t residual_max = CapSub(sum_max, target_var_max);

265 PushDown(depth + 1, i, CapSub(new_min, residual_max),

266 CapSub(new_max, residual_min));

267 }

268

269

270 }

271

272 void LeafChanged(int term_index) {

273 IntVar* const var = vars_[term_index];

274 PushUp(term_index, CapSub(var->Min(), var->OldMin()),

275 CapSub(var->OldMax(), var->Max()));

276 EnqueueDelayedDemon(sum_demon_);

277 }

278

279 void PushUp(int position, int64_t delta_min, int64_t delta_max) {

280 DCHECK_GE(delta_max, 0);

281 DCHECK_GE(delta_min, 0);

282 DCHECK_GT(CapAdd(delta_min, delta_max), 0);

283 for (int depth = MaxDepth(); depth >= 0; --depth) {

284 ReduceRange(depth, position, delta_min, delta_max);

285 position = Parent(position);

286 }

287 DCHECK_EQ(0, position);

288 target_var_->SetRange(RootMin(), RootMax());

289 }

290

291 std::string DebugString() const override {

292 return DebugStringInternal("Sum");

293 }

294

295 void Accept(ModelVisitor* const visitor) const override {

297 }

298

299 private:

300 Demon* sum_demon_;

301};

302

303

304class SmallSumConstraint : public Constraint {

305 public:

306 SmallSumConstraint(Solver* const solver, const std::vector<IntVar*>& vars,

307 IntVar* const target_var)

308 : Constraint(solver),

309 vars_(vars),

310 target_var_(target_var),

311 computed_min_(0),

312 computed_max_(0),

313 sum_demon_(nullptr) {}

314

315 ~SmallSumConstraint() override {}

316

317 void Post() override {

318 for (int i = 0; i < vars_.size(); ++i) {

319 if (!vars_[i]->Bound()) {

321 solver(), this, &SmallSumConstraint::VarChanged, "VarChanged",

322 vars_[i]);

323 vars_[i]->WhenRange(demon);

324 }

325 }

327 solver(), this, &SmallSumConstraint::SumChanged, "SumChanged"));

328 target_var_->WhenRange(sum_demon_);

329 }

330

331 void InitialPropagate() override {

332

333 int64_t sum_min = 0;

334 int64_t sum_max = 0;

335 for (IntVar* const var : vars_) {

336 sum_min = CapAdd(sum_min, var->Min());

337 sum_max = CapAdd(sum_max, var->Max());

338 }

339

340

341 computed_min_.SetValue(solver(), sum_min);

342 computed_max_.SetValue(solver(), sum_max);

343 target_var_->SetRange(sum_min, sum_max);

344

345

346 SumChanged();

347 }

348

349 void SumChanged() {

350 int64_t new_min = target_var_->Min();

351 int64_t new_max = target_var_->Max();

352 const int64_t sum_min = computed_min_.Value();

353 const int64_t sum_max = computed_max_.Value();

354 if (new_max == sum_min && new_max != std::numeric_limits<int64_t>::max()) {

355

356 for (int i = 0; i < vars_.size(); ++i) {

357 vars_[i]->SetValue(vars_[i]->Min());

358 }

359 } else if (new_min == sum_max &&

360 new_min != std::numeric_limits<int64_t>::min()) {

361

362 for (int i = 0; i < vars_.size(); ++i) {

363 vars_[i]->SetValue(vars_[i]->Max());

364 }

365 } else {

366 if (new_min > sum_min || new_max < sum_max) {

367

368 new_max = std::min(sum_max, new_max);

369 new_min = std::max(sum_min, new_min);

370

371

372 if (new_max < sum_min || new_min > sum_max) {

373 solver()->Fail();

374 }

375

376

377 for (IntVar* const var : vars_) {

378 const int64_t var_min = var->Min();

379 const int64_t var_max = var->Max();

380 const int64_t residual_min = CapSub(sum_min, var_min);

381 const int64_t residual_max = CapSub(sum_max, var_max);

382 var->SetRange(CapSub(new_min, residual_max),

383 CapSub(new_max, residual_min));

384 }

385 }

386 }

387 }

388

389 void VarChanged(IntVar* var) {

390 const int64_t delta_min = CapSub(var->Min(), var->OldMin());

391 const int64_t delta_max = CapSub(var->OldMax(), var->Max());

392 computed_min_.Add(solver(), delta_min);

393 computed_max_.Add(solver(), -delta_max);

394 if (computed_max_.Value() < target_var_->Max() ||

395 computed_min_.Value() > target_var_->Min()) {

396 target_var_->SetRange(computed_min_.Value(), computed_max_.Value());

397 } else {

398 EnqueueDelayedDemon(sum_demon_);

399 }

400 }

401

402 std::string DebugString() const override {

403 return absl::StrFormat("SmallSum(%s) == %s",

405 target_var_->DebugString());

406 }

407

408 void Accept(ModelVisitor* const visitor) const override {

411 vars_);

413 target_var_);

415 }

416

417 private:

418 const std::vector<IntVar*> vars_;

419 IntVar* target_var_;

420 NumericalRev<int64_t> computed_min_;

421 NumericalRev<int64_t> computed_max_;

422 Demon* sum_demon_;

423};

424

425

426bool DetectSumOverflow(const std::vector<IntVar*>& vars) {

427 int64_t sum_min = 0;

428 int64_t sum_max = 0;

429 for (int i = 0; i < vars.size(); ++i) {

430 sum_min = CapAdd(sum_min, vars[i]->Min());

431 sum_max = CapAdd(sum_max, vars[i]->Max());

432 if (sum_min == std::numeric_limits<int64_t>::min() ||

433 sum_max == std::numeric_limits<int64_t>::max()) {

434 return true;

435 }

436 }

437 return false;

438}

439

440

441class SafeSumConstraint : public TreeArrayConstraint {

442 public:

443 SafeSumConstraint(Solver* const solver, const std::vector<IntVar*>& vars,

444 IntVar* const sum_var)

445 : TreeArrayConstraint(solver, vars, sum_var), sum_demon_(nullptr) {}

446

447 ~SafeSumConstraint() override {}

448

449 void Post() override {

450 for (int i = 0; i < vars_.size(); ++i) {

452 solver(), this, &SafeSumConstraint::LeafChanged, "LeafChanged", i);

453 vars_[i]->WhenRange(demon);

454 }

456 solver(), this, &SafeSumConstraint::SumChanged, "SumChanged"));

457 target_var_->WhenRange(sum_demon_);

458 }

459

460 void SafeComputeNode(int depth, int position, int64_t* const sum_min,

461 int64_t* const sum_max) {

462 DCHECK_LT(depth, MaxDepth());

463 const int block_start = ChildStart(position);

464 const int block_end = ChildEnd(depth, position);

465 for (int k = block_start; k <= block_end; ++k) {

466 if (*sum_min != std::numeric_limits<int64_t>::min()) {

467 *sum_min = CapAdd(*sum_min, Min(depth + 1, k));

468 }

469 if (*sum_max != std::numeric_limits<int64_t>::max()) {

470 *sum_max = CapAdd(*sum_max, Max(depth + 1, k));

471 }

472 if (*sum_min == std::numeric_limits<int64_t>::min() &&

473 *sum_max == std::numeric_limits<int64_t>::max()) {

474 break;

475 }

476 }

477 }

478

479 void InitialPropagate() override {

480

481 for (int i = 0; i < vars_.size(); ++i) {

482 InitLeaf(i, vars_[i]->Min(), vars_[i]->Max());

483 }

484

485 for (int i = MaxDepth() - 1; i >= 0; --i) {

486 for (int j = 0; j < Width(i); ++j) {

487 int64_t sum_min = 0;

488 int64_t sum_max = 0;

489 SafeComputeNode(i, j, &sum_min, &sum_max);

490 InitNode(i, j, sum_min, sum_max);

491 }

492 }

493

494 target_var_->SetRange(RootMin(), RootMax());

495

496

497 SumChanged();

498 }

499

500 void SumChanged() {

501 DCHECK(CheckInternalState());

502 if (target_var_->Max() == RootMin()) {

503

504 for (int i = 0; i < vars_.size(); ++i) {

505 vars_[i]->SetValue(vars_[i]->Min());

506 }

507 } else if (target_var_->Min() == RootMax()) {

508

509 for (int i = 0; i < vars_.size(); ++i) {

510 vars_[i]->SetValue(vars_[i]->Max());

511 }

512 } else {

513 PushDown(0, 0, target_var_->Min(), target_var_->Max());

514 }

515 }

516

517 void PushDown(int depth, int position, int64_t new_min, int64_t new_max) {

518

519 if (new_min <= Min(depth, position) && new_max >= Max(depth, position)) {

520 return;

521 }

522

523

524 if (IsLeaf(depth)) {

525 vars_[position]->SetRange(new_min, new_max);

526 return;

527 }

528

529

530

531

532

533 const int64_t sum_min = Min(depth, position);

534 const int64_t sum_max = Max(depth, position);

535

536

537 new_max = std::min(sum_max, new_max);

538 new_min = std::max(sum_min, new_min);

539

540

541 if (new_max < sum_min || new_min > sum_max) {

542 solver()->Fail();

543 }

544

545

546 const int block_start = ChildStart(position);

547 const int block_end = ChildEnd(depth, position);

548 for (int pos = block_start; pos <= block_end; ++pos) {

549 const int64_t target_var_min = Min(depth + 1, pos);

550 const int64_t residual_min =

551 sum_min != std::numeric_limits<int64_t>::min()

552 ? CapSub(sum_min, target_var_min)

553 : std::numeric_limits<int64_t>::min();

554 const int64_t target_var_max = Max(depth + 1, pos);

555 const int64_t residual_max =

556 sum_max != std::numeric_limits<int64_t>::max()

557 ? CapSub(sum_max, target_var_max)

558 : std::numeric_limits<int64_t>::max();

559 PushDown(depth + 1, pos,

560 (residual_max == std::numeric_limits<int64_t>::min()

561 ? std::numeric_limits<int64_t>::min()

562 : CapSub(new_min, residual_max)),

563 (residual_min == std::numeric_limits<int64_t>::max()

564 ? std::numeric_limits<int64_t>::min()

565 : CapSub(new_max, residual_min)));

566 }

567

568

569 }

570

571 void LeafChanged(int term_index) {

572 IntVar* const var = vars_[term_index];

573 PushUp(term_index, CapSub(var->Min(), var->OldMin()),

574 CapSub(var->OldMax(), var->Max()));

575 EnqueueDelayedDemon(sum_demon_);

576 }

577

578 void PushUp(int position, int64_t delta_min, int64_t delta_max) {

579 DCHECK_GE(delta_max, 0);

580 DCHECK_GE(delta_min, 0);

581 if (CapAdd(delta_min, delta_max) == 0) {

582

583

584 return;

585 }

586 bool delta_corrupted = false;

587 for (int depth = MaxDepth(); depth >= 0; --depth) {

588 if (Min(depth, position) != std::numeric_limits<int64_t>::min() &&

589 Max(depth, position) != std::numeric_limits<int64_t>::max() &&

590 delta_min != std::numeric_limits<int64_t>::max() &&

591 delta_max != std::numeric_limits<int64_t>::max() &&

592 !delta_corrupted) {

593 ReduceRange(depth, position, delta_min, delta_max);

594 } else if (depth == MaxDepth()) {

595 SetRange(depth, position, vars_[position]->Min(),

596 vars_[position]->Max());

597 delta_corrupted = true;

598 } else {

599 int64_t sum_min = 0;

600 int64_t sum_max = 0;

601 SafeComputeNode(depth, position, &sum_min, &sum_max);

602 if (sum_min == std::numeric_limits<int64_t>::min() &&

603 sum_max == std::numeric_limits<int64_t>::max()) {

604 return;

605 }

606 SetRange(depth, position, sum_min, sum_max);

607 delta_corrupted = true;

608 }

609 position = Parent(position);

610 }

611 DCHECK_EQ(0, position);

612 target_var_->SetRange(RootMin(), RootMax());

613 }

614

615 std::string DebugString() const override {

616 return DebugStringInternal("Sum");

617 }

618

619 void Accept(ModelVisitor* const visitor) const override {

621 }

622

623 private:

624 bool CheckInternalState() {

625 for (int i = 0; i < vars_.size(); ++i) {

626 CheckLeaf(i, vars_[i]->Min(), vars_[i]->Max());

627 }

628

629 for (int i = MaxDepth() - 1; i >= 0; --i) {

630 for (int j = 0; j < Width(i); ++j) {

631 int64_t sum_min = 0;

632 int64_t sum_max = 0;

633 SafeComputeNode(i, j, &sum_min, &sum_max);

634 CheckNode(i, j, sum_min, sum_max);

635 }

636 }

637 return true;

638 }

639

640 void CheckLeaf(int position, int64_t var_min, int64_t var_max) {

641 CheckNode(MaxDepth(), position, var_min, var_max);

642 }

643

644 void CheckNode(int depth, int position, int64_t node_min, int64_t node_max) {

645 DCHECK_EQ(Min(depth, position), node_min);

646 DCHECK_EQ(Max(depth, position), node_max);

647 }

648

649 Demon* sum_demon_;

650};

651

652

653

654

655class MinConstraint : public TreeArrayConstraint {

656 public:

657 MinConstraint(Solver* const solver, const std::vector<IntVar*>& vars,

658 IntVar* const min_var)

659 : TreeArrayConstraint(solver, vars, min_var), min_demon_(nullptr) {}

660

661 ~MinConstraint() override {}

662

663 void Post() override {

664 for (int i = 0; i < vars_.size(); ++i) {

666 solver(), this, &MinConstraint::LeafChanged, "LeafChanged", i);

667 vars_[i]->WhenRange(demon);

668 }

670 solver(), this, &MinConstraint::MinVarChanged, "MinVarChanged"));

671 target_var_->WhenRange(min_demon_);

672 }

673

674 void InitialPropagate() override {

675

676 for (int i = 0; i < vars_.size(); ++i) {

677 InitLeaf(i, vars_[i]->Min(), vars_[i]->Max());

678 }

679

680

681 for (int i = MaxDepth() - 1; i >= 0; --i) {

682 for (int j = 0; j < Width(i); ++j) {

683 int64_t min_min = std::numeric_limits<int64_t>::max();

684 int64_t min_max = std::numeric_limits<int64_t>::max();

685 const int block_start = ChildStart(j);

686 const int block_end = ChildEnd(i, j);

687 for (int k = block_start; k <= block_end; ++k) {

688 min_min = std::min(min_min, Min(i + 1, k));

689 min_max = std::min(min_max, Max(i + 1, k));

690 }

691 InitNode(i, j, min_min, min_max);

692 }

693 }

694

695 target_var_->SetRange(RootMin(), RootMax());

696

697

698 MinVarChanged();

699 }

700

701 void MinVarChanged() {

702 PushDown(0, 0, target_var_->Min(), target_var_->Max());

703 }

704

705 void PushDown(int depth, int position, int64_t new_min, int64_t new_max) {

706

707 if (new_min <= Min(depth, position) && new_max >= Max(depth, position)) {

708 return;

709 }

710

711

712 if (IsLeaf(depth)) {

713 vars_[position]->SetRange(new_min, new_max);

714 return;

715 }

716

717 const int64_t node_min = Min(depth, position);

718 const int64_t node_max = Max(depth, position);

719

720 int candidate = -1;

721 int active = 0;

722 const int block_start = ChildStart(position);

723 const int block_end = ChildEnd(depth, position);

724

725 if (new_max < node_max) {

726

727 for (int i = block_start; i <= block_end; ++i) {

728 if (Min(depth + 1, i) <= new_max) {

729 if (active++ >= 1) {

730 break;

731 }

732 candidate = i;

733 }

734 }

735 if (active == 0) {

736 solver()->Fail();

737 }

738 }

739

740 if (node_min < new_min) {

741 for (int i = block_start; i <= block_end; ++i) {

742 if (i == candidate && active == 1) {

743 PushDown(depth + 1, i, new_min, new_max);

744 } else {

745 PushDown(depth + 1, i, new_min, Max(depth + 1, i));

746 }

747 }

748 } else if (active == 1) {

749 PushDown(depth + 1, candidate, Min(depth + 1, candidate), new_max);

750 }

751 }

752

753

754 void LeafChanged(int term_index) {

755 IntVar* const var = vars_[term_index];

756 SetRange(MaxDepth(), term_index, var->Min(), var->Max());

757 const int parent_depth = MaxDepth() - 1;

758 const int parent = Parent(term_index);

759 const int64_t old_min = var->OldMin();

760 const int64_t var_min = var->Min();

761 const int64_t var_max = var->Max();

762 if ((old_min == Min(parent_depth, parent) && old_min != var_min) ||

763 var_max < Max(parent_depth, parent)) {

764

765 PushUp(term_index);

766 }

767 }

768

769 void PushUp(int position) {

770 int depth = MaxDepth();

771 while (depth > 0) {

772 const int parent = Parent(position);

773 const int parent_depth = depth - 1;

774 int64_t min_min = std::numeric_limits<int64_t>::max();

775 int64_t min_max = std::numeric_limits<int64_t>::max();

776 const int block_start = ChildStart(parent);

777 const int block_end = ChildEnd(parent_depth, parent);

778 for (int k = block_start; k <= block_end; ++k) {

779 min_min = std::min(min_min, Min(depth, k));

780 min_max = std::min(min_max, Max(depth, k));

781 }

782 if (min_min > Min(parent_depth, parent) ||

783 min_max < Max(parent_depth, parent)) {

784 SetRange(parent_depth, parent, min_min, min_max);

785 } else {

786 break;

787 }

788 depth = parent_depth;

789 position = parent;

790 }

791 if (depth == 0) {

792 target_var_->SetRange(RootMin(), RootMax());

793 }

794 MinVarChanged();

795 }

796

797 std::string DebugString() const override {

798 return DebugStringInternal("Min");

799 }

800

801 void Accept(ModelVisitor* const visitor) const override {

803 }

804

805 private:

806 Demon* min_demon_;

807};

808

809class SmallMinConstraint : public Constraint {

810 public:

811 SmallMinConstraint(Solver* const solver, const std::vector<IntVar*>& vars,

812 IntVar* const target_var)

813 : Constraint(solver),

814 vars_(vars),

815 target_var_(target_var),

816 computed_min_(0),

817 computed_max_(0) {}

818

819 ~SmallMinConstraint() override {}

820

821 void Post() override {

822 for (int i = 0; i < vars_.size(); ++i) {

823 if (!vars_[i]->Bound()) {

825 solver(), this, &SmallMinConstraint::VarChanged, "VarChanged",

826 vars_[i]);

827 vars_[i]->WhenRange(demon);

828 }

829 }

831 solver(), this, &SmallMinConstraint::MinVarChanged, "MinVarChanged"));

832 target_var_->WhenRange(mdemon);

833 }

834

835 void InitialPropagate() override {

836 int64_t min_min = std::numeric_limits<int64_t>::max();

837 int64_t min_max = std::numeric_limits<int64_t>::max();

838 for (IntVar* const var : vars_) {

839 min_min = std::min(min_min, var->Min());

840 min_max = std::min(min_max, var->Max());

841 }

842 computed_min_.SetValue(solver(), min_min);

843 computed_max_.SetValue(solver(), min_max);

844

845 target_var_->SetRange(min_min, min_max);

846

847

848 MinVarChanged();

849 }

850

851 std::string DebugString() const override {

852 return absl::StrFormat("SmallMin(%s) == %s",

854 target_var_->DebugString());

855 }

856

857 void Accept(ModelVisitor* const visitor) const override {

860 vars_);

862 target_var_);

864 }

865

866 private:

867 void VarChanged(IntVar* var) {

868 const int64_t old_min = var->OldMin();

869 const int64_t var_min = var->Min();

870 const int64_t var_max = var->Max();

871 if ((old_min == computed_min_.Value() && old_min != var_min) ||

872 var_max < computed_max_.Value()) {

873

874 int64_t min_min = std::numeric_limits<int64_t>::max();

875 int64_t min_max = std::numeric_limits<int64_t>::max();

876 for (IntVar* const var : vars_) {

877 min_min = std::min(min_min, var->Min());

878 min_max = std::min(min_max, var->Max());

879 }

880 if (min_min > computed_min_.Value() || min_max < computed_max_.Value()) {

881 computed_min_.SetValue(solver(), min_min);

882 computed_max_.SetValue(solver(), min_max);

883 target_var_->SetRange(computed_min_.Value(), computed_max_.Value());

884 }

885 }

886 MinVarChanged();

887 }

888

889 void MinVarChanged() {

890 const int64_t new_min = target_var_->Min();

891 const int64_t new_max = target_var_->Max();

892

893 if (new_min <= computed_min_.Value() && new_max >= computed_max_.Value()) {

894 return;

895 }

896

897 IntVar* candidate = nullptr;

898 int active = 0;

899

900 if (new_max < computed_max_.Value()) {

901

902 for (IntVar* const var : vars_) {

903 if (var->Min() <= new_max) {

904 if (active++ >= 1) {

905 break;

906 }

907 candidate = var;

908 }

909 }

910 if (active == 0) {

911 solver()->Fail();

912 }

913 }

914 if (computed_min_.Value() < new_min) {

915 if (active == 1) {

916 candidate->SetRange(new_min, new_max);

917 } else {

918 for (IntVar* const var : vars_) {

919 var->SetMin(new_min);

920 }

921 }

922 } else if (active == 1) {

923 candidate->SetMax(new_max);

924 }

925 }

926

927 std::vector<IntVar*> vars_;

928 IntVar* const target_var_;

929 Rev<int64_t> computed_min_;

930 Rev<int64_t> computed_max_;

931};

932

933

934

935

936class MaxConstraint : public TreeArrayConstraint {

937 public:

938 MaxConstraint(Solver* const solver, const std::vector<IntVar*>& vars,

939 IntVar* const max_var)

940 : TreeArrayConstraint(solver, vars, max_var), max_demon_(nullptr) {}

941

942 ~MaxConstraint() override {}

943

944 void Post() override {

945 for (int i = 0; i < vars_.size(); ++i) {

947 solver(), this, &MaxConstraint::LeafChanged, "LeafChanged", i);

948 vars_[i]->WhenRange(demon);

949 }

951 solver(), this, &MaxConstraint::MaxVarChanged, "MaxVarChanged"));

952 target_var_->WhenRange(max_demon_);

953 }

954

955 void InitialPropagate() override {

956

957 for (int i = 0; i < vars_.size(); ++i) {

958 InitLeaf(i, vars_[i]->Min(), vars_[i]->Max());

959 }

960

961

962 for (int i = MaxDepth() - 1; i >= 0; --i) {

963 for (int j = 0; j < Width(i); ++j) {

964 int64_t max_min = std::numeric_limits<int64_t>::min();

965 int64_t max_max = std::numeric_limits<int64_t>::min();

966 const int block_start = ChildStart(j);

967 const int block_end = ChildEnd(i, j);

968 for (int k = block_start; k <= block_end; ++k) {

969 max_min = std::max(max_min, Min(i + 1, k));

970 max_max = std::max(max_max, Max(i + 1, k));

971 }

972 InitNode(i, j, max_min, max_max);

973 }

974 }

975

976 target_var_->SetRange(RootMin(), RootMax());

977

978

979 MaxVarChanged();

980 }

981

982 void MaxVarChanged() {

983 PushDown(0, 0, target_var_->Min(), target_var_->Max());

984 }

985

986 void PushDown(int depth, int position, int64_t new_min, int64_t new_max) {

987

988 if (new_min <= Min(depth, position) && new_max >= Max(depth, position)) {

989 return;

990 }

991

992

993 if (IsLeaf(depth)) {

994 vars_[position]->SetRange(new_min, new_max);

995 return;

996 }

997

998 const int64_t node_min = Min(depth, position);

999 const int64_t node_max = Max(depth, position);

1000

1001 int candidate = -1;

1002 int active = 0;

1003 const int block_start = ChildStart(position);

1004 const int block_end = ChildEnd(depth, position);

1005

1006 if (node_min < new_min) {

1007

1008 for (int i = block_start; i <= block_end; ++i) {

1009 if (Max(depth + 1, i) >= new_min) {

1010 if (active++ >= 1) {

1011 break;

1012 }

1013 candidate = i;

1014 }

1015 }

1016 if (active == 0) {

1017 solver()->Fail();

1018 }

1019 }

1020

1021 if (node_max > new_max) {

1022 for (int i = block_start; i <= block_end; ++i) {

1023 if (i == candidate && active == 1) {

1024 PushDown(depth + 1, i, new_min, new_max);

1025 } else {

1026 PushDown(depth + 1, i, Min(depth + 1, i), new_max);

1027 }

1028 }

1029 } else if (active == 1) {

1030 PushDown(depth + 1, candidate, new_min, Max(depth + 1, candidate));

1031 }

1032 }

1033

1034 void LeafChanged(int term_index) {

1035 IntVar* const var = vars_[term_index];

1036 SetRange(MaxDepth(), term_index, var->Min(), var->Max());

1037 const int parent_depth = MaxDepth() - 1;

1038 const int parent = Parent(term_index);

1039 const int64_t old_max = var->OldMax();

1040 const int64_t var_min = var->Min();

1041 const int64_t var_max = var->Max();

1042 if ((old_max == Max(parent_depth, parent) && old_max != var_max) ||

1043 var_min > Min(parent_depth, parent)) {

1044

1045 PushUp(term_index);

1046 }

1047 }

1048

1049 void PushUp(int position) {

1050 int depth = MaxDepth();

1051 while (depth > 0) {

1052 const int parent = Parent(position);

1053 const int parent_depth = depth - 1;

1054 int64_t max_min = std::numeric_limits<int64_t>::min();

1055 int64_t max_max = std::numeric_limits<int64_t>::min();

1056 const int block_start = ChildStart(parent);

1057 const int block_end = ChildEnd(parent_depth, parent);

1058 for (int k = block_start; k <= block_end; ++k) {

1059 max_min = std::max(max_min, Min(depth, k));

1060 max_max = std::max(max_max, Max(depth, k));

1061 }

1062 if (max_min > Min(parent_depth, parent) ||

1063 max_max < Max(parent_depth, parent)) {

1064 SetRange(parent_depth, parent, max_min, max_max);

1065 } else {

1066 break;

1067 }

1068 depth = parent_depth;

1069 position = parent;

1070 }

1071 if (depth == 0) {

1072 target_var_->SetRange(RootMin(), RootMax());

1073 }

1074 MaxVarChanged();

1075 }

1076

1077 std::string DebugString() const override {

1078 return DebugStringInternal("Max");

1079 }

1080

1081 void Accept(ModelVisitor* const visitor) const override {

1083 }

1084

1085 private:

1086 Demon* max_demon_;

1087};

1088

1089class SmallMaxConstraint : public Constraint {

1090 public:

1091 SmallMaxConstraint(Solver* const solver, const std::vector<IntVar*>& vars,

1092 IntVar* const target_var)

1093 : Constraint(solver),

1094 vars_(vars),

1095 target_var_(target_var),

1096 computed_min_(0),

1097 computed_max_(0) {}

1098

1099 ~SmallMaxConstraint() override {}

1100

1101 void Post() override {

1102 for (int i = 0; i < vars_.size(); ++i) {

1103 if (!vars_[i]->Bound()) {

1105 solver(), this, &SmallMaxConstraint::VarChanged, "VarChanged",

1106 vars_[i]);

1107 vars_[i]->WhenRange(demon);

1108 }

1109 }

1111 solver(), this, &SmallMaxConstraint::MaxVarChanged, "MinVarChanged"));

1112 target_var_->WhenRange(mdemon);

1113 }

1114

1115 void InitialPropagate() override {

1116 int64_t max_min = std::numeric_limits<int64_t>::min();

1117 int64_t max_max = std::numeric_limits<int64_t>::min();

1118 for (IntVar* const var : vars_) {

1119 max_min = std::max(max_min, var->Min());

1120 max_max = std::max(max_max, var->Max());

1121 }

1122 computed_min_.SetValue(solver(), max_min);

1123 computed_max_.SetValue(solver(), max_max);

1124

1125 target_var_->SetRange(max_min, max_max);

1126

1127

1128 MaxVarChanged();

1129 }

1130

1131 std::string DebugString() const override {

1132 return absl::StrFormat("SmallMax(%s) == %s",

1134 target_var_->DebugString());

1135 }

1136

1137 void Accept(ModelVisitor* const visitor) const override {

1140 vars_);

1142 target_var_);

1144 }

1145

1146 private:

1147 void VarChanged(IntVar* var) {

1148 const int64_t old_max = var->OldMax();

1149 const int64_t var_min = var->Min();

1150 const int64_t var_max = var->Max();

1151 if ((old_max == computed_max_.Value() && old_max != var_max) ||

1152 var_min > computed_min_.Value()) {

1153

1154 int64_t max_min = std::numeric_limits<int64_t>::min();

1155 int64_t max_max = std::numeric_limits<int64_t>::min();

1156 for (IntVar* const var : vars_) {

1157 max_min = std::max(max_min, var->Min());

1158 max_max = std::max(max_max, var->Max());

1159 }

1160 if (max_min > computed_min_.Value() || max_max < computed_max_.Value()) {

1161 computed_min_.SetValue(solver(), max_min);

1162 computed_max_.SetValue(solver(), max_max);

1163 target_var_->SetRange(computed_min_.Value(), computed_max_.Value());

1164 }

1165 }

1166 MaxVarChanged();

1167 }

1168

1169 void MaxVarChanged() {

1170 const int64_t new_min = target_var_->Min();

1171 const int64_t new_max = target_var_->Max();

1172

1173 if (new_min <= computed_min_.Value() && new_max >= computed_max_.Value()) {

1174 return;

1175 }

1176

1177 IntVar* candidate = nullptr;

1178 int active = 0;

1179

1180 if (new_min > computed_min_.Value()) {

1181

1182 for (IntVar* const var : vars_) {

1183 if (var->Max() >= new_min) {

1184 if (active++ >= 1) {

1185 break;

1186 }

1187 candidate = var;

1188 }

1189 }

1190 if (active == 0) {

1191 solver()->Fail();

1192 }

1193 }

1194 if (computed_max_.Value() > new_max) {

1195 if (active == 1) {

1196 candidate->SetRange(new_min, new_max);

1197 } else {

1198 for (IntVar* const var : vars_) {

1199 var->SetMax(new_max);

1200 }

1201 }

1202 } else if (active == 1) {

1203 candidate->SetMin(new_min);

1204 }

1205 }

1206

1207 std::vector<IntVar*> vars_;

1208 IntVar* const target_var_;

1209 Rev<int64_t> computed_min_;

1210 Rev<int64_t> computed_max_;

1211};

1212

1213

1214

1216 public:

1217 ArrayBoolAndEq(Solver* const s, const std::vector<IntVar*>& vars,

1218 IntVar* const target)

1219 : CastConstraint(s, target),

1220 vars_(vars),

1221 demons_(vars.size()),

1222 unbounded_(0) {}

1223

1224 ~ArrayBoolAndEq() override {}

1225

1226 void Post() override {

1227 for (int i = 0; i < vars_.size(); ++i) {

1228 if (!vars_[i]->Bound()) {

1229 demons_[i] =

1231 "PropagateVar", vars_[i]);

1232 vars_[i]->WhenBound(demons_[i]);

1233 }

1234 }

1235 if (!target_var_->Bound()) {

1237 solver(), this, &ArrayBoolAndEq::PropagateTarget, "PropagateTarget");

1238 target_var_->WhenBound(target_demon);

1239 }

1240 }

1241

1242 void InitialPropagate() override {

1243 target_var_->SetRange(0, 1);

1244 if (target_var_->Min() == 1) {

1245 for (int i = 0; i < vars_.size(); ++i) {

1246 vars_[i]->SetMin(1);

1247 }

1248 } else {

1249 int possible_zero = -1;

1250 int ones = 0;

1251 int unbounded = 0;

1252 for (int i = 0; i < vars_.size(); ++i) {

1253 if (!vars_[i]->Bound()) {

1254 unbounded++;

1255 possible_zero = i;

1256 } else if (vars_[i]->Max() == 0) {

1257 InhibitAll();

1258 target_var_->SetMax(0);

1259 return;

1260 } else {

1261 DCHECK_EQ(1, vars_[i]->Min());

1262 ones++;

1263 }

1264 }

1265 if (unbounded == 0) {

1266 target_var_->SetMin(1);

1267 } else if (target_var_->Max() == 0 && unbounded == 1) {

1268 CHECK_NE(-1, possible_zero);

1269 vars_[possible_zero]->SetMax(0);

1270 } else {

1271 unbounded_.SetValue(solver(), unbounded);

1272 }

1273 }

1274 }

1275

1276 void PropagateVar(IntVar* var) {

1277 if (var->Min() == 1) {

1278 unbounded_.Decr(solver());

1279 if (unbounded_.Value() == 0 && !decided_.Switched()) {

1280 target_var_->SetMin(1);

1281 decided_.Switch(solver());

1282 } else if (target_var_->Max() == 0 && unbounded_.Value() == 1 &&

1283 !decided_.Switched()) {

1284 ForceToZero();

1285 }

1286 } else {

1287 InhibitAll();

1288 target_var_->SetMax(0);

1289 }

1290 }

1291

1292 void PropagateTarget() {

1293 if (target_var_->Min() == 1) {

1294 for (int i = 0; i < vars_.size(); ++i) {

1295 vars_[i]->SetMin(1);

1296 }

1297 } else {

1298 if (unbounded_.Value() == 1 && !decided_.Switched()) {

1299 ForceToZero();

1300 }

1301 }

1302 }

1303

1304 std::string DebugString() const override {

1305 return absl::StrFormat("And(%s) == %s", JoinDebugStringPtr(vars_, ", "),

1306 target_var_->DebugString());

1307 }

1308

1309 void Accept(ModelVisitor* const visitor) const override {

1312 vars_);

1314 target_var_);

1316 }

1317

1318 private:

1319 void InhibitAll() {

1320 for (int i = 0; i < demons_.size(); ++i) {

1321 if (demons_[i] != nullptr) {

1322 demons_[i]->inhibit(solver());

1323 }

1324 }

1325 }

1326

1327 void ForceToZero() {

1328 for (int i = 0; i < vars_.size(); ++i) {

1329 if (vars_[i]->Min() == 0) {

1330 vars_[i]->SetValue(0);

1331 decided_.Switch(solver());

1332 return;

1333 }

1334 }

1335 solver()->Fail();

1336 }

1337

1338 const std::vector<IntVar*> vars_;

1339 std::vector<Demon*> demons_;

1340 NumericalRev<int> unbounded_;

1341 RevSwitch decided_;

1342};

1343

1345 public:

1346 ArrayBoolOrEq(Solver* const s, const std::vector<IntVar*>& vars,

1347 IntVar* const target)

1348 : CastConstraint(s, target),

1349 vars_(vars),

1350 demons_(vars.size()),

1351 unbounded_(0) {}

1352

1353 ~ArrayBoolOrEq() override {}

1354

1355 void Post() override {

1356 for (int i = 0; i < vars_.size(); ++i) {

1357 if (!vars_[i]->Bound()) {

1358 demons_[i] =

1360 "PropagateVar", vars_[i]);

1361 vars_[i]->WhenBound(demons_[i]);

1362 }

1363 }

1364 if (!target_var_->Bound()) {

1366 solver(), this, &ArrayBoolOrEq::PropagateTarget, "PropagateTarget");

1367 target_var_->WhenBound(target_demon);

1368 }

1369 }

1370

1371 void InitialPropagate() override {

1372 target_var_->SetRange(0, 1);

1373 if (target_var_->Max() == 0) {

1374 for (int i = 0; i < vars_.size(); ++i) {

1375 vars_[i]->SetMax(0);

1376 }

1377 } else {

1378 int zeros = 0;

1379 int possible_one = -1;

1380 int unbounded = 0;

1381 for (int i = 0; i < vars_.size(); ++i) {

1382 if (!vars_[i]->Bound()) {

1383 unbounded++;

1384 possible_one = i;

1385 } else if (vars_[i]->Min() == 1) {

1386 InhibitAll();

1387 target_var_->SetMin(1);

1388 return;

1389 } else {

1390 DCHECK_EQ(0, vars_[i]->Max());

1391 zeros++;

1392 }

1393 }

1394 if (unbounded == 0) {

1395 target_var_->SetMax(0);

1396 } else if (target_var_->Min() == 1 && unbounded == 1) {

1397 CHECK_NE(-1, possible_one);

1398 vars_[possible_one]->SetMin(1);

1399 } else {

1400 unbounded_.SetValue(solver(), unbounded);

1401 }

1402 }

1403 }

1404

1405 void PropagateVar(IntVar* var) {

1406 if (var->Min() == 0) {

1407 unbounded_.Decr(solver());

1408 if (unbounded_.Value() == 0 && !decided_.Switched()) {

1409 target_var_->SetMax(0);

1410 decided_.Switch(solver());

1411 }

1412 if (target_var_->Min() == 1 && unbounded_.Value() == 1 &&

1413 !decided_.Switched()) {

1414 ForceToOne();

1415 }

1416 } else {

1417 InhibitAll();

1418 target_var_->SetMin(1);

1419 }

1420 }

1421

1422 void PropagateTarget() {

1423 if (target_var_->Max() == 0) {

1424 for (int i = 0; i < vars_.size(); ++i) {

1425 vars_[i]->SetMax(0);

1426 }

1427 } else {

1428 if (unbounded_.Value() == 1 && !decided_.Switched()) {

1429 ForceToOne();

1430 }

1431 }

1432 }

1433

1434 std::string DebugString() const override {

1435 return absl::StrFormat("Or(%s) == %s", JoinDebugStringPtr(vars_, ", "),

1436 target_var_->DebugString());

1437 }

1438

1439 void Accept(ModelVisitor* const visitor) const override {

1442 vars_);

1444 target_var_);

1446 }

1447

1448 private:

1449 void InhibitAll() {

1450 for (int i = 0; i < demons_.size(); ++i) {

1451 if (demons_[i] != nullptr) {

1452 demons_[i]->inhibit(solver());

1453 }

1454 }

1455 }

1456

1457 void ForceToOne() {

1458 for (int i = 0; i < vars_.size(); ++i) {

1459 if (vars_[i]->Max() == 1) {

1460 vars_[i]->SetValue(1);

1461 decided_.Switch(solver());

1462 return;

1463 }

1464 }

1465 solver()->Fail();

1466 }

1467

1468 const std::vector<IntVar*> vars_;

1469 std::vector<Demon*> demons_;

1470 NumericalRev<int> unbounded_;

1471 RevSwitch decided_;

1472};

1473

1474

1475

1476class BaseSumBooleanConstraint : public Constraint {

1477 public:

1478 BaseSumBooleanConstraint(Solver* const s, const std::vector<IntVar*>& vars)

1479 : Constraint(s), vars_(vars) {}

1480

1481 ~BaseSumBooleanConstraint() override {}

1482

1483 protected:

1484 std::string DebugStringInternal(absl::string_view name) const {

1485 return absl::StrFormat("%s(%s)", name, JoinDebugStringPtr(vars_, ", "));

1486 }

1487

1488 const std::vector<IntVar*> vars_;

1489 RevSwitch inactive_;

1490};

1491

1492

1493

1494class SumBooleanLessOrEqualToOne : public BaseSumBooleanConstraint {

1495 public:

1496 SumBooleanLessOrEqualToOne(Solver* const s, const std::vector<IntVar*>& vars)

1497 : BaseSumBooleanConstraint(s, vars) {}

1498

1499 ~SumBooleanLessOrEqualToOne() override {}

1500

1501 void Post() override {

1502 for (int i = 0; i < vars_.size(); ++i) {

1503 if (!vars_[i]->Bound()) {

1505 &SumBooleanLessOrEqualToOne::Update,

1506 "Update", vars_[i]);

1507 vars_[i]->WhenBound(u);

1508 }

1509 }

1510 }

1511

1512 void InitialPropagate() override {

1513 for (int i = 0; i < vars_.size(); ++i) {

1514 if (vars_[i]->Min() == 1) {

1515 PushAllToZeroExcept(vars_[i]);

1516 return;

1517 }

1518 }

1519 }

1520

1521 void Update(IntVar* var) {

1522 if (!inactive_.Switched()) {

1523 DCHECK(var->Bound());

1524 if (var->Min() == 1) {

1525 PushAllToZeroExcept(var);

1526 }

1527 }

1528 }

1529

1530 void PushAllToZeroExcept(IntVar* var) {

1531 inactive_.Switch(solver());

1532 for (int i = 0; i < vars_.size(); ++i) {

1533 IntVar* const other = vars_[i];

1534 if (other != var && other->Max() != 0) {

1535 other->SetMax(0);

1536 }

1537 }

1538 }

1539

1540 std::string DebugString() const override {

1541 return DebugStringInternal("SumBooleanLessOrEqualToOne");

1542 }

1543

1544 void Accept(ModelVisitor* const visitor) const override {

1547 vars_);

1550 }

1551};

1552

1553

1554

1555

1556

1557class SumBooleanGreaterOrEqualToOne : public BaseSumBooleanConstraint {

1558 public:

1559 SumBooleanGreaterOrEqualToOne(Solver* s, const std::vector<IntVar*>& vars);

1560 ~SumBooleanGreaterOrEqualToOne() override {}

1561

1562 void Post() override;

1563 void InitialPropagate() override;

1564

1565 void Update(int index);

1566 void UpdateVar();

1567

1568 std::string DebugString() const override;

1569

1570 void Accept(ModelVisitor* const visitor) const override {

1573 vars_);

1576 }

1577

1578 private:

1579 RevBitSet bits_;

1580};

1581

1582SumBooleanGreaterOrEqualToOne::SumBooleanGreaterOrEqualToOne(

1583 Solver* const s, const std::vector<IntVar*>& vars)

1584 : BaseSumBooleanConstraint(s, vars), bits_(vars.size()) {}

1585

1586void SumBooleanGreaterOrEqualToOne::Post() {

1587 for (int i = 0; i < vars_.size(); ++i) {

1589 solver(), this, &SumBooleanGreaterOrEqualToOne::Update, "Update", i);

1590 vars_[i]->WhenRange(d);

1591 }

1592}

1593

1594void SumBooleanGreaterOrEqualToOne::InitialPropagate() {

1595 for (int i = 0; i < vars_.size(); ++i) {

1596 IntVar* const var = vars_[i];

1597 if (var->Min() == 1LL) {

1598 inactive_.Switch(solver());

1599 return;

1600 }

1601 if (var->Max() == 1LL) {

1602 bits_.SetToOne(solver(), i);

1603 }

1604 }

1605 if (bits_.IsCardinalityZero()) {

1606 solver()->Fail();

1607 } else if (bits_.IsCardinalityOne()) {

1608 vars_[bits_.GetFirstBit(0)]->SetValue(int64_t{1});

1609 inactive_.Switch(solver());

1610 }

1611}

1612

1613void SumBooleanGreaterOrEqualToOne::Update(int index) {

1614 if (!inactive_.Switched()) {

1615 if (vars_[index]->Min() == 1LL) {

1616 inactive_.Switch(solver());

1617 } else {

1618 bits_.SetToZero(solver(), index);

1619 if (bits_.IsCardinalityZero()) {

1620 solver()->Fail();

1621 } else if (bits_.IsCardinalityOne()) {

1622 vars_[bits_.GetFirstBit(0)]->SetValue(int64_t{1});

1623 inactive_.Switch(solver());

1624 }

1625 }

1626 }

1627}

1628

1629std::string SumBooleanGreaterOrEqualToOne::DebugString() const {

1630 return DebugStringInternal("SumBooleanGreaterOrEqualToOne");

1631}

1632

1633

1634

1635class SumBooleanEqualToOne : public BaseSumBooleanConstraint {

1636 public:

1637 SumBooleanEqualToOne(Solver* const s, const std::vector<IntVar*>& vars)

1638 : BaseSumBooleanConstraint(s, vars), active_vars_(0) {}

1639

1640 ~SumBooleanEqualToOne() override {}

1641

1642 void Post() override {

1643 for (int i = 0; i < vars_.size(); ++i) {

1645 solver(), this, &SumBooleanEqualToOne::Update, "Update", i);

1646 vars_[i]->WhenBound(u);

1647 }

1648 }

1649

1650 void InitialPropagate() override {

1651 int min1 = 0;

1652 int max1 = 0;

1653 int index_min = -1;

1654 int index_max = -1;

1655 for (int i = 0; i < vars_.size(); ++i) {

1656 const IntVar* const var = vars_[i];

1657 if (var->Min() == 1) {

1658 min1++;

1659 index_min = i;

1660 }

1661 if (var->Max() == 1) {

1662 max1++;

1663 index_max = i;

1664 }

1665 }

1666 if (min1 > 1 || max1 == 0) {

1667 solver()->Fail();

1668 } else if (min1 == 1) {

1669 DCHECK_NE(-1, index_min);

1670 PushAllToZeroExcept(index_min);

1671 } else if (max1 == 1) {

1672 DCHECK_NE(-1, index_max);

1673 vars_[index_max]->SetValue(1);

1674 inactive_.Switch(solver());

1675 } else {

1676 active_vars_.SetValue(solver(), max1);

1677 }

1678 }

1679

1680 void Update(int index) {

1681 if (!inactive_.Switched()) {

1682 DCHECK(vars_[index]->Bound());

1683 const int64_t value = vars_[index]->Min();

1684 if (value == 0) {

1685 active_vars_.Decr(solver());

1686 DCHECK_GE(active_vars_.Value(), 0);

1687 if (active_vars_.Value() == 0) {

1688 solver()->Fail();

1689 } else if (active_vars_.Value() == 1) {

1690 bool found = false;

1691 for (int i = 0; i < vars_.size(); ++i) {

1692 IntVar* const var = vars_[i];

1693 if (var->Max() == 1) {

1694 var->SetValue(1);

1695 PushAllToZeroExcept(i);

1696 found = true;

1697 break;

1698 }

1699 }

1700 if (!found) {

1701 solver()->Fail();

1702 }

1703 }

1704 } else {

1705 PushAllToZeroExcept(index);

1706 }

1707 }

1708 }

1709

1710 void PushAllToZeroExcept(int index) {

1711 inactive_.Switch(solver());

1712 for (int i = 0; i < vars_.size(); ++i) {

1713 if (i != index && vars_[i]->Max() != 0) {

1714 vars_[i]->SetMax(0);

1715 }

1716 }

1717 }

1718

1719 std::string DebugString() const override {

1720 return DebugStringInternal("SumBooleanEqualToOne");

1721 }

1722

1723 void Accept(ModelVisitor* const visitor) const override {

1724 visitor->BeginVisitConstraint(ModelVisitor::kSumEqual, this);

1725 visitor->VisitIntegerVariableArrayArgument(ModelVisitor::kVarsArgument,

1726 vars_);

1727 visitor->VisitIntegerArgument(ModelVisitor::kValueArgument, 1);

1728 visitor->EndVisitConstraint(ModelVisitor::kSumEqual, this);

1729 }

1730

1731 private:

1732 NumericalRev<int> active_vars_;

1733};

1734

1735

1736

1737class SumBooleanEqualToVar : public BaseSumBooleanConstraint {

1738 public:

1739 SumBooleanEqualToVar(Solver* const s, const std::vector<IntVar*>& bool_vars,

1740 IntVar* const sum_var)

1741 : BaseSumBooleanConstraint(s, bool_vars),

1742 num_possible_true_vars_(0),

1743 num_always_true_vars_(0),

1744 sum_var_(sum_var) {}

1745

1746 ~SumBooleanEqualToVar() override {}

1747

1748 void Post() override {

1749 for (int i = 0; i < vars_.size(); ++i) {

1751 solver(), this, &SumBooleanEqualToVar::Update, "Update", i);

1752 vars_[i]->WhenBound(u);

1753 }

1754 if (!sum_var_->Bound()) {

1756 solver(), this, &SumBooleanEqualToVar::UpdateVar, "UpdateVar");

1757 sum_var_->WhenRange(u);

1758 }

1759 }

1760

1761 void InitialPropagate() override {

1762 int num_always_true_vars = 0;

1763 int possible_true = 0;

1764 for (int i = 0; i < vars_.size(); ++i) {

1765 const IntVar* const var = vars_[i];

1766 if (var->Min() == 1) {

1767 num_always_true_vars++;

1768 }

1769 if (var->Max() == 1) {

1770 possible_true++;

1771 }

1772 }

1773 sum_var_->SetRange(num_always_true_vars, possible_true);

1774 const int64_t var_min = sum_var_->Min();

1775 const int64_t var_max = sum_var_->Max();

1776 if (num_always_true_vars == var_max && possible_true > var_max) {

1777 PushAllUnboundToZero();

1778 } else if (possible_true == var_min && num_always_true_vars < var_min) {

1779 PushAllUnboundToOne();

1780 } else {

1781 num_possible_true_vars_.SetValue(solver(), possible_true);

1782 num_always_true_vars_.SetValue(solver(), num_always_true_vars);

1783 }

1784 }

1785

1786 void UpdateVar() {

1787 if (!inactive_.Switched()) {

1788 if (num_possible_true_vars_.Value() == sum_var_->Min()) {

1789 PushAllUnboundToOne();

1790 sum_var_->SetValue(num_possible_true_vars_.Value());

1791 } else if (num_always_true_vars_.Value() == sum_var_->Max()) {

1792 PushAllUnboundToZero();

1793 sum_var_->SetValue(num_always_true_vars_.Value());

1794 }

1795 }

1796 }

1797

1798 void Update(int index) {

1799 if (!inactive_.Switched()) {

1800 DCHECK(vars_[index]->Bound());

1801 const int64_t value = vars_[index]->Min();

1802 if (value == 0) {

1803 num_possible_true_vars_.Decr(solver());

1804 sum_var_->SetRange(num_always_true_vars_.Value(),

1805 num_possible_true_vars_.Value());

1806 if (num_possible_true_vars_.Value() == sum_var_->Min()) {

1807 PushAllUnboundToOne();

1808 }

1809 } else {

1810 DCHECK_EQ(1, value);

1811 num_always_true_vars_.Incr(solver());

1812 sum_var_->SetRange(num_always_true_vars_.Value(),

1813 num_possible_true_vars_.Value());

1814 if (num_always_true_vars_.Value() == sum_var_->Max()) {

1815 PushAllUnboundToZero();

1816 }

1817 }

1818 }

1819 }

1820

1821 void PushAllUnboundToZero() {

1822 int64_t counter = 0;

1823 inactive_.Switch(solver());

1824 for (int i = 0; i < vars_.size(); ++i) {

1825 if (vars_[i]->Min() == 0) {

1826 vars_[i]->SetValue(0);

1827 } else {

1828 counter++;

1829 }

1830 }

1831 if (counter < sum_var_->Min() || counter > sum_var_->Max()) {

1832 solver()->Fail();

1833 }

1834 }

1835

1836 void PushAllUnboundToOne() {

1837 int64_t counter = 0;

1838 inactive_.Switch(solver());

1839 for (int i = 0; i < vars_.size(); ++i) {

1840 if (vars_[i]->Max() == 1) {

1841 vars_[i]->SetValue(1);

1842 counter++;

1843 }

1844 }

1845 if (counter < sum_var_->Min() || counter > sum_var_->Max()) {

1846 solver()->Fail();

1847 }

1848 }

1849

1850 std::string DebugString() const override {

1851 return absl::StrFormat("%s == %s", DebugStringInternal("SumBoolean"),

1852 sum_var_->DebugString());

1853 }

1854

1855 void Accept(ModelVisitor* const visitor) const override {

1856 visitor->BeginVisitConstraint(ModelVisitor::kSumEqual, this);

1857 visitor->VisitIntegerVariableArrayArgument(ModelVisitor::kVarsArgument,

1858 vars_);

1859 visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,

1860 sum_var_);

1861 visitor->EndVisitConstraint(ModelVisitor::kSumEqual, this);

1862 }

1863

1864 private:

1865 NumericalRev<int> num_possible_true_vars_;

1866 NumericalRev<int> num_always_true_vars_;

1867 IntVar* const sum_var_;

1868};

1869

1870

1871

1872

1873

1874struct Container {

1875 IntVar* var;

1876 int64_t coef;

1877 Container(IntVar* v, int64_t c) : var(v), coef(c) {}

1878 bool operator<(const Container& c) const { return (coef < c.coef); }

1879};

1880

1881

1882

1883

1884

1885

1886

1887

1888int64_t SortBothChangeConstant(std::vector<IntVar*>* const vars,

1889 std::vector<int64_t>* const coefs,

1890 bool keep_inside) {

1891 CHECK(vars != nullptr);

1892 CHECK(coefs != nullptr);

1893 if (vars->empty()) {

1894 return 0;

1895 }

1896 int64_t cst = 0;

1897 std::vector<Container> to_sort;

1898 for (int index = 0; index < vars->size(); ++index) {

1899 if ((*vars)[index]->Bound()) {

1900 cst = CapAdd(cst, CapProd((*coefs)[index], (*vars)[index]->Min()));

1901 } else if ((*coefs)[index] != 0) {

1902 to_sort.push_back(Container((*vars)[index], (*coefs)[index]));

1903 }

1904 }

1905 if (keep_inside && cst != 0) {

1906 CHECK_LT(to_sort.size(), vars->size());

1907 Solver* const solver = (*vars)[0]->solver();

1908 to_sort.push_back(Container(solver->MakeIntConst(1), cst));

1909 cst = 0;

1910 }

1911 std::sort(to_sort.begin(), to_sort.end());

1912 for (int index = 0; index < to_sort.size(); ++index) {

1913 (*vars)[index] = to_sort[index].var;

1914 (*coefs)[index] = to_sort[index].coef;

1915 }

1916 vars->resize(to_sort.size());

1917 coefs->resize(to_sort.size());

1918 return cst;

1919}

1920

1921

1922

1923class BooleanScalProdLessConstant : public Constraint {

1924 public:

1925 BooleanScalProdLessConstant(Solver* const s, const std::vector<IntVar*>& vars,

1926 const std::vector<int64_t>& coefs,

1927 int64_t upper_bound)

1928 : Constraint(s),

1929 vars_(vars),

1930 coefs_(coefs),

1931 upper_bound_(upper_bound),

1932 first_unbound_backward_(vars.size() - 1),

1933 sum_of_bound_variables_(0LL),

1934 max_coefficient_(0) {

1935 CHECK(!vars.empty());

1936 for (int i = 0; i < vars_.size(); ++i) {

1937 DCHECK_GE(coefs_[i], 0);

1938 }

1939 upper_bound_ =

1940 CapSub(upper_bound, SortBothChangeConstant(&vars_, &coefs_, false));

1941 max_coefficient_.SetValue(s, coefs_[vars_.size() - 1]);

1942 }

1943

1944 ~BooleanScalProdLessConstant() override {}

1945

1946 void Post() override {

1947 for (int var_index = 0; var_index < vars_.size(); ++var_index) {

1948 if (vars_[var_index]->Bound()) {

1949 continue;

1950 }

1952 &BooleanScalProdLessConstant::Update,

1953 "InitialPropagate", var_index);

1954 vars_[var_index]->WhenRange(d);

1955 }

1956 }

1957

1958 void PushFromTop() {

1959 const int64_t slack = CapSub(upper_bound_, sum_of_bound_variables_.Value());

1960 if (slack < 0) {

1961 solver()->Fail();

1962 }

1963 if (slack < max_coefficient_.Value()) {

1964 int64_t last_unbound = first_unbound_backward_.Value();

1965 for (; last_unbound >= 0; --last_unbound) {

1966 if (!vars_[last_unbound]->Bound()) {

1967 if (coefs_[last_unbound] <= slack) {

1968 max_coefficient_.SetValue(solver(), coefs_[last_unbound]);

1969 break;

1970 } else {

1971 vars_[last_unbound]->SetValue(0);

1972 }

1973 }

1974 }

1975 first_unbound_backward_.SetValue(solver(), last_unbound);

1976 }

1977 }

1978

1979 void InitialPropagate() override {

1980 Solver* const s = solver();

1981 int last_unbound = -1;

1982 int64_t sum = 0LL;

1983 for (int index = 0; index < vars_.size(); ++index) {

1984 if (vars_[index]->Bound()) {

1985 const int64_t value = vars_[index]->Min();

1986 sum = CapAdd(sum, CapProd(value, coefs_[index]));

1987 } else {

1988 last_unbound = index;

1989 }

1990 }

1991 sum_of_bound_variables_.SetValue(s, sum);

1992 first_unbound_backward_.SetValue(s, last_unbound);

1993 PushFromTop();

1994 }

1995

1996 void Update(int var_index) {

1997 if (vars_[var_index]->Min() == 1) {

1998 sum_of_bound_variables_.SetValue(

1999 solver(), CapAdd(sum_of_bound_variables_.Value(), coefs_[var_index]));

2000 PushFromTop();

2001 }

2002 }

2003

2004 std::string DebugString() const override {

2005 return absl::StrFormat("BooleanScalProd([%s], [%s]) <= %d)",

2007 absl::StrJoin(coefs_, ", "), upper_bound_);

2008 }

2009

2010 void Accept(ModelVisitor* const visitor) const override {

2011 visitor->BeginVisitConstraint(ModelVisitor::kScalProdLessOrEqual, this);

2012 visitor->VisitIntegerVariableArrayArgument(ModelVisitor::kVarsArgument,

2013 vars_);

2014 visitor->VisitIntegerArrayArgument(ModelVisitor::kCoefficientsArgument,

2015 coefs_);

2016 visitor->VisitIntegerArgument(ModelVisitor::kValueArgument, upper_bound_);

2017 visitor->EndVisitConstraint(ModelVisitor::kScalProdLessOrEqual, this);

2018 }

2019

2020 private:

2021 std::vector<IntVar*> vars_;

2022 std::vector<int64_t> coefs_;

2023 int64_t upper_bound_;

2024 Rev<int> first_unbound_backward_;

2025 Rev<int64_t> sum_of_bound_variables_;

2026 Rev<int64_t> max_coefficient_;

2027};

2028

2029

2030

2031class PositiveBooleanScalProdEqVar : public CastConstraint {

2032 public:

2033 PositiveBooleanScalProdEqVar(Solver* const s,

2034 const std::vector<IntVar*>& vars,

2035 const std::vector<int64_t>& coefs,

2036 IntVar* const var)

2037 : CastConstraint(s, var),

2038 vars_(vars),

2039 coefs_(coefs),

2040 first_unbound_backward_(vars.size() - 1),

2041 sum_of_bound_variables_(0LL),

2042 sum_of_all_variables_(0LL),

2043 max_coefficient_(0) {

2044 SortBothChangeConstant(&vars_, &coefs_, true);

2045 max_coefficient_.SetValue(s, coefs_[vars_.size() - 1]);

2046 }

2047

2048 ~PositiveBooleanScalProdEqVar() override {}

2049

2050 void Post() override {

2051 for (int var_index = 0; var_index < vars_.size(); ++var_index) {

2052 if (vars_[var_index]->Bound()) {

2053 continue;

2054 }

2056 solver(), this, &PositiveBooleanScalProdEqVar::Update, "Update",

2057 var_index);

2058 vars_[var_index]->WhenRange(d);

2059 }

2060 if (!target_var_->Bound()) {

2062 solver(), this, &PositiveBooleanScalProdEqVar::Propagate,

2063 "Propagate");

2064 target_var_->WhenRange(uv);

2065 }

2066 }

2067

2068 void Propagate() {

2069 target_var_->SetRange(sum_of_bound_variables_.Value(),

2070 sum_of_all_variables_.Value());

2071 const int64_t slack_up =

2072 CapSub(target_var_->Max(), sum_of_bound_variables_.Value());

2073 const int64_t slack_down =

2074 CapSub(sum_of_all_variables_.Value(), target_var_->Min());

2075 const int64_t max_coeff = max_coefficient_.Value();

2076 if (slack_down < max_coeff || slack_up < max_coeff) {

2077 int64_t last_unbound = first_unbound_backward_.Value();

2078 for (; last_unbound >= 0; --last_unbound) {

2079 if (!vars_[last_unbound]->Bound()) {

2080 if (coefs_[last_unbound] > slack_up) {

2081 vars_[last_unbound]->SetValue(0);

2082 } else if (coefs_[last_unbound] > slack_down) {

2083 vars_[last_unbound]->SetValue(1);

2084 } else {

2085 max_coefficient_.SetValue(solver(), coefs_[last_unbound]);

2086 break;

2087 }

2088 }

2089 }

2090 first_unbound_backward_.SetValue(solver(), last_unbound);

2091 }

2092 }

2093

2094 void InitialPropagate() override {

2095 Solver* const s = solver();

2096 int last_unbound = -1;

2097 int64_t sum_bound = 0;

2098 int64_t sum_all = 0;

2099 for (int index = 0; index < vars_.size(); ++index) {

2100 const int64_t value = CapProd(vars_[index]->Max(), coefs_[index]);

2101 sum_all = CapAdd(sum_all, value);

2102 if (vars_[index]->Bound()) {

2103 sum_bound = CapAdd(sum_bound, value);

2104 } else {

2105 last_unbound = index;

2106 }

2107 }

2108 sum_of_bound_variables_.SetValue(s, sum_bound);

2109 sum_of_all_variables_.SetValue(s, sum_all);

2110 first_unbound_backward_.SetValue(s, last_unbound);

2111 Propagate();

2112 }

2113

2114 void Update(int var_index) {

2115 if (vars_[var_index]->Min() == 1) {

2116 sum_of_bound_variables_.SetValue(

2117 solver(), CapAdd(sum_of_bound_variables_.Value(), coefs_[var_index]));

2118 } else {

2119 sum_of_all_variables_.SetValue(

2120 solver(), CapSub(sum_of_all_variables_.Value(), coefs_[var_index]));

2121 }

2122 Propagate();

2123 }

2124

2125 std::string DebugString() const override {

2126 return absl::StrFormat("PositiveBooleanScal([%s], [%s]) == %s",

2128 absl::StrJoin(coefs_, ", "),

2129 target_var_->DebugString());

2130 }

2131

2132 void Accept(ModelVisitor* const visitor) const override {

2133 visitor->BeginVisitConstraint(ModelVisitor::kScalProdEqual, this);

2134 visitor->VisitIntegerVariableArrayArgument(ModelVisitor::kVarsArgument,

2135 vars_);

2136 visitor->VisitIntegerArrayArgument(ModelVisitor::kCoefficientsArgument,

2137 coefs_);

2138 visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,

2139 target_var_);

2140 visitor->EndVisitConstraint(ModelVisitor::kScalProdEqual, this);

2141 }

2142

2143 private:

2144 std::vector<IntVar*> vars_;

2145 std::vector<int64_t> coefs_;

2146 Rev<int> first_unbound_backward_;

2147 Rev<int64_t> sum_of_bound_variables_;

2148 Rev<int64_t> sum_of_all_variables_;

2149 Rev<int64_t> max_coefficient_;

2150};

2151

2152

2153

2154class PositiveBooleanScalProd : public BaseIntExpr {

2155 public:

2156

2157

2158 PositiveBooleanScalProd(Solver* const s, const std::vector<IntVar*>& vars,

2159 const std::vector<int64_t>& coefs)

2160 : BaseIntExpr(s), vars_(vars), coefs_(coefs) {

2161 CHECK(!vars.empty());

2162 SortBothChangeConstant(&vars_, &coefs_, true);

2163 for (int i = 0; i < vars_.size(); ++i) {

2164 DCHECK_GE(coefs_[i], 0);

2165 }

2166 }

2167

2168 ~PositiveBooleanScalProd() override {}

2169

2170 int64_t Min() const override {

2171 int64_t min = 0;

2172 for (int i = 0; i < vars_.size(); ++i) {

2173 if (vars_[i]->Min()) {

2174 min = CapAdd(min, coefs_[i]);

2175 }

2176 }

2177 return min;

2178 }

2179

2180 void SetMin(int64_t m) override {

2181 SetRange(m, std::numeric_limits<int64_t>::max());

2182 }

2183

2184 int64_t Max() const override {

2185 int64_t max = 0;

2186 for (int i = 0; i < vars_.size(); ++i) {

2187 if (vars_[i]->Max()) {

2188 max = CapAdd(max, coefs_[i]);

2189 }

2190 }

2191 return max;

2192 }

2193

2194 void SetMax(int64_t m) override {

2195 SetRange(std::numeric_limits<int64_t>::min(), m);

2196 }

2197

2198 void SetRange(int64_t l, int64_t u) override {

2199 int64_t current_min = 0;

2200 int64_t current_max = 0;

2201 int64_t diameter = -1;

2202 for (int i = 0; i < vars_.size(); ++i) {

2203 const int64_t coefficient = coefs_[i];

2204 const int64_t var_min = CapProd(vars_[i]->Min(), coefficient);

2205 const int64_t var_max = CapProd(vars_[i]->Max(), coefficient);

2206 current_min = CapAdd(current_min, var_min);

2207 current_max = CapAdd(current_max, var_max);

2208 if (var_min != var_max) {

2209 diameter = CapSub(var_max, var_min);

2210 }

2211 }

2212 if (u >= current_max && l <= current_min) {

2213 return;

2214 }

2215 if (u < current_min || l > current_max) {

2216 solver()->Fail();

2217 }

2218

2219 u = std::min(current_max, u);

2220 l = std::max(l, current_min);

2221

2222 if (CapSub(u, l) > diameter) {

2223 return;

2224 }

2225

2226 for (int i = 0; i < vars_.size(); ++i) {

2227 const int64_t coefficient = coefs_[i];

2228 IntVar* const var = vars_[i];

2229 const int64_t new_min =

2231 const int64_t new_max =

2233 if (new_max < 0 || new_min > coefficient || new_min > new_max) {

2234 solver()->Fail();

2235 }

2236 if (new_min > 0LL) {

2237 var->SetMin(int64_t{1});

2238 } else if (new_max < coefficient) {

2239 var->SetMax(int64_t{0});

2240 }

2241 }

2242 }

2243

2244 std::string DebugString() const override {

2245 return absl::StrFormat("PositiveBooleanScalProd([%s], [%s])",

2247 absl::StrJoin(coefs_, ", "));

2248 }

2249

2250 void WhenRange(Demon* d) override {

2251 for (int i = 0; i < vars_.size(); ++i) {

2252 vars_[i]->WhenRange(d);

2253 }

2254 }

2255 IntVar* CastToVar() override {

2256 Solver* const s = solver();

2257 int64_t vmin = 0LL;

2258 int64_t vmax = 0LL;

2259 Range(&vmin, &vmax);

2260 IntVar* const var = solver()->MakeIntVar(vmin, vmax);

2261 if (!vars_.empty()) {

2262 CastConstraint* const ct =

2263 s->RevAlloc(new PositiveBooleanScalProdEqVar(s, vars_, coefs_, var));

2264 s->AddCastConstraint(ct, var, this);

2265 }

2266 return var;

2267 }

2268

2269 void Accept(ModelVisitor* const visitor) const override {

2270 visitor->BeginVisitIntegerExpression(ModelVisitor::kScalProd, this);

2271 visitor->VisitIntegerVariableArrayArgument(ModelVisitor::kVarsArgument,

2272 vars_);

2273 visitor->VisitIntegerArrayArgument(ModelVisitor::kCoefficientsArgument,

2274 coefs_);

2275 visitor->EndVisitIntegerExpression(ModelVisitor::kScalProd, this);

2276 }

2277

2278 private:

2279 std::vector<IntVar*> vars_;

2280 std::vector<int64_t> coefs_;

2281};

2282

2283

2284

2285class PositiveBooleanScalProdEqCst : public Constraint {

2286 public:

2287 PositiveBooleanScalProdEqCst(Solver* const s,

2288 const std::vector<IntVar*>& vars,

2289 const std::vector<int64_t>& coefs,

2290 int64_t constant)

2291 : Constraint(s),

2292 vars_(vars),

2293 coefs_(coefs),

2294 first_unbound_backward_(vars.size() - 1),

2295 sum_of_bound_variables_(0LL),

2296 sum_of_all_variables_(0LL),

2297 constant_(constant),

2298 max_coefficient_(0) {

2299 CHECK(!vars.empty());

2300 constant_ =

2301 CapSub(constant_, SortBothChangeConstant(&vars_, &coefs_, false));

2302 max_coefficient_.SetValue(s, coefs_[vars_.size() - 1]);

2303 }

2304

2305 ~PositiveBooleanScalProdEqCst() override {}

2306

2307 void Post() override {

2308 for (int var_index = 0; var_index < vars_.size(); ++var_index) {

2309 if (!vars_[var_index]->Bound()) {

2311 solver(), this, &PositiveBooleanScalProdEqCst::Update, "Update",

2312 var_index);

2313 vars_[var_index]->WhenRange(d);

2314 }

2315 }

2316 }

2317

2318 void Propagate() {

2319 if (sum_of_bound_variables_.Value() > constant_ ||

2320 sum_of_all_variables_.Value() < constant_) {

2321 solver()->Fail();

2322 }

2323 const int64_t slack_up = CapSub(constant_, sum_of_bound_variables_.Value());

2324 const int64_t slack_down = CapSub(sum_of_all_variables_.Value(), constant_);

2325 const int64_t max_coeff = max_coefficient_.Value();

2326 if (slack_down < max_coeff || slack_up < max_coeff) {

2327 int64_t last_unbound = first_unbound_backward_.Value();

2328 for (; last_unbound >= 0; --last_unbound) {

2329 if (!vars_[last_unbound]->Bound()) {

2330 if (coefs_[last_unbound] > slack_up) {

2331 vars_[last_unbound]->SetValue(0);

2332 } else if (coefs_[last_unbound] > slack_down) {

2333 vars_[last_unbound]->SetValue(1);

2334 } else {

2335 max_coefficient_.SetValue(solver(), coefs_[last_unbound]);

2336 break;

2337 }

2338 }

2339 }

2340 first_unbound_backward_.SetValue(solver(), last_unbound);

2341 }

2342 }

2343

2344 void InitialPropagate() override {

2345 Solver* const s = solver();

2346 int last_unbound = -1;

2347 int64_t sum_bound = 0LL;

2348 int64_t sum_all = 0LL;

2349 for (int index = 0; index < vars_.size(); ++index) {

2350 const int64_t value = CapProd(vars_[index]->Max(), coefs_[index]);

2351 sum_all = CapAdd(sum_all, value);

2352 if (vars_[index]->Bound()) {

2353 sum_bound = CapAdd(sum_bound, value);

2354 } else {

2355 last_unbound = index;

2356 }

2357 }

2358 sum_of_bound_variables_.SetValue(s, sum_bound);

2359 sum_of_all_variables_.SetValue(s, sum_all);

2360 first_unbound_backward_.SetValue(s, last_unbound);

2361 Propagate();

2362 }

2363

2364 void Update(int var_index) {

2365 if (vars_[var_index]->Min() == 1) {

2366 sum_of_bound_variables_.SetValue(

2367 solver(), CapAdd(sum_of_bound_variables_.Value(), coefs_[var_index]));

2368 } else {

2369 sum_of_all_variables_.SetValue(

2370 solver(), CapSub(sum_of_all_variables_.Value(), coefs_[var_index]));

2371 }

2372 Propagate();

2373 }

2374

2375 std::string DebugString() const override {

2376 return absl::StrFormat("PositiveBooleanScalProd([%s], [%s]) == %d",

2378 absl::StrJoin(coefs_, ", "), constant_);

2379 }

2380

2381 void Accept(ModelVisitor* const visitor) const override {

2382 visitor->BeginVisitConstraint(ModelVisitor::kScalProdEqual, this);

2383 visitor->VisitIntegerVariableArrayArgument(ModelVisitor::kVarsArgument,

2384 vars_);

2385 visitor->VisitIntegerArrayArgument(ModelVisitor::kCoefficientsArgument,

2386 coefs_);

2387 visitor->VisitIntegerArgument(ModelVisitor::kValueArgument, constant_);

2388 visitor->EndVisitConstraint(ModelVisitor::kScalProdEqual, this);

2389 }

2390

2391 private:

2392 std::vector<IntVar*> vars_;

2393 std::vector<int64_t> coefs_;

2394 Rev<int> first_unbound_backward_;

2395 Rev<int64_t> sum_of_bound_variables_;

2396 Rev<int64_t> sum_of_all_variables_;

2397 int64_t constant_;

2398 Rev<int64_t> max_coefficient_;

2399};

2400

2401

2402

2403#define IS_TYPE(type, tag) type.compare(ModelVisitor::tag) == 0

2404

2405class ExprLinearizer : public ModelParser {

2406 public:

2407 explicit ExprLinearizer(

2408 absl::flat_hash_map<IntVar*, int64_t>* const variables_to_coefficients)

2409 : variables_to_coefficients_(variables_to_coefficients), constant_(0) {}

2410

2411 ~ExprLinearizer() override {}

2412

2413

2414 void BeginVisitModel(const std::string& solver_name) override {

2415 LOG(FATAL) << "Should not be here";

2416 }

2417

2418 void EndVisitModel(const std::string& solver_name) override {

2419 LOG(FATAL) << "Should not be here";

2420 }

2421

2422 void BeginVisitConstraint(const std::string& type_name,

2423 const Constraint* const constraint) override {

2424 LOG(FATAL) << "Should not be here";

2425 }

2426

2427 void EndVisitConstraint(const std::string& type_name,

2428 const Constraint* const constraint) override {

2429 LOG(FATAL) << "Should not be here";

2430 }

2431

2432 void BeginVisitExtension(const std::string& type) override {}

2433

2434 void EndVisitExtension(const std::string& type) override {}

2435 void BeginVisitIntegerExpression(const std::string& type_name,

2436 const IntExpr* const expr) override {

2437 BeginVisit(true);

2438 }

2439

2440 void EndVisitIntegerExpression(const std::string& type_name,

2441 const IntExpr* const expr) override {

2442 if (IS_TYPE(type_name, kSum)) {

2443 VisitSum(expr);

2444 } else if (IS_TYPE(type_name, kScalProd)) {

2445 VisitScalProd(expr);

2446 } else if (IS_TYPE(type_name, kDifference)) {

2447 VisitDifference(expr);

2448 } else if (IS_TYPE(type_name, kOpposite)) {

2449 VisitOpposite(expr);

2450 } else if (IS_TYPE(type_name, kProduct)) {

2451 VisitProduct(expr);

2452 } else if (IS_TYPE(type_name, kTrace)) {

2453 VisitTrace(expr);

2454 } else {

2455 VisitIntegerExpression(expr);

2456 }

2457 EndVisit();

2458 }

2459

2460 void VisitIntegerVariable(const IntVar* const variable,

2461 const std::string& operation, int64_t value,

2462 IntVar* const delegate) override {

2463 if (operation == ModelVisitor::kSumOperation) {

2464 AddConstant(value);

2465 VisitSubExpression(delegate);

2466 } else if (operation == ModelVisitor::kDifferenceOperation) {

2467 AddConstant(value);

2468 PushMultiplier(-1);

2469 VisitSubExpression(delegate);

2470 PopMultiplier();

2471 } else if (operation == ModelVisitor::kProductOperation) {

2472 PushMultiplier(value);

2473 VisitSubExpression(delegate);

2474 PopMultiplier();

2475 } else if (operation == ModelVisitor::kTraceOperation) {

2476 VisitSubExpression(delegate);

2477 }

2478 }

2479

2480 void VisitIntegerVariable(const IntVar* const variable,

2481 IntExpr* const delegate) override {

2482 if (delegate != nullptr) {

2483 VisitSubExpression(delegate);

2484 } else {

2485 if (variable->Bound()) {

2486 AddConstant(variable->Min());

2487 } else {

2488 RegisterExpression(variable, 1);

2489 }

2490 }

2491 }

2492

2493

2494 void VisitIntegerArgument(const std::string& arg_name,

2495 int64_t value) override {

2496 Top()->SetIntegerArgument(arg_name, value);

2497 }

2498

2499 void VisitIntegerArrayArgument(const std::string& arg_name,

2500 const std::vector<int64_t>& values) override {

2501 Top()->SetIntegerArrayArgument(arg_name, values);

2502 }

2503

2504 void VisitIntegerMatrixArgument(const std::string& arg_name,

2505 const IntTupleSet& values) override {

2506 Top()->SetIntegerMatrixArgument(arg_name, values);

2507 }

2508

2509

2510 void VisitIntegerExpressionArgument(const std::string& arg_name,

2511 IntExpr* const argument) override {

2512 Top()->SetIntegerExpressionArgument(arg_name, argument);

2513 }

2514

2515 void VisitIntegerVariableArrayArgument(

2516 const std::string& arg_name,

2517 const std::vector<IntVar*>& arguments) override {

2518 Top()->SetIntegerVariableArrayArgument(arg_name, arguments);

2519 }

2520

2521

2522 void VisitIntervalArgument(const std::string& arg_name,

2523 IntervalVar* const argument) override {}

2524

2525 void VisitIntervalArrayArgument(

2526 const std::string& arg_name,

2527 const std::vector<IntervalVar*>& argument) override {}

2528

2529 void Visit(const IntExpr* const expr, int64_t multiplier) {

2530 if (expr->Min() == expr->Max()) {

2531 constant_ = CapAdd(constant_, CapProd(expr->Min(), multiplier));

2532 } else {

2533 PushMultiplier(multiplier);

2534 expr->Accept(this);

2535 PopMultiplier();

2536 }

2537 }

2538

2539 int64_t Constant() const { return constant_; }

2540

2541 std::string DebugString() const override { return "ExprLinearizer"; }

2542

2543 private:

2544 void BeginVisit(bool active) { PushArgumentHolder(); }

2545

2546 void EndVisit() { PopArgumentHolder(); }

2547

2548 void VisitSubExpression(const IntExpr* const cp_expr) {

2549 cp_expr->Accept(this);

2550 }

2551

2552 void VisitSum(const IntExpr* const cp_expr) {

2553 if (Top()->HasIntegerVariableArrayArgument(ModelVisitor::kVarsArgument)) {

2554 const std::vector<IntVar*>& cp_vars =

2555 Top()->FindIntegerVariableArrayArgumentOrDie(

2556 ModelVisitor::kVarsArgument);

2557 for (int i = 0; i < cp_vars.size(); ++i) {

2558 VisitSubExpression(cp_vars[i]);

2559 }

2560 } else if (Top()->HasIntegerExpressionArgument(

2561 ModelVisitor::kLeftArgument)) {

2562 const IntExpr* const left = Top()->FindIntegerExpressionArgumentOrDie(

2563 ModelVisitor::kLeftArgument);

2564 const IntExpr* const right = Top()->FindIntegerExpressionArgumentOrDie(

2565 ModelVisitor::kRightArgument);

2566 VisitSubExpression(left);

2567 VisitSubExpression(right);

2568 } else {

2569 const IntExpr* const expr = Top()->FindIntegerExpressionArgumentOrDie(

2570 ModelVisitor::kExpressionArgument);

2571 const int64_t value =

2572 Top()->FindIntegerArgumentOrDie(ModelVisitor::kValueArgument);

2573 VisitSubExpression(expr);

2574 AddConstant(value);

2575 }

2576 }

2577

2578 void VisitScalProd(const IntExpr* const cp_expr) {

2579 const std::vector<IntVar*>& cp_vars =

2580 Top()->FindIntegerVariableArrayArgumentOrDie(

2581 ModelVisitor::kVarsArgument);

2582 const std::vector<int64_t>& cp_coefficients =

2583 Top()->FindIntegerArrayArgumentOrDie(

2584 ModelVisitor::kCoefficientsArgument);

2585 CHECK_EQ(cp_vars.size(), cp_coefficients.size());

2586 for (int i = 0; i < cp_vars.size(); ++i) {

2587 const int64_t coefficient = cp_coefficients[i];

2588 PushMultiplier(coefficient);

2589 VisitSubExpression(cp_vars[i]);

2590 PopMultiplier();

2591 }

2592 }

2593

2594 void VisitDifference(const IntExpr* const cp_expr) {

2595 if (Top()->HasIntegerExpressionArgument(ModelVisitor::kLeftArgument)) {

2596 const IntExpr* const left = Top()->FindIntegerExpressionArgumentOrDie(

2597 ModelVisitor::kLeftArgument);

2598 const IntExpr* const right = Top()->FindIntegerExpressionArgumentOrDie(

2599 ModelVisitor::kRightArgument);

2600 VisitSubExpression(left);

2601 PushMultiplier(-1);

2602 VisitSubExpression(right);

2603 PopMultiplier();

2604 } else {

2605 const IntExpr* const expr = Top()->FindIntegerExpressionArgumentOrDie(

2606 ModelVisitor::kExpressionArgument);

2607 const int64_t value =

2608 Top()->FindIntegerArgumentOrDie(ModelVisitor::kValueArgument);

2609 AddConstant(value);

2610 PushMultiplier(-1);

2611 VisitSubExpression(expr);

2612 PopMultiplier();

2613 }

2614 }

2615

2616 void VisitOpposite(const IntExpr* const cp_expr) {

2617 const IntExpr* const expr = Top()->FindIntegerExpressionArgumentOrDie(

2618 ModelVisitor::kExpressionArgument);

2619 PushMultiplier(-1);

2620 VisitSubExpression(expr);

2621 PopMultiplier();

2622 }

2623

2624 void VisitProduct(const IntExpr* const cp_expr) {

2625 if (Top()->HasIntegerExpressionArgument(

2626 ModelVisitor::kExpressionArgument)) {

2627 const IntExpr* const expr = Top()->FindIntegerExpressionArgumentOrDie(

2628 ModelVisitor::kExpressionArgument);

2629 const int64_t value =

2630 Top()->FindIntegerArgumentOrDie(ModelVisitor::kValueArgument);

2631 PushMultiplier(value);

2632 VisitSubExpression(expr);

2633 PopMultiplier();

2634 } else {

2635 RegisterExpression(cp_expr, 1);

2636 }

2637 }

2638

2639 void VisitTrace(const IntExpr* const cp_expr) {

2640 const IntExpr* const expr = Top()->FindIntegerExpressionArgumentOrDie(

2641 ModelVisitor::kExpressionArgument);

2642 VisitSubExpression(expr);

2643 }

2644

2645 void VisitIntegerExpression(const IntExpr* const cp_expr) {

2646 RegisterExpression(cp_expr, 1);

2647 }

2648

2649 void RegisterExpression(const IntExpr* const expr, int64_t coef) {

2650 int64_t& value =

2651 (*variables_to_coefficients_)[const_cast<IntExpr*>(expr)->Var()];

2652 value = CapAdd(value, CapProd(coef, multipliers_.back()));

2653 }

2654

2655 void AddConstant(int64_t constant) {

2656 constant_ = CapAdd(constant_, CapProd(constant, multipliers_.back()));

2657 }

2658

2659 void PushMultiplier(int64_t multiplier) {

2660 if (multipliers_.empty()) {

2661 multipliers_.push_back(multiplier);

2662 } else {

2663 multipliers_.push_back(CapProd(multiplier, multipliers_.back()));

2664 }

2665 }

2666

2667 void PopMultiplier() { multipliers_.pop_back(); }

2668

2669

2670

2671 absl::flat_hash_map<IntVar*, int64_t>* const variables_to_coefficients_;

2672 std::vector<int64_t> multipliers_;

2673 int64_t constant_;

2674};

2675#undef IS_TYPE

2676

2677

2678

2679void DeepLinearize(Solver* const solver, const std::vector<IntVar*>& pre_vars,

2680 absl::Span<const int64_t> pre_coefs,

2681 std::vector<IntVar*>* vars, std::vector<int64_t>* coefs,

2682 int64_t* constant) {

2683 CHECK(solver != nullptr);

2684 CHECK(vars != nullptr);

2685 CHECK(coefs != nullptr);

2686 CHECK(constant != nullptr);

2687 *constant = 0;

2688 vars->reserve(pre_vars.size());

2689 coefs->reserve(pre_coefs.size());

2690

2691 bool need_linearization = false;

2692 for (int i = 0; i < pre_vars.size(); ++i) {

2693 IntVar* const variable = pre_vars[i];

2694 const int64_t coefficient = pre_coefs[i];

2695 if (variable->Bound()) {

2696 *constant = CapAdd(*constant, CapProd(coefficient, variable->Min()));

2697 } else if (solver->CastExpression(variable) == nullptr) {

2698 vars->push_back(variable);

2699 coefs->push_back(coefficient);

2700 } else {

2701 need_linearization = true;

2702 vars->clear();

2703 coefs->clear();

2704 break;

2705 }

2706 }

2707 if (need_linearization) {

2708

2709 absl::flat_hash_map<IntVar*, int64_t> variables_to_coefficients;

2710 ExprLinearizer linearizer(&variables_to_coefficients);

2711 for (int i = 0; i < pre_vars.size(); ++i) {

2712 linearizer.Visit(pre_vars[i], pre_coefs[i]);

2713 }

2714 *constant = linearizer.Constant();

2715 for (const auto& variable_to_coefficient : variables_to_coefficients) {

2716 if (variable_to_coefficient.second != 0) {

2717 vars->push_back(variable_to_coefficient.first);

2718 coefs->push_back(variable_to_coefficient.second);

2719 }

2720 }

2721 }

2722}

2723

2724Constraint* MakeScalProdEqualityFct(Solver* const solver,

2725 const std::vector<IntVar*>& pre_vars,

2726 absl::Span<const int64_t> pre_coefs,

2727 int64_t cst) {

2728 int64_t constant = 0;

2729 std::vector<IntVar*> vars;

2730 std::vector<int64_t> coefs;

2731 DeepLinearize(solver, pre_vars, pre_coefs, &vars, &coefs, &constant);

2732 cst = CapSub(cst, constant);

2733

2734 const int size = vars.size();

2735 if (size == 0 || AreAllNull(coefs)) {

2736 return cst == 0 ? solver->MakeTrueConstraint()

2737 : solver->MakeFalseConstraint();

2738 }

2740 int64_t sum = 0;

2741 for (int i = 0; i < size; ++i) {

2742 sum = CapAdd(sum, CapProd(coefs[i], vars[i]->Min()));

2743 }

2744 return sum == cst ? solver->MakeTrueConstraint()

2745 : solver->MakeFalseConstraint();

2746 }

2748 return solver->MakeSumEquality(vars, cst);

2749 }

2752 return solver->RevAlloc(

2753 new PositiveBooleanScalProdEqCst(solver, vars, coefs, cst));

2754 }

2756 std::vector<int64_t> opp_coefs(coefs.size());

2757 for (int i = 0; i < coefs.size(); ++i) {

2758 opp_coefs[i] = -coefs[i];

2759 }

2760 return solver->RevAlloc(

2761 new PositiveBooleanScalProdEqCst(solver, vars, opp_coefs, -cst));

2762 }

2763 }

2764

2765

2766 int constants = 0;

2767 int positives = 0;

2768 int negatives = 0;

2769 for (int i = 0; i < size; ++i) {

2770 if (coefs[i] == 0 || vars[i]->Bound()) {

2771 constants++;

2772 } else if (coefs[i] > 0) {

2773 positives++;

2774 } else {

2775 negatives++;

2776 }

2777 }

2778 if (positives > 0 && negatives > 0) {

2779 std::vector<IntVar*> pos_terms;

2780 std::vector<IntVar*> neg_terms;

2781 int64_t rhs = cst;

2782 for (int i = 0; i < size; ++i) {

2783 if (coefs[i] == 0 || vars[i]->Bound()) {

2784 rhs = CapSub(rhs, CapProd(coefs[i], vars[i]->Min()));

2785 } else if (coefs[i] > 0) {

2786 pos_terms.push_back(solver->MakeProd(vars[i], coefs[i])->Var());

2787 } else {

2788 neg_terms.push_back(solver->MakeProd(vars[i], -coefs[i])->Var());

2789 }

2790 }

2791 if (negatives == 1) {

2792 if (rhs != 0) {

2793 pos_terms.push_back(solver->MakeIntConst(-rhs));

2794 }

2795 return solver->MakeSumEquality(pos_terms, neg_terms[0]);

2796 } else if (positives == 1) {

2797 if (rhs != 0) {

2798 neg_terms.push_back(solver->MakeIntConst(rhs));

2799 }

2800 return solver->MakeSumEquality(neg_terms, pos_terms[0]);

2801 } else {

2802 if (rhs != 0) {

2803 neg_terms.push_back(solver->MakeIntConst(rhs));

2804 }

2805 return solver->MakeEquality(solver->MakeSum(pos_terms),

2806 solver->MakeSum(neg_terms));

2807 }

2808 } else if (positives == 1) {

2809 IntExpr* pos_term = nullptr;

2810 int64_t rhs = cst;

2811 for (int i = 0; i < size; ++i) {

2812 if (coefs[i] == 0 || vars[i]->Bound()) {

2813 rhs = CapSub(rhs, CapProd(coefs[i], vars[i]->Min()));

2814 } else if (coefs[i] > 0) {

2815 pos_term = solver->MakeProd(vars[i], coefs[i]);

2816 } else {

2817 LOG(FATAL) << "Should not be here";

2818 }

2819 }

2820 return solver->MakeEquality(pos_term, rhs);

2821 } else if (negatives == 1) {

2822 IntExpr* neg_term = nullptr;

2823 int64_t rhs = cst;

2824 for (int i = 0; i < size; ++i) {

2825 if (coefs[i] == 0 || vars[i]->Bound()) {

2826 rhs = CapSub(rhs, CapProd(coefs[i], vars[i]->Min()));

2827 } else if (coefs[i] > 0) {

2828 LOG(FATAL) << "Should not be here";

2829 } else {

2830 neg_term = solver->MakeProd(vars[i], -coefs[i]);

2831 }

2832 }

2833 return solver->MakeEquality(neg_term, -rhs);

2834 } else if (positives > 1) {

2835 std::vector<IntVar*> pos_terms;

2836 int64_t rhs = cst;

2837 for (int i = 0; i < size; ++i) {

2838 if (coefs[i] == 0 || vars[i]->Bound()) {

2839 rhs = CapSub(rhs, CapProd(coefs[i], vars[i]->Min()));

2840 } else if (coefs[i] > 0) {

2841 pos_terms.push_back(solver->MakeProd(vars[i], coefs[i])->Var());

2842 } else {

2843 LOG(FATAL) << "Should not be here";

2844 }

2845 }

2846 return solver->MakeSumEquality(pos_terms, rhs);

2847 } else if (negatives > 1) {

2848 std::vector<IntVar*> neg_terms;

2849 int64_t rhs = cst;

2850 for (int i = 0; i < size; ++i) {

2851 if (coefs[i] == 0 || vars[i]->Bound()) {

2852 rhs = CapSub(rhs, CapProd(coefs[i], vars[i]->Min()));

2853 } else if (coefs[i] > 0) {

2854 LOG(FATAL) << "Should not be here";

2855 } else {

2856 neg_terms.push_back(solver->MakeProd(vars[i], -coefs[i])->Var());

2857 }

2858 }

2859 return solver->MakeSumEquality(neg_terms, -rhs);

2860 }

2861 std::vector<IntVar*> terms;

2862 for (int i = 0; i < size; ++i) {

2863 terms.push_back(solver->MakeProd(vars[i], coefs[i])->Var());

2864 }

2865 return solver->MakeSumEquality(terms, solver->MakeIntConst(cst));

2866}

2867

2868Constraint* MakeScalProdEqualityVarFct(Solver* const solver,

2869 const std::vector<IntVar*>& pre_vars,

2870 absl::Span<const int64_t> pre_coefs,

2871 IntVar* const target) {

2872 int64_t constant = 0;

2873 std::vector<IntVar*> vars;

2874 std::vector<int64_t> coefs;

2875 DeepLinearize(solver, pre_vars, pre_coefs, &vars, &coefs, &constant);

2876

2877 const int size = vars.size();

2878 if (size == 0 || AreAllNull<int64_t>(coefs)) {

2879 return solver->MakeEquality(target, constant);

2880 }

2882 return solver->MakeSumEquality(vars,

2883 solver->MakeSum(target, -constant)->Var());

2884 }

2885 if (AreAllBooleans(vars) && AreAllPositive<int64_t>(coefs)) {

2886

2887 return solver->RevAlloc(new PositiveBooleanScalProdEqVar(

2888 solver, vars, coefs, solver->MakeSum(target, -constant)->Var()));

2889 }

2890 std::vector<IntVar*> terms;

2891 for (int i = 0; i < size; ++i) {

2892 terms.push_back(solver->MakeProd(vars[i], coefs[i])->Var());

2893 }

2894 return solver->MakeSumEquality(terms,

2895 solver->MakeSum(target, -constant)->Var());

2896}

2897

2898Constraint* MakeScalProdGreaterOrEqualFct(Solver* solver,

2899 const std::vector<IntVar*>& pre_vars,

2900 absl::Span<const int64_t> pre_coefs,

2901 int64_t cst) {

2902 int64_t constant = 0;

2903 std::vector<IntVar*> vars;

2904 std::vector<int64_t> coefs;

2905 DeepLinearize(solver, pre_vars, pre_coefs, &vars, &coefs, &constant);

2906 cst = CapSub(cst, constant);

2907

2908 const int size = vars.size();

2909 if (size == 0 || AreAllNull<int64_t>(coefs)) {

2910 return cst <= 0 ? solver->MakeTrueConstraint()

2911 : solver->MakeFalseConstraint();

2912 }

2914 return solver->MakeSumGreaterOrEqual(vars, cst);

2915 }

2917

2918 std::vector<IntVar*> terms;

2919 for (int i = 0; i < size; ++i) {

2920 if (coefs[i] > 0) {

2921 terms.push_back(vars[i]);

2922 }

2923 }

2924 return solver->MakeSumGreaterOrEqual(terms, 1);

2925 }

2926 std::vector<IntVar*> terms;

2927 for (int i = 0; i < size; ++i) {

2928 terms.push_back(solver->MakeProd(vars[i], coefs[i])->Var());

2929 }

2930 return solver->MakeSumGreaterOrEqual(terms, cst);

2931}

2932

2933Constraint* MakeScalProdLessOrEqualFct(Solver* solver,

2934 const std::vector<IntVar*>& pre_vars,

2935 absl::Span<const int64_t> pre_coefs,

2936 int64_t upper_bound) {

2937 int64_t constant = 0;

2938 std::vector<IntVar*> vars;

2939 std::vector<int64_t> coefs;

2940 DeepLinearize(solver, pre_vars, pre_coefs, &vars, &coefs, &constant);

2941 upper_bound = CapSub(upper_bound, constant);

2942

2943 const int size = vars.size();

2944 if (size == 0 || AreAllNull<int64_t>(coefs)) {

2945 return upper_bound >= 0 ? solver->MakeTrueConstraint()

2946 : solver->MakeFalseConstraint();

2947 }

2948

2950 int64_t cst = 0;

2951 for (int i = 0; i < size; ++i) {

2952 cst = CapAdd(cst, CapProd(vars[i]->Min(), coefs[i]));

2953 }

2954 return cst <= upper_bound ? solver->MakeTrueConstraint()

2955 : solver->MakeFalseConstraint();

2956 }

2958 return solver->MakeSumLessOrEqual(vars, upper_bound);

2959 }

2960 if (AreAllBooleans(vars) && AreAllPositive<int64_t>(coefs)) {

2961 return solver->RevAlloc(

2962 new BooleanScalProdLessConstant(solver, vars, coefs, upper_bound));

2963 }

2964

2965 int constants = 0;

2966 int positives = 0;

2967 int negatives = 0;

2968 for (int i = 0; i < size; ++i) {

2969 if (coefs[i] == 0 || vars[i]->Bound()) {

2970 constants++;

2971 } else if (coefs[i] > 0) {

2972 positives++;

2973 } else {

2974 negatives++;

2975 }

2976 }

2977 if (positives > 0 && negatives > 0) {

2978 std::vector<IntVar*> pos_terms;

2979 std::vector<IntVar*> neg_terms;

2980 int64_t rhs = upper_bound;

2981 for (int i = 0; i < size; ++i) {

2982 if (coefs[i] == 0 || vars[i]->Bound()) {

2983 rhs = CapSub(rhs, CapProd(coefs[i], vars[i]->Min()));

2984 } else if (coefs[i] > 0) {

2985 pos_terms.push_back(solver->MakeProd(vars[i], coefs[i])->Var());

2986 } else {

2987 neg_terms.push_back(solver->MakeProd(vars[i], -coefs[i])->Var());

2988 }

2989 }

2990 if (negatives == 1) {

2991 IntExpr* const neg_term = solver->MakeSum(neg_terms[0], rhs);

2992 return solver->MakeLessOrEqual(solver->MakeSum(pos_terms), neg_term);

2993 } else if (positives == 1) {

2994 IntExpr* const pos_term = solver->MakeSum(pos_terms[0], -rhs);

2995 return solver->MakeGreaterOrEqual(solver->MakeSum(neg_terms), pos_term);

2996 } else {

2997 if (rhs != 0) {

2998 neg_terms.push_back(solver->MakeIntConst(rhs));

2999 }

3000 return solver->MakeLessOrEqual(solver->MakeSum(pos_terms),

3001 solver->MakeSum(neg_terms));

3002 }

3003 } else if (positives == 1) {

3004 IntExpr* pos_term = nullptr;

3005 int64_t rhs = upper_bound;

3006 for (int i = 0; i < size; ++i) {

3007 if (coefs[i] == 0 || vars[i]->Bound()) {

3008 rhs = CapSub(rhs, CapProd(coefs[i], vars[i]->Min()));

3009 } else if (coefs[i] > 0) {

3010 pos_term = solver->MakeProd(vars[i], coefs[i]);

3011 } else {

3012 LOG(FATAL) << "Should not be here";

3013 }

3014 }

3015 return solver->MakeLessOrEqual(pos_term, rhs);

3016 } else if (negatives == 1) {

3017 IntExpr* neg_term = nullptr;

3018 int64_t rhs = upper_bound;

3019 for (int i = 0; i < size; ++i) {

3020 if (coefs[i] == 0 || vars[i]->Bound()) {

3021 rhs = CapSub(rhs, CapProd(coefs[i], vars[i]->Min()));

3022 } else if (coefs[i] > 0) {

3023 LOG(FATAL) << "Should not be here";

3024 } else {

3025 neg_term = solver->MakeProd(vars[i], -coefs[i]);

3026 }

3027 }

3028 return solver->MakeGreaterOrEqual(neg_term, -rhs);

3029 } else if (positives > 1) {

3030 std::vector<IntVar*> pos_terms;

3031 int64_t rhs = upper_bound;

3032 for (int i = 0; i < size; ++i) {

3033 if (coefs[i] == 0 || vars[i]->Bound()) {

3034 rhs = CapSub(rhs, CapProd(coefs[i], vars[i]->Min()));

3035 } else if (coefs[i] > 0) {

3036 pos_terms.push_back(solver->MakeProd(vars[i], coefs[i])->Var());

3037 } else {

3038 LOG(FATAL) << "Should not be here";

3039 }

3040 }

3041 return solver->MakeSumLessOrEqual(pos_terms, rhs);

3042 } else if (negatives > 1) {

3043 std::vector<IntVar*> neg_terms;

3044 int64_t rhs = upper_bound;

3045 for (int i = 0; i < size; ++i) {

3046 if (coefs[i] == 0 || vars[i]->Bound()) {

3047 rhs = CapSub(rhs, CapProd(coefs[i], vars[i]->Min()));

3048 } else if (coefs[i] > 0) {

3049 LOG(FATAL) << "Should not be here";

3050 } else {

3051 neg_terms.push_back(solver->MakeProd(vars[i], -coefs[i])->Var());

3052 }

3053 }

3054 return solver->MakeSumGreaterOrEqual(neg_terms, -rhs);

3055 }

3056 std::vector<IntVar*> terms;

3057 for (int i = 0; i < size; ++i) {

3058 terms.push_back(solver->MakeProd(vars[i], coefs[i])->Var());

3059 }

3060 return solver->MakeLessOrEqual(solver->MakeSum(terms), upper_bound);

3061}

3062

3063IntExpr* MakeSumArrayAux(Solver* const solver, const std::vector<IntVar*>& vars,

3064 int64_t constant) {

3065 const int size = vars.size();

3066 DCHECK_GT(size, 2);

3067 int64_t new_min = 0;

3068 int64_t new_max = 0;

3069 for (int i = 0; i < size; ++i) {

3070 if (new_min != std::numeric_limits<int64_t>::min()) {

3071 new_min = CapAdd(vars[i]->Min(), new_min);

3072 }

3073 if (new_max != std::numeric_limits<int64_t>::max()) {

3074 new_max = CapAdd(vars[i]->Max(), new_max);

3075 }

3076 }

3077 IntExpr* const cache =

3078 solver->Cache()->FindVarArrayExpression(vars, ModelCache::VAR_ARRAY_SUM);

3079 if (cache != nullptr) {

3080 return solver->MakeSum(cache, constant);

3081 } else {

3082 const std::string name =

3083 absl::StrFormat("Sum([%s])", JoinNamePtr(vars, ", "));

3084 IntVar* const sum_var = solver->MakeIntVar(new_min, new_max, name);

3086 solver->AddConstraint(

3087 solver->RevAlloc(new SumBooleanEqualToVar(solver, vars, sum_var)));

3088 } else if (size <= solver->parameters().array_split_size()) {

3089 solver->AddConstraint(

3090 solver->RevAlloc(new SmallSumConstraint(solver, vars, sum_var)));

3091 } else {

3092 solver->AddConstraint(

3093 solver->RevAlloc(new SumConstraint(solver, vars, sum_var)));

3094 }

3095 solver->Cache()->InsertVarArrayExpression(sum_var, vars,

3096 ModelCache::VAR_ARRAY_SUM);

3097 return solver->MakeSum(sum_var, constant);

3098 }

3099}

3100

3101IntExpr* MakeSumAux(Solver* const solver, const std::vector<IntVar*>& vars,

3102 int64_t constant) {

3103 const int size = vars.size();

3104 if (size == 0) {

3105 return solver->MakeIntConst(constant);

3106 } else if (size == 1) {

3107 return solver->MakeSum(vars[0], constant);

3108 } else if (size == 2) {

3109 return solver->MakeSum(solver->MakeSum(vars[0], vars[1]), constant);

3110 } else {

3111 return MakeSumArrayAux(solver, vars, constant);

3112 }

3113}

3114

3115IntExpr* MakeScalProdAux(Solver* solver, const std::vector<IntVar*>& vars,

3116 const std::vector<int64_t>& coefs, int64_t constant) {

3118 return MakeSumAux(solver, vars, constant);

3119 }

3120

3121 const int size = vars.size();

3122 if (size == 0) {

3123 return solver->MakeIntConst(constant);

3124 } else if (size == 1) {

3125 return solver->MakeSum(solver->MakeProd(vars[0], coefs[0]), constant);

3126 } else if (size == 2) {

3127 if (coefs[0] > 0 && coefs[1] < 0) {

3128 return solver->MakeSum(

3129 solver->MakeDifference(solver->MakeProd(vars[0], coefs[0]),

3130 solver->MakeProd(vars[1], -coefs[1])),

3131 constant);

3132 } else if (coefs[0] < 0 && coefs[1] > 0) {

3133 return solver->MakeSum(

3134 solver->MakeDifference(solver->MakeProd(vars[1], coefs[1]),

3135 solver->MakeProd(vars[0], -coefs[0])),

3136 constant);

3137 } else {

3138 return solver->MakeSum(

3139 solver->MakeSum(solver->MakeProd(vars[0], coefs[0]),

3140 solver->MakeProd(vars[1], coefs[1])),

3141 constant);

3142 }

3143 } else {

3146 if (vars.size() > 8) {

3147 return solver->MakeSum(

3148 solver

3149 ->RegisterIntExpr(solver->RevAlloc(

3150 new PositiveBooleanScalProd(solver, vars, coefs)))

3151 ->Var(),

3152 constant);

3153 } else {

3154 return solver->MakeSum(

3155 solver->RegisterIntExpr(solver->RevAlloc(

3156 new PositiveBooleanScalProd(solver, vars, coefs))),

3157 constant);

3158 }

3159 } else {

3160

3161

3162

3163

3164

3165

3166

3167 std::vector<int64_t> positive_coefs;

3168 std::vector<int64_t> negative_coefs;

3169 std::vector<IntVar*> positive_coef_vars;

3170 std::vector<IntVar*> negative_coef_vars;

3171 for (int i = 0; i < size; ++i) {

3172 const int coef = coefs[i];

3173 if (coef > 0) {

3174 positive_coefs.push_back(coef);

3175 positive_coef_vars.push_back(vars[i]);

3176 } else if (coef < 0) {

3177 negative_coefs.push_back(-coef);

3178 negative_coef_vars.push_back(vars[i]);

3179 }

3180 }

3181 CHECK_GT(negative_coef_vars.size(), 0);

3182 IntExpr* const negatives =

3183 MakeScalProdAux(solver, negative_coef_vars, negative_coefs, 0);

3184 if (!positive_coef_vars.empty()) {

3185 IntExpr* const positives = MakeScalProdAux(solver, positive_coef_vars,

3186 positive_coefs, constant);

3187 return solver->MakeDifference(positives, negatives);

3188 } else {

3189 return solver->MakeDifference(constant, negatives);

3190 }

3191 }

3192 }

3193 }

3194 std::vector<IntVar*> terms;

3195 for (int i = 0; i < size; ++i) {

3196 terms.push_back(solver->MakeProd(vars[i], coefs[i])->Var());

3197 }

3198 return MakeSumArrayAux(solver, terms, constant);

3199}

3200

3201IntExpr* MakeScalProdFct(Solver* solver, const std::vector<IntVar*>& pre_vars,

3202 absl::Span<const int64_t> pre_coefs) {

3203 int64_t constant = 0;

3204 std::vector<IntVar*> vars;

3205 std::vector<int64_t> coefs;

3206 DeepLinearize(solver, pre_vars, pre_coefs, &vars, &coefs, &constant);

3207

3208 if (vars.empty()) {

3209 return solver->MakeIntConst(constant);

3210 }

3211

3212 int64_t gcd = std::abs(coefs[0]);

3213 for (int i = 1; i < coefs.size(); ++i) {

3214 gcd = MathUtil::GCD64(gcd, std::abs(coefs[i]));

3215 if (gcd == 1) {

3216 break;

3217 }

3218 }

3219 if (constant != 0 && gcd != 1) {

3220 gcd = MathUtil::GCD64(gcd, std::abs(constant));

3221 }

3222 if (gcd > 1) {

3223 for (int i = 0; i < coefs.size(); ++i) {

3224 coefs[i] /= gcd;

3225 }

3226 return solver->MakeProd(

3227 MakeScalProdAux(solver, vars, coefs, constant / gcd), gcd);

3228 }

3229 return MakeScalProdAux(solver, vars, coefs, constant);

3230}

3231

3232IntExpr* MakeSumFct(Solver* solver, const std::vector<IntVar*>& pre_vars) {

3233 absl::flat_hash_map<IntVar*, int64_t> variables_to_coefficients;

3234 ExprLinearizer linearizer(&variables_to_coefficients);

3235 for (int i = 0; i < pre_vars.size(); ++i) {

3236 linearizer.Visit(pre_vars[i], 1);

3237 }

3238 const int64_t constant = linearizer.Constant();

3239 std::vector<IntVar*> vars;

3240 std::vector<int64_t> coefs;

3241 for (const auto& variable_to_coefficient : variables_to_coefficients) {

3242 if (variable_to_coefficient.second != 0) {

3243 vars.push_back(variable_to_coefficient.first);

3244 coefs.push_back(variable_to_coefficient.second);

3245 }

3246 }

3247 return MakeScalProdAux(solver, vars, coefs, constant);

3248}

3249}

3250

3251

3252

3301

3344

3387

3409

3431

3441

3451

3481

3506

3513

3520

3527

3535

3542

3549

3556

3564

3570

3576}